Tool 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:22:21 CET 2017-12-01 08:49:28 CET 2017-12-01 09:05:52 CET 2017-12-01 09:09:01 CET 2017-12-01 08:49:44 CET
Run set cpa-seq.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.MemSafety-Other
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_0822.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/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2017-12-01_0822.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) 1 wit inspect 550   3600 6300 false(valid-deref) 1 wit inspect 15   840 timeout 0 wit inspect 96   4900 false(valid-deref) 1 wit inspect 1.1  39 - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 7.4 510 65 false(valid-deref) 1 wit inspect 8.1 460 unknown 0 wit inspect 3.0 210 timeout 0 wit inspect 96    19 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 3.9 270 36 false(valid-deref) 1 wit inspect 5.1 260 unknown 0 wit inspect 4.6 210 error (2) 0 wit inspect .96 19 - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 37   1800 240 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   380  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 31   1900 210 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8   380  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   7700 8700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 50   4000 410 - 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 46   3600 390 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6   310  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 80   4200 780 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7   350  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 80   4400 580 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   340  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 6.7 350 56 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   250  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 15   690 130 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6   290  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 14   700 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8   280  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   11000 5000 - 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 timeout 0 wit inspect 920   11000 5000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   11000 4900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   11000 4800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   10000 7100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   11000 4800 - 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 timeout 0 wit inspect 900   4500 6800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   11000 5300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   11000 4900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   11000 5300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   11000 4800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   11000 4400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout (exception) 0 wit inspect 920   11000 5000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 5.0
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 21 14000 170000 86000 3 3 28 1600 3 0 100 5300 3 1 99   77 23 18 73 3000
    correct results 12 21 920 26000 9300 3 3 28 1600 0 1 1 1.1 39 9 18 72 2900
        correct true 9 18 360 22000 2900 0 0 0 9 18 72 2900
        correct false 3 3 560 4400 6400 3 3 28 1600 0 1 1 1.1 39 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) 21 3 0 1 18
Run set cpa-seq.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.MemSafety-Other