Tool CPAchecker 1.4-svcomp16c
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-04 13:17:38 CET [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.ArraysMemSafety
Options -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ ../../results-verified/cpa-seq.2016-01-04_1317.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 3.7 1.5 170
bubblesort_unsafe_false-valid-deref.i 900   210   10000
count_down_unsafe_false-valid-deref.i 3.7 1.5 170
cstrcat_unsafe_false-valid-deref.i 3.1 1.4 160 13 8.2 320
cstrchr_unsafe_false-valid-deref.i 3.1 1.3 170
cstrlen_unsafe_false-valid-deref.i 3.7 1.5 170
cstrncat_unsafe_false-valid-deref.i 2.6 1.2 170 13 10   330
cstrncpy_unsafe_false-valid-deref.i 2.8 1.2 160 13 7.5 330
cstrpbrk_unsafe_false-valid-deref.i 3.0 1.3 170
diff_usafe_false-valid-deref.i 2.6 1.2 170 15 9.9 350
knapsack_alloca_unsafe_false-valid-deref.i 3.2 1.4 170
lis_unsafe_false-valid-deref.i 3.9 1.6 170
mult_array_unsafe_false-valid-deref.i 3.7 1.5 180
reverse_array_alloca_unsafe_false-valid-deref.i 3.8 1.6 170
reverse_array_unsafe_false-valid-deref.i 3.1 1.4 170
selectionsort_unsafe_false-valid-deref.i 3.2 1.4 180 16 8.8 360
stroeder1_unsafe_false-valid-deref.i 3.2 1.4 160 13 7.1 330
add_last-alloca_true-valid-memsafety.i 3.9 1.6 170
array01-alloca_true-valid-memsafety.i 3.9 1.6 170
array02-alloca_true-valid-memsafety.i 3.8 1.6 170
array03-alloca_true-valid-memsafety.i 3.7 1.5 180
bubblesort-alloca_true-valid-memsafety.i 3.8 1.6 180
count_down-alloca_true-valid-memsafety.i 3.9 1.6 180
cstrcat-alloca_true-valid-memsafety.i 3.7 1.6 170
cstrchr-alloca_true-valid-memsafety.i 3.7 1.6 170
cstrcmp-alloca_true-valid-memsafety.i 3.8 1.6 170
cstrcpy-alloca_true-valid-memsafety.i 3.1 1.3 170
cstrcspn-alloca_true-valid-memsafety.i 3.1 1.3 170
cstrlen-alloca_true-valid-memsafety.i 3.3 1.4 170
cstrncat-alloca_true-valid-memsafety.i 3.7 1.6 170
cstrncmp-alloca_true-valid-memsafety.i 4.1 1.6 170
cstrncpy-alloca_true-valid-memsafety.i 3.0 1.3 170
cstrpbrk-alloca_true-valid-memsafety.i 3.3 1.3 170
cstrspn-alloca_true-valid-memsafety.i 3.3 1.3 170
diff-alloca_true-valid-memsafety.i 3.9 1.6 170
insertionsort-alloca_true-valid-memsafety.i 3.8 1.6 170
java_BubbleSort-alloca_true-valid-memsafety.i 3.7 1.6 170
lis-alloca_true-valid-memsafety.i 4.0 1.6 170
mult_array-alloca_true-valid-memsafety.i 3.8 1.6 170
openbsd_cbzero-alloca_true-valid-memsafety.i 3.8 1.5 170
openbsd_cmemchr-alloca_true-valid-memsafety.i 3.7 1.6 180
openbsd_cmemrchr-alloca_true-valid-memsafety.i 3.7 1.6 170
openbsd_cmemset-alloca_true-valid-memsafety.i 3.2 1.3 170
openbsd_cstpcpy-alloca_true-valid-memsafety.i 3.8 1.6 170
openbsd_cstpncpy-alloca_true-valid-memsafety.i 3.2 1.4 170
openbsd_cstrcat-alloca_true-valid-memsafety.i 3.7 1.5 170
openbsd_cstrcmp-alloca_true-valid-memsafety.i 3.9 1.5 170
openbsd_cstrcpy-alloca_true-valid-memsafety.i 3.8 1.6 170
openbsd_cstrcspn-alloca_true-valid-memsafety.i 3.1 1.3 170
openbsd_cstrlcpy-alloca_true-valid-memsafety.i 3.8 1.6 170
openbsd_cstrlen-alloca_true-valid-memsafety.i 3.1 1.3 170
openbsd_cstrncat-alloca_true-valid-memsafety.i 3.3 1.4 170
openbsd_cstrncmp-alloca_true-valid-memsafety.i 4.0 1.6 170
openbsd_cstrncpy-alloca_true-valid-memsafety.i 2.9 1.2 180
openbsd_cstrnlen-alloca_true-valid-memsafety.i 3.6 1.5 170
openbsd_cstrpbrk-alloca_true-valid-memsafety.i 3.3 1.3 170
openbsd_cstrspn-alloca_true-valid-memsafety.i 3.7 1.6 170
openbsd_cstrstr-alloca_true-valid-memsafety.i 3.7 1.6 170
rec_strlen-alloca_true-valid-memsafety.i 3.2 1.3 170
selectionsort-alloca_true-valid-memsafety.i 3.8 1.6 170
stroeder1-alloca_true-valid-memsafety.i 3.8 1.5 170
stroeder2-alloca_true-valid-memsafety.i 3.8 1.6 170
strreplace-alloca_true-valid-memsafety.i 3.9 1.6 180
subseq-alloca_true-valid-memsafety.i 3.7 1.6 170
substring-alloca_true-valid-memsafety.i 3.7 1.6 180
../../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 1100 310   21000 65 82 52 2000 65 0  
    correct results 6 17 7.9 1000 6 82 52 2000 0 0  
        correct true 0
        correct false 6 17 7.9 1000 5 82 52 2000 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (65 tasks, max score: 113) 6
Run set sv-comp16.ArraysMemSafety