Tool 2LS 0.5.0
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 09:48:02 CET [[ 2017-01-14 21:34:09 CET ]] [[ 2017-01-14 21:49:16 CET ]] [[ 2017-01-14 21:34:25 CET ]] [[ 2017-01-14 21:52:20 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/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.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 0 900    900    11000    10000 0      .10 .54 .34 11 41 6.5 3.4 96 310
ntdrivers/floppy_false-valid-deref.i.cil.c 1 48    48    640    1900 .012  .27 11    5.6  220 370 10   5.3 91 320
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 1 2.0  1.9  21    88 .012  .20 6.6  3.5  100 270 10   5.3 110 320
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.3  1.3  12    410 .0041 7.9  44 26   420 2300 16   8.5 160 470
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.3  1.3  14    410 .0041 12    46 26   580 2400 14   7.3 180 460
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .46 .46 4.4  100 .0041 0    190 120   2300 7000 11   5.8 180 360
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .37 .37 2.9  69 .0041 2.1  42 25   610 2700 12   6.4 150 350
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .35 .34 3.3  67 .0041 0    46 27   640 2700 12   6.3 140 350
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .51 .50 4.9  130 .0041 0    66 40   540 3300 14   7.4 120 380
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .51 .50 6.0  130 .0041 0    65 40   740 3600 11   5.9 210 400
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .20 .19 1.5  26 .0041 0    10 5.2 150 410 10   5.5 130 320
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .29 .29 2.7  44 .0041 0    22 11   350 1100 8.9 4.8 170 320
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .29 .28 2.6  44 .0041 0    22 11   310 940 11   6.0 160 340
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13 .15 1.2  32 .0041 8.0  910 810   19000 6700 9.3 4.9 110 310
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 .16 .20 1.0  36 .0041 12    840 730   18000 7000 9.3 5.0 86 310
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13 .13 .84 24 .0041 0    800 680   21000 7000 7.6 4.1 120 320
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12 .12 .95 25 .0041 0    840 730   15000 7000 9.1 4.9 87 320
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 2 .13 .13 1.2  25 .0041 0    910 800   19000 7000 8.3 4.4 120 310
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 .17 .20 1.1  33 .0041 8.0  920 820   16000 6200 7.5 4.0 140 310
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 2 .13 .13 1.1  25 .0041 0    960 880   19000 5800 8.5 4.5 130 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13 .13 1.1  25 .0041 0    920 860   22000 5600 7.4 4.0 140 310
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 .14 .16 1.0  31 .0041 7.9  910 810   25000 7000 8.8 4.7 110 320
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12 .11 .90 23 .0041 0    950 850   19000 6600 9.3 5.0 93 310
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12 .12 .93 25 .0041 0    910 830   22000 6300 6.6 3.6 140 310
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11 .11 .99 23 .0041 .16 910 840   19000 6300 9.6 5.1 94 320
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12 .12 .92 24 .0041 .16 910 830   18000 6400 8.1 4.4 120 320
../../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 48 960   960   12000 14000 .12  59    26 18 9.5 330 690   26 27 14 300 940   26 12000 11000 260000 110000   26 230 120 3100 7800  
    correct results 25 48 57   57   730 3800 .12  59    0 17 9.1 320 650   0 20 11 200 640   9 12000 11000 260000 110000   23 230 120 3100 7800  
        correct true 23 46 7.3 7.3 68 1800 .094 59    0 0 0   0 0   0 0 0 0 0   9 12000 11000 260000 110000   23 230 120 3100 7800  
        correct false 2 2 50   50   660 2000 .025 .47 0 17 9.1 320 650   0 20 11 200 640   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) 48
Run set sv-comp17.MemSafety-Other