Tool CBMC 5.8 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon077; apollon078; apollon091] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 08:19:34 CET 2017-12-01 08:48:13 CET 2017-12-01 09:05:59 CET 2017-12-01 09:09:10 CET 2017-12-01 08:49:56 CET
Run set cbmc.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-Other
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loop-acceleration/array3_false-valid-deref.i false(valid-deref) 0 wit inspect 19    1000 250   true -32 wit inspect 33    2600 out of memory 0 wit inspect 71     7000   timeout 0 wit inspect 96      67    - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 0 wit inspect 4.6  210 55   true -32 wit inspect 9.7  460 unknown 0 wit inspect 4.5   220   timeout 0 wit inspect 96      20    - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c error (6) 0 wit inspect 1.1  44 12   error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.8  42 20   - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     440  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.8  42 21   - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     450  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error (42) 0 wit inspect 880    5200 4600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .71 36 7.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0   320  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .73 36 8.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     330  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.1  38 12   - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     370  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.1  38 12   - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5   360  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .53 34 5.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0   270  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .65 36 6.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   300  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .68 36 6.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   300  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    3100 5100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    3700 6700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    4300 6200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1400 5900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1800 7300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1600 6000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    2000 9300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .031 4.8
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1800 6400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1300 5800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1500 6100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    1700 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    2100 7300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 0 wit inspect 870    2600 7800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 26 18 12000   36000 91000 3 -64 43 3100 3 0 76 7200 3 0 190 87 23 18 93 3200
    correct results 9 18 9.1 340 99 0 0 0 9 18 93 3100
        correct true 9 18 9.1 340 99 0 0 0 9 18 93 3100
        correct false 0 0 0 0 0
    correct-unconfimed results 2 0 24   1200 310 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 2 0 24   1200 310 0 0 0 0
    incorrect results 0 2 -64 42 3100 0 0 0
        incorrect true 0 2 -64 42 3100 0 0 0
        incorrect false 0 0 0 0 0
score (26 tasks, max score: 49) 18 -64 0 0 18
Run set cbmc.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-Other