Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 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 23:12:01 CET 2017-12-02 00:17:27 CET 2017-12-02 00:48:14 CET 2017-12-02 00:49:56 CET 2017-12-02 00:23:19 CET
Run set map2check.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.MemSafety-Other
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_2312.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/map2check.2017-12-01_2312.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/map2check.2017-12-01_2312.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2017-12-01_2312.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 unknown 0 wit inspect 890     33 11000    error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c unknown 0 wit inspect .15  19 1.6  error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c unknown 0 wit inspect .069 15 .85 error (invalid witness file) 0 wit inspect .57 46 error (2) 0 wit inspect .020 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 unknown 0 wit inspect 900     330 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 890     330 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 900     230 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 890     170 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 890     170 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 900     220 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 900     210 8600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 310     30 3800    - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5   250  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect .047 12 .42 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect .071 12 .44 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     360 8400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 5.0
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     430 8100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     600 7200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     1000 6500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     500 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     1200 5300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     990 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     1500 6300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 5.0
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     190 7500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     230 8500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     240 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     270 9300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 900     310 8300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
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 2 19000 9700 200000 3 0 1.7 130 3 0 .058 15 3 0 .0040 .79 23 2 8.0 360
    correct results 1 2 310 30 3800 0 0 0 1 2 7.5 250
        correct true 1 2 310 30 3800 0 0 0 1 2 7.5 250
        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) 2 0 0 0 2
Run set map2check.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.MemSafety-Other