Tool CBMC
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-03 00:42:25 CET [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.ArraysMemSafety
Options --graphml-cex error-witness.graphml [[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/array-memsafety/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
add_last_unsafe_false-valid-deref.i false(valid-deref) .27 .28 27 wit false(valid-deref) 14 8.8 330 -
bubblesort_unsafe_false-valid-deref.i false(valid-deref) .13 .14 24 wit false(valid-deref) 11 7.5 340 -
count_down_unsafe_false-valid-deref.i false(valid-deref) .38 .39 30 wit false(valid-deref) 14 9.4 330 -
cstrcat_unsafe_false-valid-deref.i false(valid-deref) .18 .19 24 wit false(valid-deref) 11 6.6 340 -
cstrchr_unsafe_false-valid-deref.i false(valid-deref) .18 .19 27 wit false(valid-deref) 23 15   480 -
cstrlen_unsafe_false-valid-deref.i false(valid-deref) .28 .29 28 wit false(valid-deref) 16 9.0 340 -
cstrncat_unsafe_false-valid-deref.i false(valid-deref) .19 .20 25 wit false(valid-deref) 13 7.0 340 -
cstrncpy_unsafe_false-valid-deref.i false(valid-deref) .12 .12 25 wit false(valid-deref) 12 8.7 330 -
cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) .20 .20 28 wit false(valid-deref) 18 11   410 -
diff_usafe_false-valid-deref.i false(valid-deref) .17 .18 25 wit false(valid-deref) 12 6.6 330 -
knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 3.4  3.4  180 wit false(valid-deref) 17 10   370 -
lis_unsafe_false-valid-deref.i false(valid-deref) .29 .31 28 wit false(valid-deref) 16 9.5 400 -
mult_array_unsafe_false-valid-deref.i false(valid-deref) .33 .34 33 wit false(valid-deref) 15 8.3 330 -
reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1.3  1.3  75 wit true 26 14   480 -
reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1.2  1.2  75 wit false(valid-deref) 22 12   410 -
selectionsort_unsafe_false-valid-deref.i false(valid-deref) .17 .18 24 wit false(valid-deref) 14 8.5 340 -
stroeder1_unsafe_false-valid-deref.i false(valid-deref) .14 .15 24 wit false(valid-deref) 11 6.4 330 -
add_last-alloca_true-valid-memsafety.i true 850    850    14000 wit - -
array01-alloca_true-valid-memsafety.i true 470    470    14000 wit - -
array02-alloca_true-valid-memsafety.i true 550    550    13000 wit - -
array03-alloca_true-valid-memsafety.i true 490    490    13000 wit - -
bubblesort-alloca_true-valid-memsafety.i true 560    560    13000 wit - -
count_down-alloca_true-valid-memsafety.i true 320    320    14000 wit - -
cstrcat-alloca_true-valid-memsafety.i true 140    140    15000 wit - -
cstrchr-alloca_true-valid-memsafety.i true 22    22    120 wit - -
cstrcmp-alloca_true-valid-memsafety.i true 40    40    250 wit - -
cstrcpy-alloca_true-valid-memsafety.i true 57    57    2500 wit - -
cstrcspn-alloca_true-valid-memsafety.i true 850    850    6000 wit - -
cstrlen-alloca_true-valid-memsafety.i true 12    12    65 wit - -
cstrncat-alloca_true-valid-memsafety.i true 290    290    14000 wit - -
cstrncmp-alloca_true-valid-memsafety.i true 180    180    580 wit - -
cstrncpy-alloca_true-valid-memsafety.i true 850    850    6300 wit - -
cstrpbrk-alloca_true-valid-memsafety.i true 850    850    6000 wit - -
cstrspn-alloca_true-valid-memsafety.i true 850    850    6000 wit - -
diff-alloca_true-valid-memsafety.i true 230    230    14000 wit - -
insertionsort-alloca_true-valid-memsafety.i true 370    370    15000 wit - -
java_BubbleSort-alloca_true-valid-memsafety.i true 560    560    13000 wit - -
lis-alloca_true-valid-memsafety.i true 500    500    14000 wit - -
mult_array-alloca_true-valid-memsafety.i true 850    850    12000 wit - -
openbsd_cbzero-alloca_true-valid-memsafety.i true 41    41    2300 wit - -
openbsd_cmemchr-alloca_true-valid-memsafety.i true 83    83    99 wit - -
openbsd_cmemrchr-alloca_true-valid-memsafety.i false(valid-deref) .24 .25 28 wit - -
openbsd_cmemset-alloca_true-valid-memsafety.i true 41    41    2400 wit - -
openbsd_cstpcpy-alloca_true-valid-memsafety.i true 51    51    2500 wit - -
openbsd_cstpncpy-alloca_true-valid-memsafety.i true 850    850    4900 wit - -
openbsd_cstrcat-alloca_true-valid-memsafety.i true 140    140    15000 wit - -
openbsd_cstrcmp-alloca_true-valid-memsafety.i true 130    130    310 wit - -
openbsd_cstrcpy-alloca_true-valid-memsafety.i true 57    57    2500 wit - -
openbsd_cstrcspn-alloca_true-valid-memsafety.i true 850    850    350 wit - -
openbsd_cstrlcpy-alloca_true-valid-memsafety.i true 130    130    14000 wit - -
openbsd_cstrlen-alloca_true-valid-memsafety.i true 12    12    64 wit - -
openbsd_cstrncat-alloca_true-valid-memsafety.i true 280    280    14000 wit - -
openbsd_cstrncmp-alloca_true-valid-memsafety.i true 210    210    500 wit - -
openbsd_cstrncpy-alloca_true-valid-memsafety.i true 850    850    7900 wit - -
openbsd_cstrnlen-alloca_true-valid-memsafety.i true 15    15    94 wit - -
openbsd_cstrpbrk-alloca_true-valid-memsafety.i true 850    850    100 wit - -
openbsd_cstrspn-alloca_true-valid-memsafety.i true 850    850    3500 wit - -
openbsd_cstrstr-alloca_true-valid-memsafety.i true 850    850    8100 wit - -
rec_strlen-alloca_true-valid-memsafety.i true 18    18    130 wit - -
selectionsort-alloca_true-valid-memsafety.i true 230    230    14000 wit - -
stroeder1-alloca_true-valid-memsafety.i true 5.3  5.3  60 wit - -
stroeder2-alloca_true-valid-memsafety.i true 250    250    14000 wit - -
strreplace-alloca_true-valid-memsafety.i true 180    180    14000 wit - -
subseq-alloca_true-valid-memsafety.i true 850    850    2000 wit - -
substring-alloca_true-valid-memsafety.i true 850    850    800 wit - -
../../sv-benchmarks/c/array-memsafety/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime wit2_walltime wit2_memUsage (MB)
total tasks 65 19000    19000    330000 65 260   160   6200   65 0  
    correct results 64 19000    19000    330000 17 260   160   6200   0 0  
        correct true 47 19000    19000    330000 1 0   0   0   0 0  
        correct false 17 9.0  9.1  710 16 260   160   6200   0 0  
    incorrect results 1 .24 .25 28 0 0   0   0   0 0  
        incorrect true 0
        incorrect false 1 .24 .25 28 0 0   0   0   0 0  
score (65 tasks, max score: 113) 95
Run set sv-comp16.ArraysMemSafety