Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 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* [apollon023; apollon077; apollon078; apollon117; apollon126] [apollon077; apollon078; apollon101; apollon157] [apollon045; apollon077; apollon078; apollon158] [apollon007; apollon009; apollon077; apollon078; apollon119]
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 09:05:19 CET 2017-12-01 09:58:48 CET 2017-12-01 10:19:41 CET 2017-12-01 10:22:00 CET 2017-12-01 10:02:39 CET
Run set depthk.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_0905.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/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_0905.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 false(valid-deref) 0 wit inspect .52 28 5.7 error 0 wit inspect 2.3  250 true -32 wit inspect 5.4   260   true -32 wit inspect .68   18    - wit inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .36 27 3.9 timeout 0 wit inspect 91    2200 true -32 wit inspect 3.9   260   false(valid-deref) 1 wit inspect .62   18    - wit inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .55 29 6.4 error 0 wit inspect 2.4  250 true -32 wit inspect 3.9   270   true -32 wit inspect .67   18    - wit inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .36 27 3.8 true -32 wit inspect 2.9  240 false(valid-deref) 1 wit inspect 3.8   260   error (2) 0 wit inspect .58   18    - wit inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .54 28 6.8 error 0 wit inspect 2.6  260 false(valid-deref) 1 wit inspect 4.6   280   false(valid-deref) 1 wit inspect .66   80    - wit inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect 1.2  28 17   error 0 wit inspect 3.4  250 true -32 wit inspect 3.7   270   error (2) 0 wit inspect .64   18    - wit inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .35 27 3.5 true -32 wit inspect 2.0  240 false(valid-deref) 1 wit inspect 3.7   260   true -32 wit inspect .58   18    - wit inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .36 27 3.9 true -32 wit inspect 3.9  250 true -32 wit inspect 5.6   260   error (2) 0 wit inspect .59   19    - wit inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .70 28 9.5 error 0 wit inspect 3.4  250 false(valid-deref) 1 wit inspect 8.3   320   false(valid-deref) 1 wit inspect .70   150    - wit inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .35 27 4.1 timeout 0 wit inspect 91    2200 false(valid-deref) 1 wit inspect 3.6   260   error (2) 0 wit inspect .59   19    - wit inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .86 29 11   error 0 wit inspect 3.7  250 true -32 wit inspect 6.0   330   false(valid-deref) 1 wit inspect .70   18    - wit inspect
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .70 28 8.5 error 0 wit inspect 2.3  250 false(valid-deref) 1 wit inspect 5.9   290   error (2) 0 wit inspect .63   18    - wit inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .66 28 8.2 error 0 wit inspect 2.4  250 true -32 wit inspect 6.8   270   false(valid-deref) 1 wit inspect .68   18    - wit inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect 1.8  28 21   error 0 wit inspect 3.7  250 true -32 wit inspect 5.3   270   true -32 wit inspect .65   18    - wit inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .60 29 7.2 error 0 wit inspect 2.4  250 true -32 wit inspect 7.2   270   true -32 wit inspect .68   18    - wit inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .36 27 3.9 timeout 0 wit inspect 92    2200 true -32 wit inspect 4.0   270   false(valid-deref) 1 wit inspect .61   18    - wit inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .36 27 3.8 true -32 wit inspect 3.1  250 false(valid-deref) 1 wit inspect 3.5   270   true -32 wit inspect .64   18    - wit inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 700    110 9600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .031 4.8
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    280 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    320 9900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    470 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    330 8100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    270 8900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.9
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    84 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .041 4.8
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 160    46 2200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 39    34 460   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 140    47 1700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    190 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 100    30 1400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    130 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 62    79 800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    960 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    140 14000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 5.0
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    140 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    170 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    190 7900   - 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 unknown 0 wit inspect 890    330 9400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    190 8200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 5.0
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 320    90 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 100    33 1300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 5.0
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 110    43 1400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 32    34 460   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 94    31 1000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .050 4.9
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 130    45 1800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    940 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    84 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 260    81 2900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.8
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 130    45 1700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    1100 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    120 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 94    29 1200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.8
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    65 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 220    120 3300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900    940 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 110    32 1500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    370 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    120 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    590 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 1.1  29 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 19     510  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    310 8200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 100    53 1400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 5.0
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    260 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    75 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    63 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900    220 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.9
array-examples/relax_false-valid-deref.i false(valid-deref) 0 wit inspect .62 29 6.3 error 0 wit inspect 2.3  250 true -32 wit inspect 7.5   290   error (2) 0 wit inspect .66   18    - wit inspect
array-examples/sanfoundry_24_false-valid-deref.i unknown 0 wit inspect 110    100 1500   error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect
array-examples/standard_strcpy_false-valid-deref_ground.i unknown 0 wit inspect 67    31 850   error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
array-examples/standard_strcpy_original_false-valid-deref.i unknown 0 wit inspect 67    30 820   error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0036 .29 - 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 13 29000   11000 360000 21 -128 320 10000 21 -345 93 5000 21 -186 12   520 48 2 20 740
    correct results 12 13 6.7 330 83 0 7 7 33 1900 6 6 4.0 300 1 2 19 510
        correct true 1 2 1.1 29 16 0 0 0 1 2 19 510
        correct false 11 11 5.6 310 67 0 7 7 33 1900 6 6 4.0 300 0
    correct-unconfimed results 7 0 5.7 200 68 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 7 0 5.7 200 68 0 0 0 0
    incorrect results 0 4 -128 12 990 11 -352 59 3000 6 -192 3.9 110 0
        incorrect true 0 4 -128 12 990 11 -352 59 3000 6 -192 3.9 110 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 13 -128 -345 -186 2
Run set depthk.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-Arrays