Tool Predator-HP
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 12:06:28 CET [[ 2017-01-15 02:02:31 CET ]] [[ 2017-01-15 02:04:15 CET ]] [[ 2017-01-15 02:04:05 CET ]] [[ 2017-01-15 02:06:30 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options --witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.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 true 2 wit inspect 1.5  1.1 16   50 0     1.1    - - error (invalid witness file) .74 .46 8.9 45 error (invalid witness file) 6.9 3.6 130 320
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.5  1.0 27   59 0     0      - - error (invalid witness file) .63 .39 12   42 error (invalid witness file) 6.9 3.7 83 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.6  1.0 20   69 0     .070  - - error (invalid witness file) .63 .40 12   43 error (invalid witness file) 6.9 3.6 97 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  1.1 23   72 0     0      - - error (invalid witness file) .55 .35 12   42 error (invalid witness file) 7.6 4.0 95 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 2.1  1.0 24   25 .049 .029  false(valid-deref) 5.4 3.0 110 260 true 9.9 5.3 120 320 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .15 1.0 2.1 25 .049 .061  false(valid-deref) 5.2 2.8 110 270 true 11   6.0 100 350 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .14 1.0 2.0 25 .098 0      timeout 93   77   2400 3800 true 13   7.0 210 370 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .17 1.1 1.9 23 .098 0      timeout 95   75   1300 3800 error 11   5.7 210 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .17 1.1 2.6 23 .049 0      false(valid-memtrack) 5.3 2.8 92 260 true 18   9.8 180 450 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 1.1 1.8 23 .049 0      false(valid-memtrack) 5.8 3.1 100 270 true 40   24   330 720 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    450   7100   2000 0     0      - - error (invalid witness file) .59 .40 6.7 40 error (invalid witness file) 5.7 3.0 80 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .13 1.0 1.9 24 .098 0      timeout 93   70   1900 4300 unknown 18   9.8 180 330 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .15 1.0 2.2 25 .074 0      error 6.4 3.5 66 310 true 8.1 4.3 130 320 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .13 1.0 1.9 23 .098 0      timeout 94   77   2100 4100 unknown 14   7.3 130 320 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .13 1.0 1.9 23 .098 0      timeout 93   70   2600 4100 unknown 18   9.5 190 350 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .14 1.0 1.7 23 .098 0      timeout 98   72   1300 4100 unknown 23   13   260 370 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .13 1.0 1.8 24 .049 0      timeout 94   68   2400 4300 unknown 16   8.7 250 330 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .58 1.0 5.5 52 0     .36   - - error (invalid witness file) .55 .34 12   45 error (invalid witness file) 6.6 3.5 110 290
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .55 1.1 4.8 51 0     .28   - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 7.7 4.0 110 310
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .53 1.0 4.6 52 0     .22   - - error (invalid witness file) .66 .42 9.7 41 error (invalid witness file) 6.1 3.3 110 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .49 1.1 4.6 52 .074 .13   false(valid-memtrack) 12   6.3 170 400 true 19   10   180 480 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .51 1.1 4.4 53 .074 .13   false(valid-memtrack) 10   5.4 210 400 true 16   8.7 130 480 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .52 1.0 5.2 52 .074 .20   false(valid-memtrack) 13   6.5 170 400 true 19   10   190 480 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .58 1.1 4.6 51 .074 0      false(valid-memtrack) 11   5.8 220 400 true 15   7.9 190 500 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 1.0 4.8 53 .074 1.1    false(valid-memtrack) 11   5.9 190 410 true 16   8.8 160 480 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .51 1.1 4.8 52 .074 .29   false(valid-memtrack) 11   5.7 180 400 true 15   8.0 140 480 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 1.0 4.5 53 .074 .45   false(valid-memtrack) 11   5.8 220 410 true 17   9.3 200 480 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .49 1.0 5.1 52 .074 .29   false(valid-memtrack) 11   5.9 190 410 true 17   9.4 190 490 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 1.0 4.9 53 .074 1.3    false(valid-memtrack) 11   5.8 200 410 true 14   7.6 190 470 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .58 1.1 5.4 52 .074 .36   false(valid-memtrack) 11   5.5 190 400 true 16   8.8 170 500 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  1.0 23   32 0     0      - - error (invalid witness file) .56 .37 12   43 error (invalid witness file) 7.8 4.1 85 310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  1.1 21   38 0     0      - - error (invalid witness file) .61 .37 13   44 error (invalid witness file) 6.5 3.5 100 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    300   8600   900 0     0      - - error (invalid witness file) .61 .39 9.1 40 error (invalid witness file) 6.4 3.4 120 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  1.0 22   25 0     0      - - error (invalid witness file) .72 .44 9.1 42 error (invalid witness file) 6.9 3.6 98 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    300   7500   4200 0     .0082 - - error (invalid witness file) .51 .33 13   41 error (invalid witness file) 6.9 3.7 75 290
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    300   6300   3500 0     0      - - error (invalid witness file) .65 .41 6.1 39 error (invalid witness file) 7.3 3.9 67 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  1.1 23   32 0     0      - - error (invalid witness file) .71 .43 11   45 error (invalid witness file) 7.6 4.0 88 310
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  1.0 22   38 0     0      - - error (invalid witness file) .58 .37 10   41 error (invalid witness file) 7.1 3.7 90 310
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.8  1.0 20   31 0     0      - - error (invalid witness file) .69 .44 8.6 41 error (invalid witness file) 7.7 4.1 80 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    450   10000   280 .025 0      - - error (invalid witness file) .66 .42 8.3 40 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  1.1 24   39 0     .0082 - - error (invalid witness file) .72 .45 8.5 42 error (invalid witness file) 7.7 4.0 85 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  1.0 25   38 0     0      - - error (invalid witness file) .60 .37 7.8 43 error (invalid witness file) 7.4 4.0 87 290
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    300   8100   720 0     0      - - error (invalid witness file) .64 .41 8.7 41 error (invalid witness file) 6.5 3.4 84 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  1.0 23   26 0     .93   - - error (invalid witness file) .63 .39 5.8 41 error (invalid witness file) 6.0 3.2 100 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    300   5800   3300 0     0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 8.1 4.3 75 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    300   5600   3300 0     0      - - error (invalid witness file) .60 .38 5.6 39 error (invalid witness file) 6.5 3.4 110 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  1.0 23   30 0     0      - - error (invalid witness file) .69 .44 7.9 41 error (invalid witness file) 5.9 3.1 140 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  1.1 22   37 0     0      - - error (invalid witness file) .71 .44 8.6 41 error (invalid witness file) 8.2 4.3 99 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  1.1 20   32 0     0      - - error (invalid witness file) .69 .44 9.0 45 error (invalid witness file) 6.2 3.3 120 310
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .18 1.0 2.3 23 .098 0      false(valid-deref) 6.7 3.6 89 270 timeout 97   89   1800 520 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .16 1.1 2.0 25 .098 0      false(valid-deref) 5.7 3.1 120 260 true 20   10   230 480 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .17 1.0 2.3 23 .098 .11   false(valid-deref) 5.7 3.1 110 270 false(valid-deref) 30   18   370 630 - -
../../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 63 7300   2700 60000 20000 2.0 7.5 52 820 590 17000 35000   52 510 320 6500 11000   52 17 11   260 1100   52 190 99 2700 8100  
    correct results 44 63 45   46 470 1700 1.9 7.5 17 820 590 17000 35000   18 510 320 6500 11000   0 12 7.6 190 810   0 130 70 1900 5700  
        correct true 19 38 35   20 370 800 0   2.9 0 0 0 0 0   17 0 0 0 0   0 12 7.6 190 810   0 130 70 1900 5700  
        correct false 25 25 9.4 26 100 880 1.9 4.5 17 820 590 17000 35000   1 510 320 6500 11000   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) 63
Run set sv-comp17.MemSafety-LinkedLists