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-Arrays cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness.MemSafety-Arrays
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
array-memsafety/add_last_unsafe_false-valid-deref.i unknown 0 wit inspect .11 22 1.8 error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .0017 .28 - wit inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .15 22 1.7 timeout 0 wit inspect 91    2200 false(valid-deref) 1 wit inspect 7.9   270   true -32 wit inspect .62   18    - wit inspect
array-memsafety/count_down_unsafe_false-valid-deref.i unknown 0 wit inspect .14 23 1.7 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13 21 1.8 false(valid-deref) 1 wit inspect 3.3  250 false(valid-deref) 1 wit inspect 5.7   270   false(valid-deref) 1 wit inspect .82   18    - wit inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i unknown 0 wit inspect .15 23 1.7 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .026 4.9 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i unknown 0 wit inspect .12 23 1.6 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .0016 .35 - wit inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13 25 1.8 false(valid-deref) 1 wit inspect 1.9  240 false(valid-deref) 1 wit inspect 4.2   270   true -32 wit inspect .81   18    - wit inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 23 1.9 false(valid-deref) 1 wit inspect 3.1  250 false(valid-deref) 1 wit inspect 3.8   250   true -32 wit inspect .62   18    - wit inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i unknown 0 wit inspect .13 24 1.7 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 23 1.8 timeout (exception) 0 wit inspect 91    1900 false(valid-deref) 1 wit inspect 6.9   270   false(valid-deref) 1 wit inspect .72   18    - wit inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i unknown 0 wit inspect .11 24 1.8 error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect
array-memsafety/lis_unsafe_false-valid-deref.i unknown 0 wit inspect .12 23 1.7 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i unknown 0 wit inspect .11 24 1.8 error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i unknown 0 wit inspect .14 24 1.7 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i unknown 0 wit inspect .11 24 1.8 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .0021 .29 - wit inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .16 21 1.8 timeout (exception) 0 wit inspect 91    2100 false(valid-deref) 1 wit inspect 7.0   270   true -32 wit inspect .79   18    - wit inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 21 2.0 false(valid-deref) 1 wit inspect 3.5  240 false(valid-deref) 1 wit inspect 5.8   260   true -32 wit inspect .74   18    - wit inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 23 1.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 24 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .15 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 24 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 22 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 23 1.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .13 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .029 4.8
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .15 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .031 5.0
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 22 1.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .12 24 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .12 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 4.9
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .15 23 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .12 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .15 23 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 22 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 5.0
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .13 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 24 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 22 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .12 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .13 24 1.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 23 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .039 4.9
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .15 23 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .16 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .12 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .13 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .030 4.8
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 22 1.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .13 24 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 23 2.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .12 24 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 21 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 23 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .16 24 2.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .15 23 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 23 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .13 24 2.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 26 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .14 23 1.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect .11 22 1.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-examples/relax_false-valid-deref.i unknown 0 wit inspect .13 23 1.8 error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900    2600 5500   error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900    6000 8600   error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900    5300 9300   error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .34 - 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 7 2700    15000 24000 21 4 290 7700 21 7 42 1900 21 -158 5.1 130 48 0 1.1 230
    correct results 7 7 .96 160 13 4 4 12 980 7 7 41 1900 2 2 1.5 37 0
        correct true 0 0 0 0 0
        correct false 7 7 .96 160 13 4 4 12 980 7 7 41 1900 2 2 1.5 37 0
    incorrect results 0 0 0 5 -160 3.6 92 0
        incorrect true 0 0 0 5 -160 3.6 92 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 7 4 7 -158 0
Run set predatorhp.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness.MemSafety-Arrays