Tool CBMC 5.6
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-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]]
Run set sv-comp17.MemSafety-Other
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.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)
loop-acceleration/array3_false-valid-deref.i false(valid-deref) 1 wit inspect 23    23    290   930 20      0      timeout 94    59    1600   4300 out of memory 81   51   1400 7000 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 3.5  3.5  34   200 .012  .23   error 12    6.0  180   380 unknown 7.4 3.9 140 300 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c error (1) 0 wit inspect .68 .67 7.7 35 .012  0      error (invalid witness file) .64 .42 6.8 39 error (invalid witness file) 6.9 3.6 140 300 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.1  1.1  11   38 .0082 0      - - true 37    21    510   2500 true 20   11   320 460
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.1  1.1  12   38 .0082 .16   - - true 35    20    400   2300 true 19   11   240 470
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error (42) 0 wit inspect 850    850    3700   7400 6.1    0      - - error (invalid witness file) .51 .33 6.9 39 error (invalid witness file) 7.2 3.8 77 290
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .37 .36 4.0 20 .0082 0      - - true 45    27    760   2600 true 12   6.3 190 440
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .36 .36 3.8 21 .0082 0      - - true 45    27    440   2700 true 11   6.1 190 430
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .61 .61 6.8 22 .0082 0      - - true 82    52    1300   3500 true 15   7.8 240 470
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .62 .61 6.4 22 .0082 0      - - true 76    47    1100   3500 true 14   7.7 210 470
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .25 .25 2.9 18 .0082 0      - - true 9.8  5.1  140   400 true 9.2 4.9 180 330
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .34 .33 3.1 20 .0082 0      - - true 23    12    170   1000 true 12   6.2 200 390
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .32 .31 3.2 20 .0082 0      - - true 20    10    250   1000 true 13   6.8 140 390
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6100   3100 15      0      - - error (invalid witness file) .56 .35 11   39 error (invalid witness file) 6.2 3.3 100 300
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    5000   3700 16      0      - - error (invalid witness file) .64 .40 8.9 40 error (invalid witness file) 6.0 3.2 110 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    8000   4300 18      0      - - error (invalid witness file) .54 .34 10   40 error (invalid witness file) 7.2 3.8 85 310
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    7000   2000 20      0      - - error (invalid witness file) .51 .33 9.7 40 error (invalid witness file) 6.5 3.4 120 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6900   1800 8.9    0      - - error (invalid witness file) .47 .30 7.2 39 error (invalid witness file) 7.4 3.9 79 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    7700   1500 21      0      - - error (invalid witness file) .51 .33 5.5 39 error (invalid witness file) 6.7 3.5 110 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6800   2000 9.5    0      - - error (invalid witness file) .66 .41 9.5 43 error (invalid witness file) 5.9 3.1 110 300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6400   1800 22      12      - - error (invalid witness file) .49 .31 9.4 39 error (invalid witness file) 6.5 3.4 130 310
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6100   5500 20      0      - - error (invalid witness file) .52 .33 14   39 error (invalid witness file) 5.8 3.1 110 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    5700   1300 22      .0041 - - error (invalid witness file) .48 .31 9.1 39 error (invalid witness file) 7.0 3.6 98 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    6000   1700 11      0      - - error (invalid witness file) .61 .39 7.7 39 error (invalid witness file) 6.3 3.4 100 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    5300   2000 12      0      - - error (invalid witness file) .49 .32 7.0 40 error (invalid witness file) 7.3 3.8 90 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 850    850    5000   2600 13      0      - - error (invalid witness file) .49 .33 9.6 40 error (invalid witness file) 6.0 3.2 82 290
../../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 26 20 12000   12000   86000 42000 230     13    26 110 65 1800 4700   26 96 59 1600 7600   26 380 230 5100 20000   26 220 120 3300 8000  
    correct results 11 20 31   31   380 1300 20     .39 0 110 65 1800 4600   0 89 55 1500 7300   9 370 220 5000 20000   9 130 67 1900 3900  
        correct true 9 18 5.0 5.0 53 220 .074 .16 0 0 0 0 0   0 0 0 0 0   9 370 220 5000 20000   9 130 67 1900 3900  
        correct false 2 2 26   26   320 1100 20     .23 0 110 65 1800 4600   0 89 55 1500 7300   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 (26 tasks, max score: 49) 20
Run set sv-comp17.MemSafety-Other