Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.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 unknown 0 wit inspect 890    900    12000   1100 8.0  0   - - error (invalid witness file) .60 .38 8.0 41 error (invalid witness file) 6.0 3.2 110 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    7800   360 8.0  0   - - error (invalid witness file) .60 .38 10   41 error (invalid witness file) 6.2 3.3 120 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   850 11    0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 6.3 3.3 120 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   310 16    0   - - error (invalid witness file) .53 .34 10   41 error (invalid witness file) 5.9 3.2 110 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.4  1.4  16   30 3.4  0   false(valid-deref) 5.2  2.8  73   270 true 8.8 4.7 170 320 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .39 .39 4.4 29 .84 0   timeout 96    70    940   4300 true 10   5.3 160 350 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.7  4.7  13   29 4.0  0   timeout 94    79    1100   3800 true 9.8 5.2 160 350 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.7  1.7  20   38 3.4  0   timeout 95    72    880   3700 error 11   5.7 180 310 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 5.6  5.6  20   33 4.0  0   false(valid-memtrack) 6.4  3.4  62   270 true 8.6 4.6 140 320 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.3  1.3  16   29 3.4  0   false(valid-memtrack) 5.3  2.9  94   270 true 7.8 4.2 100 320 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9200   190 92    0   - - error (invalid witness file) .49 .31 13   39 error (invalid witness file) 6.0 3.2 120 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .47 .46 5.2 29 .84 0   timeout 94    78    1700   4000 true 8.8 4.7 120 350 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 44    44    350   480 13    0   error 4.7  2.5  75   270 true 8.8 4.6 110 330 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .46 .46 4.9 29 .99 0   timeout 94    75    1600   3700 true 8.4 4.5 140 340 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.0  1.0  13   29 3.4  0   timeout 94    79    910   3900 true 8.3 4.4 150 330 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.0  1.0  12   29 4.0  0   timeout 94    78    1500   3900 true 7.2 3.9 85 310 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .47 .47 5.1 29 .84 0   false(valid-memtrack) 5.6  3.0  85   270 true 8.7 4.7 150 350 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   1100 25    0   - - error (invalid witness file) .48 .31 9.9 39 error (invalid witness file) 6.3 3.4 110 300
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9900   990 25    0   - - error (invalid witness file) .50 .33 13   41 error (invalid witness file) 6.4 3.4 120 300
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   940 29    0   - - error (invalid witness file) .47 .31 8.4 39 error (invalid witness file) 6.6 3.5 130 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    9500   990 29    0   error (invalid witness file) .61 .39 8.7 39 error (invalid witness file) 6.4 3.4 110 310 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    11000   970 25    0   error (invalid witness file) .49 .31 9.2 39 error (invalid witness file) 5.9 3.2 110 290 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    10000   970 29    0   error (invalid witness file) .58 .38 8.4 41 error (invalid witness file) 6.9 3.6 130 320 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    10000   1000 27    0   error (invalid witness file) .51 .32 6.7 41 error (invalid witness file) 6.2 3.3 110 290 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    9400   1000 29    0   error (invalid witness file) .48 .31 9.4 39 error (invalid witness file) 6.8 3.6 140 310 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    9800   1200 25    0   error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.2 3.3 100 300 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    9500   1100 25    0   error (invalid witness file) .47 .30 6.7 40 error (invalid witness file) 7.0 3.6 130 310 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    900    9900   1100 25    0   error (invalid witness file) .49 .31 4.7 41 error (invalid witness file) 6.0 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    10000   1000 25    0   error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.5 3.4 88 300 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    900    3100   1100 29    0   error (invalid witness file) .72 .44 6.6 40 error (invalid witness file) 6.3 3.4 110 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9600   220 20    0   - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 6.4 3.4 130 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    2800   230 40    0   - - error (invalid witness file) .50 .31 8.9 40 error (invalid witness file) 6.0 3.2 110 290
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    8900   260 17    0   - - error (invalid witness file) .50 .32 13   39 error (invalid witness file) 6.0 3.2 120 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9100   200 97    0   - - error (invalid witness file) .49 .31 10   40 error (invalid witness file) 6.6 3.5 130 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9300   330 20    0   - - error (invalid witness file) .48 .31 9.5 39 error (invalid witness file) 6.0 3.2 98 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9000   270 17    0   - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 6.1 3.2 110 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    11000   170 34    0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.4 3.4 130 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   150 42    0   - - error (invalid witness file) .56 .36 7.6 40 error (invalid witness file) 5.9 3.2 120 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    12000   190 65    0   - - error (invalid witness file) .58 .38 8.3 40 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    8100   240 17    0   - - error (invalid witness file) .53 .35 8.2 40 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    8700   340 17    0   - - error (invalid witness file) .50 .33 13   39 error (invalid witness file) 6.3 3.3 130 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   540 62    0   - - error (invalid witness file) .56 .35 8.7 39 error (invalid witness file) 6.4 3.4 130 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    7500   230 20    0   - - error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9200   190 100    0   - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 7.5 4.0 140 310
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9800   410 20    0   - - error (invalid witness file) .49 .30 6.6 39 error (invalid witness file) 7.0 3.7 130 320
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    10000   360 17    0   - - error (invalid witness file) .51 .32 10   39 error (invalid witness file) 6.1 3.2 130 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9800   170 39    0   - - error (invalid witness file) .55 .36 12   42 error (invalid witness file) 5.8 3.1 130 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    900    13000   190 52    0   - - error (invalid witness file) .63 .42 7.2 40 error (invalid witness file) 6.0 3.2 100 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    900    9000   200 80    0   - - error (invalid witness file) .50 .32 9.9 40 error (invalid witness file) 6.8 3.5 130 310
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.5  1.5  19   36 3.5  0   false(valid-deref) 5.5  2.9  67   270 true 9.2 5.0 160 350 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 2.3  2.3  5.5 29 .84 0   timeout 96    76    1800   4000 true 8.6 4.6 110 320 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.4  1.4  16   30 4.1  0   false(valid-deref) 5.6  3.0  83   270 true 8.2 4.5 120 350 - -
../../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 15 33000 33000 350000 22000 1300 0   52 800 630 11000 34000 52 200 100 3200 8000 52 14 9.1 270 1100   52 170 90 3300 8100  
    correct results 15 15 68 67 520 910 51 0   6 790 630 11000 33000 14 130 71 2100 5000 0 0 0   0 0   0 0 0 0 0  
        correct true 0
        correct false 15 15 68 67 520 910 51 0   6 790 630 11000 33000 0 130 71 2100 5000 0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (52 tasks, max score: 79) 15
Run set sv-comp17.MemSafety-LinkedLists