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-Other
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)
loop-acceleration/array3_false-valid-deref.i 0 900    900   11000   89 .037 0      .70 .44 7.6 40 6.5 3.5 80 300
ntdrivers/floppy_false-valid-deref.i.cil.c 1 1.2  1.1 9.9 84 .025 .13   13    6.5  190   420 9.6 5.0 91 320
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 1 .36 1.1 3.1 40 .049 0      7.3  3.9  140   280 8.7 4.6 92 310
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 2.8  1.0 29   86 0     0      .67 .41 12   44 8.6 4.5 65 300
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 2.8  1.1 27   86 0     0      .75 .46 9.0 43 6.3 3.3 120 300
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 62    30   670   550 0     0      .66 .41 9.7 42 7.4 3.9 82 300
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 6.8  2.0 69   120 0     0      .72 .45 8.8 43 6.9 3.7 120 310
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 9.9  3.0 87   120 0     0      .55 .34 13   43 7.6 4.1 74 290
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 9.3  3.0 91   140 0     8.3    .56 .36 8.8 43 7.8 4.1 120 320
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 10    3.0 88   150 0     0      .67 .42 9.8 43 6.9 3.6 120 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.7  1.1 19   41 0     0      .57 .37 13   42 5.5 2.9 84 290
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 2.7  1.0 27   64 0     .26   .54 .34 13   42 5.9 3.2 90 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 2.7  1.0 25   64 0     .14   .56 .36 13   41 5.9 3.2 120 310
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 190    48   1800   350 0     .029  .54 .35 10   42 7.0 3.7 80 300
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 890    220   7900   1600 0     0      .60 .37 10   41 7.1 3.7 74 290
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 900    220   8500   1300 0     0      .53 .35 7.7 40 6.8 3.6 79 290
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 900    220   8300   1200 0     0      .61 .39 7.2 40 6.4 3.4 94 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 0 900    230   8100   1200 0     0      .57 .38 10   40 6.8 3.6 90 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 900    220   9100   990 0     .0082 .48 .31 8.5 40 7.4 4.0 72 300
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 0 900    230   8000   1200 0     .098  .68 .43 7.9 41 6.4 3.4 88 290
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 900    220   9000   890 0     .098  .52 .33 12   40 8.0 4.2 72 300
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 .83 1.1 8.1 28 0     .0082 .52 .34 8.1 41 8.3 4.3 70 320
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 3.3  1.1 36   36 0     .0082 .64 .40 7.9 44 6.0 3.2 120 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 7.9  2.0 81   55 0     0      .66 .41 8.5 44 5.7 3.0 120 300
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 20    5.1 180   77 0     0      .58 .37 10   43 8.3 4.3 99 310
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 52    13   460   120 0     .85   .66 .43 8.9 44 7.0 3.7 80 300
../../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 36 7600   2600   74000 11000 .11  10    26 21 11 340 740   26 25 13   260 930   26 14 8.8 230 960   26 160 84 2100 6900  
    correct results 19 36 1300   340   12000 3800 .074 9.8  2 20 10 330 700   0 18 9.6 180 630   0 10 6.6 170 720   0 120 62 1600 5100  
        correct true 17 34 1300   340   12000 3700 0     9.6  0 0 0 0 0   0 0 0   0 0   0 10 6.6 170 720   0 120 62 1600 5100  
        correct false 2 2 1.5 2.1 13 120 .074 .13 2 20 10 330 700   0 18 9.6 180 630   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) 36
Run set sv-comp17.MemSafety-Other