Tool ULTIMATE Automizer 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*
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:39:25 CET 2017-12-03 05:43:13 CET 2017-12-03 06:05:52 CET 2017-12-03 06:06:56 CET 2017-12-03 05:47:48 CET
Run set uautomizer.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-Other
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_0439.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/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2017-12-03_0439.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   4400 12000 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .019 4.8 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 41 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c unknown 0 wit inspect 4.0 230 34 error (invalid witness file) 0 wit inspect .78 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.0 480 64 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5 390
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.5 460 57 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4 390
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.1 350 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1 310
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.3 340 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3 320
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.1 340 55 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8 310
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.1 400 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9 350
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.2 400 63 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0 350
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.3 280 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4 250
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.2 320 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7 290
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.9 320 49 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4 290
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.1 240 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2 230
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.5 250 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 230
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 240 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9 230
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 250 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0 240
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 250 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8 240
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 240 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6 240
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 250 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4 240
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.5 250 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9 250
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 240 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5 230
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.0 230 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 230
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 250 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 230
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 250 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5 230
locks/test_locks_9_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 7.0 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 1000 12000 13000 3 0 1.8 130 3 0 .059 15 3 0 .0037 .80 23 46 150 6300
    correct results 23 46 120 6900 1000 0 0 0 23 46 150 6300
        correct true 23 46 120 6900 1000 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 uautomizer.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-Other