Tool 2LS 0.6.0 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-01 08:19:20 CET 2017-12-01 08:41:15 CET 2017-12-01 08:58:15 CET 2017-12-01 08:59:36 CET 2017-12-01 08:42:37 CET
Run set 2ls.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.MemSafety-Other
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.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/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.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 0 640    15000 3900    0 .56 43 0 .019 4.9 0 .0013 .26 -
ntdrivers/floppy_false-valid-deref.i.cil.c 0 23    110 290    0 .53 43 0 .018 4.8 0 .0011 .28 -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 0 1.1  36 13    0 .52 43 0 .024 4.9 0 .0010 .26 -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.3  420 15    - - - 2 9.1 440
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.3  420 14    - - - 2 10   440
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .51 110 4.4  - - - 2 7.5 320
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .37 73 3.1  - - - 2 7.4 310
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .34 74 3.3  - - - 2 7.3 320
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .53 140 6.4  - - - 2 8.4 370
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .52 140 5.9  - - - 2 8.6 360
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .19 27 1.4  - - - 2 6.3 270
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .24 47 3.4  - - - 2 6.7 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .29 47 2.2  - - - 2 8.2 310
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12 26 1.1  - - - 2 5.4 230
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13 25 1.1  - - - 2 4.9 230
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13 25 1.1  - - - 2 5.2 220
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 .16 26 .98 - - - 2 4.7 230
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 2 .12 28 1.2  - - - 2 4.8 230
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 .15 27 1.0  - - - 2 5.6 230
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 2 .15 26 1.1  - - - 2 4.8 230
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 .15 26 1.0  - - - 2 4.9 250
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13 23 .75 - - - 2 4.5 230
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 .14 24 .85 - - - 2 4.4 230
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 .14 24 .77 - - - 2 4.6 230
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 .14 26 .89 - - - 2 4.9 230
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13 24 1.1  - - - 2 4.7 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 670   17000 4300 3 0 1.6 130 3 0 .061 15 3 0 .0035 .81 23 46 140 6400
    correct results 23 46 7.3 1800 72 0 0 0 23 46 140 6400
        correct true 23 46 7.3 1800 72 0 0 0 23 46 140 6400
        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 2ls.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.MemSafety-Other