Tool ULTIMATE Kojak 0.1.23-3204b741 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* [apollon037; apollon054; apollon077; apollon078; apollon115] 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]
Date of execution 2017-12-03 04:40:15 CET 2017-12-03 05:43:12 CET 2017-12-03 06:07:12 CET 2017-12-03 06:08:25 CET 2017-12-03 05:47:35 CET
Run set ukojak.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-Other
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_0440.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/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_0440.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 timeout 0 wit inspect 900   5200 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .041 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c unknown 0 wit inspect 4.6 250 39 error (invalid witness file) 0 wit inspect .76 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c unknown 0 wit inspect 4.0 230 39 error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0041 .28 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 17   760 130 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8 400
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 17   760 140 - wit inspect - wit inspect - wit inspect true 2 wit inspect 10   420
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 14   770 130 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1 310
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.5 470 83 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6 310
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.7 470 78 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4 320
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   580 92 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9 360
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   550 99 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7 360
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.7 470 65 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9 260
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.7 470 82 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9 290
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 10   470 75 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 290
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.8 260 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 230
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.0 260 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3 230
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.1 270 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6 230
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.1 270 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 230
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.1 270 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4 230
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.1 270 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4 230
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.4 280 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2 240
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.5 290 48 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 240
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 250 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4 230
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.5 250 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5 230
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 250 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5 250
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.6 260 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 230
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.9 260 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 230
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 46 1100 15000 13000 3 0 2.0 120 3 0 .079 15 3 0 .0063 .80 23 46 150 6300
    correct results 23 46 180 9200 1500 0 0 0 23 46 150 6300
        correct true 23 46 180 9200 1500 0 0 0 23 46 150 6300
        correct false 0 0 0 0 0
    incorrect results 0 0 0 0 0
        incorrect true 0 0 0 0 0
        incorrect false 0 0 0 0 0
score (26 tasks, max score: 49) 46 0 0 0 46
Run set ukojak.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-Other