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-Arrays cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.MemSafety-Arrays
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
array-memsafety/add_last_unsafe_false-valid-deref.i error 0 wit inspect 2.5 220 22 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i timeout (segmentation fault) 0 wit inspect 900   12000 7400 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .038 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
array-memsafety/count_down_unsafe_false-valid-deref.i error 0 wit inspect 2.9 240 24 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .0022 .29 - wit inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.5 240 19 false(valid-deref) 1 wit inspect 2.9  240 false(valid-deref) 1 wit inspect 6.0   260   false(valid-deref) 1 wit inspect .59   18    - wit inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i error 0 wit inspect 2.5 210 24 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i error 0 wit inspect 2.8 240 27 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.5 250 21 false(valid-deref) 1 wit inspect 2.8  260 false(valid-deref) 1 wit inspect 6.4   260   true -32 wit inspect .61   18    - wit inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.5 250 21 false(valid-deref) 1 wit inspect 2.9  250 true -32 wit inspect 5.1   240   true -32 wit inspect .59   18    - wit inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i error 0 wit inspect 2.8 240 22 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
array-memsafety/diff_usafe_false-valid-deref.i segmentation fault 0 wit inspect 810   9700 7300 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i error 0 wit inspect 2.7 240 25 error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect
array-memsafety/lis_unsafe_false-valid-deref.i error 0 wit inspect 2.5 210 22 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i error 0 wit inspect 2.7 240 22 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i error 0 wit inspect 2.6 210 23 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i error 0 wit inspect 2.5 220 20 error (invalid witness file) 0 wit inspect .46 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i segmentation fault 0 wit inspect 620   7600 5900 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0036 .35 - wit inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.5 250 24 false(valid-deref) 1 wit inspect 3.2  260 false(valid-deref) 1 wit inspect 5.0   270   true -32 wit inspect .60   18    - wit inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 210 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 21 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.9
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.8 240 28 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.4 220 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.8 240 24 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 25 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 210 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 24 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 210 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 21 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 210 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 24 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 21 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 24 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 240 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 25 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.8 240 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 20 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.9 240 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.9 240 24 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 29 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 210 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 25 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 23 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.7 240 25 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 25 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.6 220 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 26 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 21 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.9 240 27 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 2.5 220 22 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-examples/relax_false-valid-deref.i error 0 wit inspect 2.8 240 24 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .028 4.8 error (invalid witness file) 0 wit inspect .0037 .30 - wit inspect
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900   5000 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect
array-examples/standard_strcpy_false-valid-deref_ground.i false(valid-deref) 1 wit inspect 2.4 250 22 false(valid-deref) 1 wit inspect 2.8  250 true -32 wit inspect 7.2   280   true -32 wit inspect .59   18    - wit inspect
array-examples/standard_strcpy_original_false-valid-deref.i false(valid-deref) 1 wit inspect 2.4 250 22 false(valid-deref) 1 wit inspect 3.5  240 true -32 wit inspect 8.1   290   true -32 wit inspect .58   18    - wit inspect
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 69 6 3400 49000 34000 21 6 27 2100 21 -93 38 1700 21 -159 3.6  110 48 0 .98 230
    correct results 6 6 15 1500 130 6 6 18 1500 3 3 17 800 1 1 .59 18 0
        correct true 0 0 0 0 0
        correct false 6 6 15 1500 130 6 6 18 1500 3 3 17 800 1 1 .59 18 0
    incorrect results 0 0 3 -96 20 810 5 -160 3.0  92 0
        incorrect true 0 0 3 -96 20 810 5 -160 3.0  92 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 6 6 -93 -159 0
Run set cpa-seq.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.MemSafety-Arrays