Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-23-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-16 17:45:19 CET [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.ArraysMemSafety
Options [[ ../../results-verified/esbmc.2016-01-16_1745.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) 69     69    130 wit true 11   6.8 350 -
bubblesort_unsafe_false-valid-deref.i false(valid-deref) 800     800    12000 wit true 11   6.1 340 -
count_down_unsafe_false-valid-deref.i unknown 900     900    10000 wit - -
cstrcat_unsafe_false-valid-deref.i false(valid-deref) .77  .80 31 wit true 12   7.3 340 -
cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1.4   1.7  23 wit true 12   8.0 340 -
cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1.1   1.5  19 wit true 11   6.6 330 -
cstrncat_unsafe_false-valid-deref.i false(valid-deref) .88  .91 47 wit true 12   7.4 340 -
cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 210     210    3700 wit true 14   7.8 350 -
cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 100     100    3600 wit true 9.7 5.4 320 -
diff_usafe_false-valid-deref.i unknown 900     900    7500 wit - -
knapsack_alloca_unsafe_false-valid-deref.i out of memory 150     150    15000 wit - -
lis_unsafe_false-valid-deref.i out of memory 39     39    15000 wit - -
mult_array_unsafe_false-valid-deref.i false(valid-deref) 4.1   4.5  88 wit true 13   7.8 330 -
reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 390     390    690 wit true 14   7.9 330 -
reverse_array_unsafe_false-valid-deref.i false(valid-deref) 880     880    960 wit true 13   7.8 350 -
selectionsort_unsafe_false-valid-deref.i false(valid-deref) 65     65    5800 wit true 11   6.4 330 -
stroeder1_unsafe_false-valid-deref.i false(valid-deref) .30  .33 17 wit true 11   6.8 330 -
add_last-alloca_true-valid-memsafety.i true 120     120    150 wit - -
array01-alloca_true-valid-memsafety.i true 590     590    10000 wit - -
array02-alloca_true-valid-memsafety.i out of memory 91     90    15000 wit - -
array03-alloca_true-valid-memsafety.i true 480     480    15000 wit - -
bubblesort-alloca_true-valid-memsafety.i out of memory 84     83    15000 wit - -
count_down-alloca_true-valid-memsafety.i true 540     540    9800 wit - -
cstrcat-alloca_true-valid-memsafety.i true 15     15    62 wit - -
cstrchr-alloca_true-valid-memsafety.i true 1.5   1.5  32 wit - -
cstrcmp-alloca_true-valid-memsafety.i true 3.8   3.8  46 wit - -
cstrcpy-alloca_true-valid-memsafety.i true 1.8   1.8  45 wit - -
cstrcspn-alloca_true-valid-memsafety.i unknown 900     900    6300 wit - -
cstrlen-alloca_true-valid-memsafety.i true 1.1   1.1  21 wit - -
cstrncat-alloca_true-valid-memsafety.i true 35     35    95 wit - -
cstrncmp-alloca_true-valid-memsafety.i true 6.2   6.2  120 wit - -
cstrncpy-alloca_true-valid-memsafety.i true 80     80    4900 wit - -
cstrpbrk-alloca_true-valid-memsafety.i unknown 900     900    6300 wit - -
cstrspn-alloca_true-valid-memsafety.i unknown 900     900    6300 wit - -
diff-alloca_true-valid-memsafety.i unknown 900     900    10000 wit - -
insertionsort-alloca_true-valid-memsafety.i true 230     230    5700 wit - -
java_BubbleSort-alloca_true-valid-memsafety.i out of memory 260     260    15000 wit - -
lis-alloca_true-valid-memsafety.i out of memory 49     49    15000 wit - -
mult_array-alloca_true-valid-memsafety.i true 1.9   1.9  66 wit - -
openbsd_cbzero-alloca_true-valid-memsafety.i true .58  .59 28 wit - -
openbsd_cmemchr-alloca_true-valid-memsafety.i true 1.1   1.1  42 wit - -
openbsd_cmemrchr-alloca_true-valid-memsafety.i true 4.7   4.8  49 wit - -
openbsd_cmemset-alloca_true-valid-memsafety.i true .75  .76 26 wit - -
openbsd_cstpcpy-alloca_true-valid-memsafety.i true 1.8   1.8  42 wit - -
openbsd_cstpncpy-alloca_true-valid-memsafety.i true 80     80    4400 wit - -
openbsd_cstrcat-alloca_true-valid-memsafety.i true 15     15    62 wit - -
openbsd_cstrcmp-alloca_true-valid-memsafety.i true 4.4   4.4  82 wit - -
openbsd_cstrcpy-alloca_true-valid-memsafety.i true 1.8   1.8  42 wit - -
openbsd_cstrcspn-alloca_true-valid-memsafety.i false(valid-deref) 260     260    8400 wit - -
openbsd_cstrlcpy-alloca_true-valid-memsafety.i true 190     190    180 wit - -
openbsd_cstrlen-alloca_true-valid-memsafety.i true 1.2   1.2  22 wit - -
openbsd_cstrncat-alloca_true-valid-memsafety.i true 26     26    94 wit - -
openbsd_cstrncmp-alloca_true-valid-memsafety.i true 4.3   4.3  150 wit - -
openbsd_cstrncpy-alloca_true-valid-memsafety.i true 79     79    4400 wit - -
openbsd_cstrnlen-alloca_true-valid-memsafety.i true 1.3   1.3  25 wit - -
openbsd_cstrpbrk-alloca_true-valid-memsafety.i unknown 900     900    5800 wit - -
openbsd_cstrspn-alloca_true-valid-memsafety.i unknown .098 .11 18 wit - -
openbsd_cstrstr-alloca_true-valid-memsafety.i out of memory 51     50    15000 wit - -
rec_strlen-alloca_true-valid-memsafety.i true 1.2   1.2  26 wit - -
selectionsort-alloca_true-valid-memsafety.i unknown 900     900    9000 wit - -
stroeder1-alloca_true-valid-memsafety.i true .65  .66 25 wit - -
stroeder2-alloca_true-valid-memsafety.i true 860     860    6900 wit - -
strreplace-alloca_true-valid-memsafety.i true 1.7   1.7  57 wit - -
subseq-alloca_true-valid-memsafety.i true 81     81    140 wit - -
substring-alloca_true-valid-memsafety.i unknown 900     900    9600 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 15000 15000 280000 65 150   92   4400   65 0  
    correct results 47 6000 6000 90000 13 150   92   4400   0 0  
        correct true 34 3500 3500 63000 13 0   0   0   0 0  
        correct false 13 2500 2500 27000 0 150   92   4400   0 0  
    incorrect results 1 260 260 8400 0 0   0   0   0 0  
        incorrect true 0
        incorrect false 1 260 260 8400 0 0   0   0   0 0  
score (65 tasks, max score: 113) 65
Run set sv-comp16.ArraysMemSafety