Tool SMACK 1.9.3 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-07 19:13:55 CET 2018-12-08 22:05:35 CET 2018-12-08 23:40:49 CET 2018-12-12 21:01:56 CET 2018-12-08 22:13:47 CET
Run set smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options -w error-witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu wall mem energy blkio-w blkio-r
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(valid-memcleanup) 1 wit inspect 3.4 3.4 89 48 .86 0   false(valid-memcleanup) 1 wit inspect 4.4 2.4 250 0   0     true -32 --- inspect 8.1 4.5 310 .62 0     true -32 --- inspect .65 .65 20 .078 0      - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.9 4.1 94 48 1.2  0   false(valid-memcleanup) 1 wit inspect 4.6 2.5 260 0   0     error (7) 0 --- inspect 23   13   360 .75 0     error (2) 0 --- inspect .74 .74 20 .13  0      - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 8.2 8.1 120 110 1.2  0   error (recursion) 0 wit inspect 4.3 2.4 250 0   0     error (7) 0 --- inspect 21   12   340 .71 .016 error (2) 0 --- inspect .69 .68 20 .12  0      - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 4.1 95 45 1.2  0   false(valid-memcleanup) 1 wit inspect 4.8 2.6 270 0   0     error (7) 0 --- inspect 24   14   340 .71 13     true -32 --- inspect .67 .67 20 .11  .029  - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 4.0 97 56 1.1  0   false(valid-memcleanup) 1 wit inspect 5.6 3.0 280 0   0     error (7) 0 --- inspect 22   13   330 .68 0     error (2) 0 --- inspect .67 .67 20 .11  0      - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.7 3.5 96 46 .99 0   false(valid-memcleanup) 1 wit inspect 5.5 2.9 270 0   0     error (7) 0 --- inspect 18   10   310 .68 0     true -32 --- inspect .66 .66 20 .094 0      - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.9 4.1 130 54 1.0  0   false(valid-memcleanup) 1 wit inspect 4.4 2.4 260 0   .63  error (7) 0 --- inspect 20   12   310 .68 0     error (2) 0 --- inspect .66 .70 20 .094 .025  - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.6 3.5 94 48 .92 0   false(valid-memcleanup) 1 wit inspect 4.1 2.2 250 0   0     error (7) 0 --- inspect 18   10   310 .71 0     timeout 0 --- inspect 96    96    20 .090 0      - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.7 3.5 94 44 .94 0   false(valid-memcleanup) 1 wit inspect 4.2 2.3 250 0   0     error (7) 0 --- inspect 16   9.9 310 .68 0     error (2) 0 --- inspect .66 .66 20 .090 .0041 - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.1 4.0 100 57 1.0  0   false(valid-memcleanup) 1 wit inspect 6.4 3.4 270 0   .025 error (7) 0 --- inspect 17   9.4 310 .71 0     true -32 --- inspect .66 .68 20 .094 0      - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.7 3.6 95 51 .95 0   false(valid-memcleanup) 1 wit inspect 4.3 2.4 250 0   0     error (7) 0 --- inspect 17   10   310 .71 .020 error (2) 0 --- inspect .66 .66 20 .086 0      - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.0 4.1 100 39 1.0  0   false(valid-memcleanup) 1 wit inspect 5.8 3.1 260 0   0     error (7) 0 --- inspect 16   9.7 310 .68 0     error (2) 0 --- inspect .67 .67 20 .094 0      - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.6 3.5 95 46 .94 0   false(valid-memcleanup) 1 wit inspect 5.3 2.9 270 0   0     error (7) 0 --- inspect 19   11   310 .68 0     true -32 --- inspect .66 .65 20 .086 0      - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 4.0 97 50 .99 0   false(valid-memcleanup) 1 wit inspect 5.7 3.1 250 0   0     error (7) 0 --- inspect 19   11   310 .75 0     true -32 --- inspect .67 .67 20 .090 0      - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.6 3.5 98 42 .92 0   false(valid-memcleanup) 1 wit inspect 4.2 2.3 250 0   0     error (7) 0 --- inspect 20   11   310 .71 .016 timeout 0 --- inspect 96    97    20 .090 0      - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.7 3.5 93 43 .92 0   false(valid-memcleanup) 1 wit inspect 4.1 2.3 250 0   0     error (7) 0 --- inspect 16   9.8 310 .68 0     error (2) 0 --- inspect .66 .66 20 .090 .35   - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.1 4.1 100 50 1.0  0   false(valid-memcleanup) 1 wit inspect 4.7 2.5 250 0   0     error (7) 0 --- inspect 17   9.8 310 .75 0     true -32 --- inspect .66 .66 20 .090 0      - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 4.0 96 58 .93 0   false(valid-memcleanup) 1 wit inspect 4.7 2.6 250 0   0     error (7) 0 --- inspect 17   9.7 310 .75 0     true -32 --- inspect .66 .66 20 .086 .0041 - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.7 3.5 97 50 .92 0   false(valid-memcleanup) 1 wit inspect 4.5 2.4 250 0   0     error (7) 0 --- inspect 19   11   310 .75 0     error (2) 0 --- inspect .69 .69 20 .086 0      - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 4.4 4.6 110 66 .99 0   timeout 0 wit inspect 97   68   2400 0   0     error (7) 0 --- inspect 16   9.4 310 .68 0     error (2) 0 --- inspect .67 .67 20 .090 0      - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.6 3.5 120 43 .92 0   false(valid-memcleanup) 1 wit inspect 5.7 3.1 260 0   0     error (7) 0 --- inspect 16   9.3 310 .68 0     true -32 --- inspect .66 .66 20 .086 0      - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.5 3.5 89 39 .89 0   false(valid-memcleanup) 1 wit inspect 4.1 2.3 250 0   0     true -32 --- inspect 9.6 5.2 320 .66 0     true -32 --- inspect .67 .67 20 .078 0      - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.6 3.5 120 40 .89 0   false(valid-memcleanup) 1 wit inspect 5.8 3.1 270 0   0     true -32 --- inspect 10   6.0 300 .62 0     error (2) 0 --- inspect .70 .71 20 .078 0      - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.4 3.5 89 42 .87 0   false(valid-memcleanup) 1 wit inspect 4.9 2.7 250 0   0     true -32 --- inspect 8.0 4.9 310 .62 0     error (2) 0 --- inspect .66 .66 20 .078 0      - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.5 3.4 84 45 .86 0   false(valid-memcleanup) 1 wit inspect 4.2 2.3 240 0   0     true -32 --- inspect 10   5.5 310 .66 0     true -32 --- inspect .64 .64 20 .078 0      - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.9 4.0 94 47 .91 0   false(valid-memcleanup) 1 wit inspect 5.8 3.2 250 0   0     true -32 --- inspect 8.8 4.9 320 .62 0     true -32 --- inspect .69 .69 20 .098 0      - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.4 3.4 85 50 .84 0   false(valid-memcleanup) 1 wit inspect 4.5 2.5 260 0   0     true -32 --- inspect 8.2 4.6 310 .62 .012 true -32 --- inspect .65 .65 20 .078 0      - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.5 3.5 98 40 .90 0   false(valid-memcleanup) 1 wit inspect 4.4 2.4 260 0   0     true -32 --- inspect 8.5 5.1 310 .62 .033 true -32 --- inspect .65 .65 20 .082 0      - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.3 4.5 94 54 .91 0   false(valid-memcleanup) 1 wit inspect 6.3 3.4 260 0   .012 true -32 --- inspect 8.6 4.8 320 .66 0     error (2) 0 --- inspect .65 .65 20 .086 0      - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 3.5 3.5 86 43 .86 0   true -32 wit inspect 7.3 3.9 270 0   0     true -32 --- inspect 8.7 5.2 310 .66 0     true -32 --- inspect .65 .65 20 .082 0      - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 3.6 3.5 91 44 .94 0   true -32 wit inspect 4.8 2.6 260 0   .57  true -32 --- inspect 9.6 5.3 330 .66 .012 error (2) 0 --- inspect .66 .66 20 .098 0      - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 7.4 7.1 130 88 1.0  0   false(valid-memcleanup) 1 wit inspect 8.0 4.2 270 0   0     true -32 --- inspect 8.4 5.1 320 .66 0     error (2) 0 --- inspect .68 .70 20 .057 0      - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu wall mem energy blkio-w blkio-r
total 32 28 130 130 3200 1600 31   0   32 -36 250 150   10000 0   1.2  32 -384 480 280 10000 22   13     32 -480 210   210   650 2.9 .41  0
    correct results 28 28 110 110 2800 1400 27   0   28 28 140 76   7200 0   .67 0 0 0
        correct true 0 0 0 0 0
        correct false 28 28 110 110 2800 1400 27   0   28 28 140 76   7200 0   .67 0 0 0
    correct-unconfimed results 4 0 20 20 410 260 4.0 0   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 4 0 20 20 410 260 4.0 0   0 0 0 0
    incorrect results 0 2 -64 12 6.4 520 0   .57 12 -384 110 61 3800 7.7 .057 15 -480 9.9 9.9 310 1.3 .033 0
        incorrect true 0 2 -64 12 6.4 520 0   .57 12 -384 110 61 3800 7.7 .057 15 -480 9.9 9.9 310 1.3 .033 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 28 -36 -384 -480 0
Run set smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-MemCleanup