Tool ULTIMATE Taipan 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 07:53:44 CET 2017-12-03 08:20:31 CET 2017-12-03 08:37:50 CET 2017-12-03 08:38:58 CET 2017-12-03 08:21:58 CET
Run set utaipan.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.MemSafety-Other
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-03_0753.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/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2017-12-03_0753.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   1500 11000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0038 .32 - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c unknown 0 wit inspect 4.6 260 40 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .038 4.8 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c unknown 0 wit inspect 3.9 230 31 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.6 470 64 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1 390
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.7 460 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5 390
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.5 350 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0 320
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.9 350 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3 310
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.3 350 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1 310
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.3 410 60 - 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 6.6 400 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9 350
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.3 280 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2 260
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.1 320 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.9 320 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7 300
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.1 250 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 240
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 4.6 230
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 250 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 230
locks/test_locks_13_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 5.1 230
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 240 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 230
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 250 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7 230
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.7 250 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3 240
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.3 250 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 240
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 5.9 320 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7 220
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.2 250 35 - 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 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5 220
locks/test_locks_8_true-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 4.5 230
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 4.4 250 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 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 9000 12000 3 0 1.7 130 3 0 .13 14 3 0 .012 .84 23 46 140 6300
    correct results 23 46 120 7000 990 0 0 0 23 46 140 6300
        correct true 23 46 120 7000 990 0 0 0 23 46 140 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 utaipan.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.MemSafety-Other