Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 04:38:11 CET [[ 2017-01-14 23:48:17 CET ]] [[ 2017-01-14 23:57:43 CET ]] [[ 2017-01-14 23:52:59 CET ]] [[ 2017-01-15 00:03:21 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 11   4.2  15 220 0   0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 7.0 3.7 86 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (recursion) 0 wit inspect 2.7 1.1  25 220 0   0   - - error (invalid witness file) .61 .39 8.3 40 error (invalid witness file) 6.9 3.7 82 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   700    1500 4400 0   0   - - error (invalid witness file) .52 .33 8.7 40 error (invalid witness file) 6.6 3.5 69 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 930   670    9300 7800 0   0   - - error (invalid witness file) .48 .32 9.4 39 error (invalid witness file) 6.2 3.3 110 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 3.6 1.3  32 260 0   0   false(valid-deref) 6.1  3.3  75   260 true 8.3 4.5 120 320 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 3.1 1.2  28 250 0   0   true 4.7  2.6  55   260 true 10   5.4 140 340 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.4 1.3  27 260 0   0   false(valid-memtrack) 5.4  2.9  66   260 true 17   9.3 250 550 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   700    9000 7300 0   0   error (invalid witness file) .54 .35 8.5 39 error (invalid witness file) 7.6 3.9 120 320 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 13   4.7  16 260 0   0   false(valid-memtrack) 6.1  3.3  58   260 unknown 22   11   230 350 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.3 1.2  25 260 0   0   false(valid-memtrack) 4.9  2.7  57   280 unknown 18   9.6 310 350 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 940   620    9200 9400 0   0   - - error (invalid witness file) .47 .31 11   40 error (invalid witness file) 6.0 3.2 110 290
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   700    6800 7500 0   0   error (invalid witness file) .50 .34 12   40 error (invalid witness file) 6.7 3.6 100 300 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i error 0 wit inspect 2.6 .98 25 220 0   0   error (invalid witness file) .62 .40 7.6 39 error (invalid witness file) 6.7 3.5 100 310 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   700    9000 7300 0   0   error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.0 3.2 120 300 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   680    5800 8100 0   0   error (invalid witness file) .51 .32 9.7 39 error (invalid witness file) 7.6 4.0 120 320 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   690    9000 7700 0   0   error (invalid witness file) .64 .40 7.8 40 error (invalid witness file) 7.1 3.8 90 300 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.5 1.2  33 270 0   0   false(valid-memtrack) 5.4  2.9  60   270 unknown 20   11   310 370 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 7.3 2.0  56 420 0   0   - - false(valid-memtrack) 12    6.5  220   420 true 15   8.1 220 470
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 6.9 2.0  50 420 0   0   - - false(valid-memtrack) 14    7.3  160   420 true 14   7.8 140 480
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 6.8 2.0  54 410 0   0   - - false(valid-memtrack) 13    6.8  160   420 true 16   8.6 200 480
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.8 2.0  52 410 0   0   false(valid-memtrack) 11    5.7  140   420 true 15   8.4 270 480 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.6 1.9  57 420 0   0   false(valid-memtrack) 11    6.0  130   420 true 16   8.8 280 490 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.7 1.9  53 420 0   0   false(valid-memtrack) 14    7.0  170   430 true 15   8.4 210 480 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.6 1.9  54 410 0   0   false(valid-memtrack) 11    5.8  160   420 true 15   8.4 290 470 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.9 2.0  53 420 0   0   false(valid-memtrack) 11    5.9  130   420 true 19   10   190 480 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 28   8.1  29 310 0   0   false(valid-memtrack) 11    5.6  120   430 true 14   7.4 210 480 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.4 2.1  56 420 0   0   false(valid-memtrack) 12    6.0  130   420 true 14   7.7 270 470 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.9 2.1  55 420 0   0   false(valid-memtrack) 13    6.5  150   420 true 20   11   180 480 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.5 2.2  54 420 0   0   false(valid-memtrack) 11    5.5  86   420 true 17   9.3 170 470 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.1 2.2  50 410 0   0   false(valid-memtrack) 14    7.3  130   430 true 14   7.5 170 480 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   680    11000 7700 0   0   - - error (invalid witness file) .52 .35 8.5 40 error (invalid witness file) 5.4 2.9 110 290
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   710    8800 7300 0   0   - - error (invalid witness file) .47 .32 6.1 40 error (invalid witness file) 6.4 3.4 78 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   750    11000 6800 0   0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.2 110 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   660    7900 8200 0   0   - - error (invalid witness file) .52 .34 11   43 error (invalid witness file) 5.9 3.1 110 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   680    11000 8000 0   0   - - error (invalid witness file) .54 .35 11   42 error (invalid witness file) 6.4 3.3 110 310
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   700    9700 7500 0   0   - - error (invalid witness file) .50 .33 6.7 40 error (invalid witness file) 7.4 3.8 130 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   770    2300 4200 0   0   - - error (invalid witness file) .53 .33 8.3 40 error (invalid witness file) 6.5 3.4 120 320
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 970   150    4900 11000 0   0   - - error (invalid witness file) .58 .38 8.9 39 error (invalid witness file) 6.8 3.5 92 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   700    9000 7500 0   0   - - error (invalid witness file) .59 .37 10   40 error (invalid witness file) 6.5 3.5 85 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 950   670    8800 8300 0   0   - - error (invalid witness file) .62 .40 7.8 40 error (invalid witness file) 6.6 3.5 96 310
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   690    10000 7500 0   0   - - error (invalid witness file) .52 .34 11   39 error (invalid witness file) 6.1 3.3 93 310
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   690    10000 8000 0   0   - - error (invalid witness file) .51 .32 10   42 error (invalid witness file) 6.0 3.2 110 310
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   740    9600 6900 0   0   - - error (invalid witness file) .57 .37 10   40 error (invalid witness file) 6.4 3.4 120 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   650    7200 8800 0   0   - - error (invalid witness file) .50 .32 6.7 39 error (invalid witness file) 5.9 3.2 110 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 930   660    9200 8600 0   0   - - error (invalid witness file) .56 .37 7.9 40 error (invalid witness file) 5.7 3.1 83 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   690    11000 8300 0   0   - - error (invalid witness file) .47 .31 10   39 error (invalid witness file) 7.5 3.9 77 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   710    1700 4300 0   0   - - error (invalid witness file) .50 .31 10   40 error (invalid witness file) 5.6 3.0 67 290
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   150    4600 11000 0   0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.3 3.3 110 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   690    8000 8000 0   0   - - error (invalid witness file) .52 .35 6.1 39 error (invalid witness file) 6.2 3.3 110 300
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 3.7 1.3  27 270 0   0   false(valid-deref) 5.8  3.1  84   290 false(valid-deref) 73   63   1300 550 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 3.6 1.3  32 260 0   0   true 4.9  2.6  71   260 true 18   9.6 290 490 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 3.5 1.2  27 270 0   0   false(valid-deref) 6.1  3.3  50   260 false(valid-deref) 17   9.4 150 580 - -
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 52 -29 25000 18000   220000 220000 0   0   52 170 90 2000 6900   52 400 240 6000 11000   52 52 29 760 2200   52 200 110 2900 8700  
    correct results 19 19 130 41   760 6400 0   0   19 170 88 1900 6600   16 360 220 5400 8700   0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 19 19 130 41   760 6400 0   0   17 170 88 1900 6600   2 360 220 5400 8700   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 3 -48 21 6.1 160 1200 0   0   0 0 0 0 0   0 0 0 0 0   3 40 21 540 1200   3 45 25 550 1400  
        incorrect true 0
        incorrect false 3 -48 21 6.1 160 1200 0   0   0 0 0 0 0   0 0 0 0 0   3 40 21 540 1200   0 45 25 550 1400  
score (52 tasks, max score: 79) -29
Run set sv-comp17.MemSafety-LinkedLists