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 .27 .28 27 14 8.8 330
bubblesort_unsafe_false-valid-deref.i .13 .14 24 11 7.5 340
count_down_unsafe_false-valid-deref.i .38 .39 30 14 9.4 330
cstrcat_unsafe_false-valid-deref.i .18 .19 24 11 6.6 340
cstrchr_unsafe_false-valid-deref.i .18 .19 27 23 15   480
cstrlen_unsafe_false-valid-deref.i .28 .29 28 16 9.0 340
cstrncat_unsafe_false-valid-deref.i .19 .20 25 13 7.0 340
cstrncpy_unsafe_false-valid-deref.i .12 .12 25 12 8.7 330
cstrpbrk_unsafe_false-valid-deref.i .20 .20 28 18 11   410
diff_usafe_false-valid-deref.i .17 .18 25 12 6.6 330
knapsack_alloca_unsafe_false-valid-deref.i 3.4  3.4  180 17 10   370
lis_unsafe_false-valid-deref.i .29 .31 28 16 9.5 400
mult_array_unsafe_false-valid-deref.i .33 .34 33 15 8.3 330
reverse_array_alloca_unsafe_false-valid-deref.i 1.3  1.3  75 26 14   480
reverse_array_unsafe_false-valid-deref.i 1.2  1.2  75 22 12   410
selectionsort_unsafe_false-valid-deref.i .17 .18 24 14 8.5 340
stroeder1_unsafe_false-valid-deref.i .14 .15 24 11 6.4 330
add_last-alloca_true-valid-memsafety.i 850    850    14000
array01-alloca_true-valid-memsafety.i 470    470    14000
array02-alloca_true-valid-memsafety.i 550    550    13000
array03-alloca_true-valid-memsafety.i 490    490    13000
bubblesort-alloca_true-valid-memsafety.i 560    560    13000
count_down-alloca_true-valid-memsafety.i 320    320    14000
cstrcat-alloca_true-valid-memsafety.i 140    140    15000
cstrchr-alloca_true-valid-memsafety.i 22    22    120
cstrcmp-alloca_true-valid-memsafety.i 40    40    250
cstrcpy-alloca_true-valid-memsafety.i 57    57    2500
cstrcspn-alloca_true-valid-memsafety.i 850    850    6000
cstrlen-alloca_true-valid-memsafety.i 12    12    65
cstrncat-alloca_true-valid-memsafety.i 290    290    14000
cstrncmp-alloca_true-valid-memsafety.i 180    180    580
cstrncpy-alloca_true-valid-memsafety.i 850    850    6300
cstrpbrk-alloca_true-valid-memsafety.i 850    850    6000
cstrspn-alloca_true-valid-memsafety.i 850    850    6000
diff-alloca_true-valid-memsafety.i 230    230    14000
insertionsort-alloca_true-valid-memsafety.i 370    370    15000
java_BubbleSort-alloca_true-valid-memsafety.i 560    560    13000
lis-alloca_true-valid-memsafety.i 500    500    14000
mult_array-alloca_true-valid-memsafety.i 850    850    12000
openbsd_cbzero-alloca_true-valid-memsafety.i 41    41    2300
openbsd_cmemchr-alloca_true-valid-memsafety.i 83    83    99
openbsd_cmemrchr-alloca_true-valid-memsafety.i .24 .25 28
openbsd_cmemset-alloca_true-valid-memsafety.i 41    41    2400
openbsd_cstpcpy-alloca_true-valid-memsafety.i 51    51    2500
openbsd_cstpncpy-alloca_true-valid-memsafety.i 850    850    4900
openbsd_cstrcat-alloca_true-valid-memsafety.i 140    140    15000
openbsd_cstrcmp-alloca_true-valid-memsafety.i 130    130    310
openbsd_cstrcpy-alloca_true-valid-memsafety.i 57    57    2500
openbsd_cstrcspn-alloca_true-valid-memsafety.i 850    850    350
openbsd_cstrlcpy-alloca_true-valid-memsafety.i 130    130    14000
openbsd_cstrlen-alloca_true-valid-memsafety.i 12    12    64
openbsd_cstrncat-alloca_true-valid-memsafety.i 280    280    14000
openbsd_cstrncmp-alloca_true-valid-memsafety.i 210    210    500
openbsd_cstrncpy-alloca_true-valid-memsafety.i 850    850    7900
openbsd_cstrnlen-alloca_true-valid-memsafety.i 15    15    94
openbsd_cstrpbrk-alloca_true-valid-memsafety.i 850    850    100
openbsd_cstrspn-alloca_true-valid-memsafety.i 850    850    3500
openbsd_cstrstr-alloca_true-valid-memsafety.i 850    850    8100
rec_strlen-alloca_true-valid-memsafety.i 18    18    130
selectionsort-alloca_true-valid-memsafety.i 230    230    14000
stroeder1-alloca_true-valid-memsafety.i 5.3  5.3  60
stroeder2-alloca_true-valid-memsafety.i 250    250    14000
strreplace-alloca_true-valid-memsafety.i 180    180    14000
subseq-alloca_true-valid-memsafety.i 850    850    2000
substring-alloca_true-valid-memsafety.i 850    850    800
../../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