Tool Predator-HP 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] 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 21:45:44 CET 2017-12-01 22:31:23 CET 2017-12-01 22:35:27 CET 2017-12-01 22:38:24 CET 2017-12-01 22:34:17 CET
Run set predatorhp.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness.MemSafety-Other
Options --witness error-witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/predatorhp.2017-12-01_2145.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/predatorhp.2017-12-01_2145.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/predatorhp.2017-12-01_2145.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2017-12-01_2145.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    86 9600   error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .026 5.0 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 1.2  83 10   false(valid-deref) 1 wit inspect 4.9  470 unknown 0 wit inspect 5.1   230   timeout 0 wit inspect 96      19    - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect .34 41 3.8 false(valid-deref) 1 wit inspect 5.8  270 unknown 0 wit inspect 5.2   220   error (2) 0 wit inspect 1.3    19    - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 2.9  86 28   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.3   200  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 2.8  86 26   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.6   200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 62    560 670   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.3   200  
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.0  120 64   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4   200  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.1  120 62   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.4   200  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.5  130 87   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.2   200  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 10    150 97   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.8   200  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.7  46 19   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.2   200  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 2.7  64 30   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4   190  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 2.7  64 30   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.2   200  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 190    350 1800   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.0   200  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1600 8600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1300 9600   - 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 900    1100 7700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.8
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1300 9600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    950 8400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    1100 8300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900    930 8300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .78 28 9.3 - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.3   190  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.5  34 28   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4   200  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 12    60 110   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.4   190  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 20    77 190   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.9   200  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 64    140 600   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 5.0   200  
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 34 7600   11000 74000 3 2 11 780 3 0 10 450 3 0 98 38 23 0 61 3200
    correct results 18 34 400   2200 3900 2 2 11 740 0 0 0
        correct true 16 32 400   2100 3900 0 0 0 0
        correct false 2 2 1.5 120 14 2 2 11 740 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) 34 2 0 0 0
Run set predatorhp.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness.MemSafety-Other