Tool CBMC
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:48:40 CET
Run set [sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup]
Options --graphml-witness witness.graphml
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
array-memsafety/add_last_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .11  7.1 .77
array-memsafety/bubblesort_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .11  7.2 .37
array-memsafety/count_down_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .11  7.5 .99
array-memsafety/cstrcat_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .064 7.1 .58
array-memsafety/cstrchr_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .078 7.5 .95
array-memsafety/cstrlen_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .091 7.7 .60
array-memsafety/cstrncat_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .067 7.1 .61
array-memsafety/cstrncpy_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .068 8.0 .72
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .10  7.5 1.0 
array-memsafety/diff_usafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .074 7.3 .67
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .65  74   8.2 
array-memsafety/lis_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .11  7.5 .94
array-memsafety/mult_array_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .14  15   1.5 
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .28  29   3.0 
array-memsafety/reverse_array_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .24  29   2.8 
array-memsafety/selectionsort_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .065 7.1 .66
array-memsafety/stroeder1_unsafe_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .077 7.4 .33
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 710     13000   6100   
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 830     14000   8900   
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (134) 270     13000   3000   
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 190     14000   2100   
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 280     13000   3200   
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 850     14000   10000   
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 110     14000   1100   
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     2800   11000   
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     3300   11000   
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 120     13000   1200   
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     4700   10000   
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     3400   5900   
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 240     14000   2500   
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     3400   11000   
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 360     14000   3800   
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     4700   13000   
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     4700   10000   
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     12000   5000   
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 460     14000   5400   
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 270     13000   3800   
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 800     14000   8800   
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 100     14000   830   
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (6) 140     13000   1500   
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     1900   9400   
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack false(valid-deref) .079 7.2 .81
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (6) 150     13000   1500   
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 120     13000   1200   
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 360     14000   3400   
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 110     14000   1100   
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     1800   9900   
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 120     13000   1400   
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 870     310   3600   
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     8200   6000   
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     3400   4400   
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 230     14000   2400   
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     3800   9600   
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 350     14000   4200   
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     1600   9000   
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     260   7400   
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     1000   10000   
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     4700   4500   
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     5000   7500   
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 120     14000   1200   
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     2500   3900   
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 240     13000   2400   
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     11000   9300   
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     1200   4700   
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack error (42) 880     5300   9600   
array-examples/relax_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .13  7.9 .76
array-examples/sanfoundry_24_false-valid-deref.i valid-deref valid-free valid-memtrack error (42) 880     4000   7900   
array-examples/standard_strcpy_false-valid-deref_ground.i valid-deref valid-free valid-memtrack out of memory 56     15000   750   
array-examples/standard_strcpy_original_false-valid-deref.i valid-deref valid-free valid-memtrack out of memory 57     15000   720   
array-memsafety-realloc/array-realloc_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .11  8.0 1.3 
array-memsafety-realloc/array-realloc_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 10     1300   140   
memsafety/960521-1_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .84  30   11   
memsafety/test-0137_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .27  22   3.5 
memsafety/test-0235_false-valid-deref.i valid-deref valid-free valid-memtrack error (134) 58     2600   500   
memsafety/960521-1_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .91  30   11   
memsafety/test-0158_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .13  9.2 .70
memsafety/test-0232_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .12  8.1 1.2 
memsafety/20020406-1_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .15  8.9 1.9 
memsafety/20051113-1.c_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .22  7.5 3.5 
memsafety/lockfree-3.1_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 2.7   120   32   
memsafety/lockfree-3.2_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .096 7.5 1.0 
memsafety/lockfree-3.3_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 2.7   120   35   
memsafety/test-0019_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .079 8.3 .69
memsafety/test-0102_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .18  11   2.2 
memsafety/test-0158_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .060 7.0 .67
memsafety/test-0220_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .21  11   2.0 
memsafety/test-0232_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .093 6.8 1.0 
memsafety/test-0234_false-valid-memtrack.i valid-deref valid-free valid-memtrack error (134) 6.4   310   82   
memsafety/test-0235_false-valid-memtrack.i valid-deref valid-free valid-memtrack error (134) 12     580   150   
memsafety/960521-1_true-valid-memsafety.i valid-deref valid-free valid-memtrack out of memory 93     15000   1300   
memsafety/lockfree-3.0_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2000   6200   
memsafety/test-0019_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .097 6.9 .78
memsafety/test-0102_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     4400   11000   
memsafety/test-0134_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2500   8200   
memsafety/test-0158_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .091 7.1 1.1 
memsafety/test-0214_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack error (42) 880     2100   8200   
memsafety/test-0217_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack out of memory 50     13000   620   
memsafety/test-0218_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack error (42) 880     3900   11000   
memsafety/test-0219_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     920   6300   
memsafety/test-0232_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     3300   11000   
memsafety/test-0234_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1100   3900   
memsafety/test-0235_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2400   3500   
memsafety/test-0236_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1800   4400   
memsafety/test-0237_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1800   6700   
memsafety/test-0504_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1800   8200   
memsafety/test-0513_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1900   10000   
memsafety/test-0521_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     12000   9400   
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .16  6.8 1.1 
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     3800   12000   
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2500   6800   
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 870     2300   6600   
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack error (42) 880     1900   7000   
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack error (42) 880     2100   9400   
memsafety-ext/tree_of_cslls_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     9400   8900   
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack error (42) 880     1800   8500   
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i valid-deref valid-free valid-memtrack error (42) 880     1800   6400   
memsafety-ext2/split_list_test05_false-valid-deref.i valid-deref valid-free valid-memtrack error (42) 880     12000   9900   
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 12     410   130   
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 1.3   68   15   
memsafety-ext2/length_test03_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .83  20   11   
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 10     120   120   
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1500   8500   
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1800   8700   
memsafety-ext2/length_test03_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2200   9700   
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     4900   8700   
memsafety-ext2/split_list_test05_true-valid-memsafety.i valid-deref valid-free valid-memtrack error 880     11000   10000   
list-ext-properties/960521-1_1_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .10  8.7 1.1 
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-memtrack) .16  12   1.6 
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-free) .13  9.5 1.2 
list-ext-properties/960521-1_1_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .11  9.0 1.3 
list-ext-properties/test-0158_1_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .12  8.2 .61
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .096 7.7 .91
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .070 6.5 .43
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .15  7.2 1.2 
list-ext-properties/960521-1_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 36     1000   460   
list-ext-properties/list-ext_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 76     240   1000   
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 37     110   450   
list-ext-properties/simple-ext_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 32     200   410   
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .10  7.9 1.2 
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .10  6.3 .62
list-ext-properties/test-0214_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 570     490   4600   
list-ext-properties/test-0217_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 450     380   4500   
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true 2.8   37   35   
list-ext-properties/test-0504_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 3.3   59   49   
list-ext-properties/test-0513_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 4.3   140   56   
memory-alloca/c.03-alloca_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1300   8300   
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c valid-deref valid-free valid-memtrack false(valid-deref) .095 7.3 1.0 
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .069 7.7 .61
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c valid-deref valid-free valid-memtrack false(valid-deref) .075 7.8 .43
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .084 7.4 .40
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c valid-deref valid-free valid-memtrack false(valid-deref) 1.3   20   17   
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) 1.3   21   20   
ldv-memsafety/memset2_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .075 7.6 .52
ldv-memsafety/memset3_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .093 7.6 .53
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .12  8.1 .52
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .10  8.2 .56
ldv-memsafety/memsetNonZero_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .12  8.0 .53
ldv-memsafety/memset_false-valid-deref-write.c valid-deref valid-free valid-memtrack false(valid-deref) .082 8.6 .53
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c valid-deref valid-free valid-memtrack error (42) 880     4100   6200   
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true 1.3   18   17   
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c valid-deref valid-free valid-memtrack true 1.2   13   19   
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true 1.4   18   16   
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c valid-deref valid-free valid-memtrack true 6.2   67   95   
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true 1.3   13   18   
ldv-memsafety/StructInitialization1_true-valid-memsafety.c valid-deref valid-free valid-memtrack true .093 6.4 .28
ldv-memsafety/StructInitialization2_true-valid-memsafety.c valid-deref valid-free valid-memtrack true .097 6.2 .33
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true .050 7.5 .48
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true .15  6.8 .55
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true .15  7.1 .69
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true .095 7.9 .63
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true .080 7.1 .83
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true .084 7.5 .77
ldv-memsafety/memset_true-valid-memsafety_true-termination.c valid-deref valid-free valid-memtrack true .091 7.3 .63
ldv-memsafety/memleaks_test14_3_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .15  11   1.8 
ldv-memsafety/memleaks_test22_3_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .15  8.9 1.7 
ldv-memsafety/memleaks_test22_5_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .15  8.9 1.6 
ldv-memsafety/memleaks_test23_2_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) 6.6   160   80   
ldv-memsafety/memleaks_test23_4_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) 6.6   160   89   
ldv-memsafety/memleaks_test11_1_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .16  11   1.8 
ldv-memsafety/memleaks_test12_false-valid-free.i valid-deref valid-free valid-memtrack error (134) .24  13   2.7 
ldv-memsafety/memleaks_test17_2_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) 1.3   54   17   
ldv-memsafety/memleaks_test19_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .16  8.0 2.1 
ldv-memsafety/memleaks_test1_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .12  8.1 1.0 
ldv-memsafety/memleaks_test3_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .11  9.3 1.2 
ldv-memsafety/memleaks_test6_2_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .12  8.3 1.5 
ldv-memsafety/memleaks_test8_2_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .11  8.3 1.0 
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .21  10   1.8 
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .15  10   1.9 
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .10  7.6 1.1 
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .15  11   1.5 
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .13  6.8 1.0 
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .15  10   1.9 
ldv-memsafety/memleaks_test15_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .15  8.4 1.5 
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .10  6.8 1.0 
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .13  6.7 .82
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 1.9   63   25   
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 1.5   49   22   
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .16  12   2.1 
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) 1.1   38   13   
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .44  13   5.5 
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .099 6.6 .89
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .096 7.5 .90
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .095 7.5 .97
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .14  8.5 1.6 
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .12  7.3 1.3 
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .14  8.0 1.6 
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .13  7.0 1.2 
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .088 7.3 .84
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .10  6.5 1.0 
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .11  7.2 1.3 
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .11  7.0 1.2 
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .11  7.2 1.1 
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .096 7.2 .98
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .10  7.9 .99
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i valid-deref valid-free valid-memtrack false(valid-memtrack) .11  6.7 .88
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .32  12   5.1 
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .23  11   3.4 
ldv-memsafety/memleaks_test12_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .23  13   2.6 
ldv-memsafety/memleaks_test13_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .25  11   3.2 
ldv-memsafety/memleaks_test14_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .24  12   2.2 
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .31  13   4.1 
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .14  7.3 1.7 
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true 2.9   64   48   
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack out of memory 280     13000   2800   
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true 1.6   38   21   
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .18  7.4 2.5 
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .14  7.2 1.5 
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .15  7.0 1.5 
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .14  6.9 1.6 
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .22  8.1 2.5 
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .23  9.6 2.7 
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .22  9.5 2.7 
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2200   12000   
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2200   12000   
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .14  7.4 1.5 
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .16  7.3 1.7 
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .16  6.8 1.4 
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .16  7.4 1.7 
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .15  7.1 2.1 
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .17  6.7 1.8 
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .14  7.1 1.6 
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .10  6.5 1.0 
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .12  7.3 1.1 
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .18  6.9 1.3 
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .12  7.6 1.5 
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i valid-deref valid-free valid-memtrack true .15  7.5 1.4 
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .12  7.1 .75
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .088 8.1 1.1 
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .13  8.0 .92
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .10  7.9 .95
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i valid-deref valid-free valid-memtrack false(valid-free) .096 8.4 .77
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     3800   8000   
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2500   8400   
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack out of memory 310     13000   3200   
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     4500   11000   
heap-manipulation/tree_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-memtrack) .25  18   2.9 
heap-manipulation/tree_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .26  18   2.8 
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .14  10   1.7 
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .23  18   3.5 
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .23  13   2.3 
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .15  11   1.6 
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     5000   10000   
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .11  7.1 .80
list-properties/list_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .16  10   1.5 
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .083 6.7 .55
list-properties/simple_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .080 7.7 1.1 
list-properties/splice_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .12  9.0 1.3 
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 120     970   1200   
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 99     940   1000   
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 110     960   1100   
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 79     1700   870   
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 82     1700   940   
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 84     1700   860   
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 78     1700   960   
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 82     1700   820   
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 82     1700   980   
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 83     1700   830   
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 81     1700   870   
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 82     1700   870   
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) 82     1700   990   
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     680   12000   
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack out of memory 250     15000   3000   
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     3700   10000   
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     4100   13000   
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2600   7800   
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2800   6400   
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     5300   13000   
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1500   7800   
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     610   9500   
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     600   10000   
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1100   6100   
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack out of memory 220     15000   2800   
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 870     3900   11000   
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     4200   12000   
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2100   12000   
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     1300   8300   
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2400   11000   
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     2000   9200   
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     500   10000   
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-memtrack) .18  15   2.2 
forester-heap/sll-01_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .16  11   1.8 
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-memtrack) .14  11   1.7 
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .33  8.8 3.8 
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .34  8.9 3.6 
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .32  8.7 3.7 
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .35  9.5 4.8 
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .32  8.5 4.0 
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .31  8.8 4.2 
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .27  7.4 3.3 
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .29  7.2 3.3 
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .23  7.7 3.3 
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .25  7.7 2.7 
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .29  9.9 3.9 
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .32  10   3.5 
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .30  9.4 3.5 
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .32  11   4.9 
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .27  9.2 3.4 
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .28  9.7 3.7 
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .27  9.4 3.1 
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .24  6.9 2.3 
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .23  7.8 2.4 
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .24  8.3 2.7 
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .29  8.9 3.7 
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .34  9.5 4.0 
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .28  8.2 3.5 
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .31  8.7 3.7 
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .29  9.0 3.8 
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .30  9.1 4.7 
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .34  9.3 3.4 
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .27  8.3 2.7 
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .22  7.4 3.0 
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .23  7.7 2.9 
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .27  10   3.1 
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .29  10   3.3 
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .25  9.3 3.2 
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .28  10   3.4 
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .24  8.6 3.5 
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .26  9.5 3.9 
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .24  9.3 3.0 
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .19  6.7 1.9 
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .22  7.9 2.8 
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .20  8.1 2.7 
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .29  9.9 3.2 
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .21  7.3 2.3 
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .32  12   3.8 
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .26  8.8 2.7 
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 5.4   78   72   
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack true 18     230   250   
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (42) 880     4000   12000   
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i valid-deref valid-free valid-memtrack true .097 6.9 .87
list-ext3-properties/dll_circular_traversal_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .23  9.6 2.8 
list-ext3-properties/sll_circular_traversal_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) .23  9.0 2.3 
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .18  6.9 2.6 
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i valid-deref valid-free valid-memtrack false(valid-memtrack) .078 6.7 .80
loops/invert_string_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .077 7.7 .51
loop-acceleration/array3_false-valid-deref.i valid-deref valid-free valid-memtrack false(valid-deref) 14     610   180   
ntdrivers/floppy_false-valid-deref.i.cil.c valid-deref valid-free valid-memtrack false(valid-deref) 4.4   150   94   
ntdrivers/kbfiltr_false-valid-deref.i.cil.c valid-deref valid-free valid-memtrack error (134) .74  22   12   
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .93  31   10   
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .91  31   11   
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack error (42) 880     5600   3100   
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .22  9.8 2.9 
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .22  9.8 2.6 
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .47  16   7.6 
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .46  16   7.1 
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .17  6.2 1.8 
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .17  9.0 2.1 
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c valid-deref valid-free valid-memtrack true .18  8.9 2.0 
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 870     870   8100   
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     1000   9200   
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     1200   8300   
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     1400   9200   
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     460   9700   
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     1400   9300   
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     520   10000   
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     460   9000   
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     950   7600   
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     1300   9000   
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     1500   9500   
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 880     580   8600   
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c valid-deref valid-free valid-memtrack error (42) 870     710   8700   
memsafety-ext3/derefAfterFree1_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .076 7.6 .54
memsafety-ext3/derefAfterFree2_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .21  7.6 1.3 
memsafety-ext3/derefInLoop1_false-valid-deref.c valid-deref valid-free valid-memtrack true .13  6.5 .41
memsafety-ext3/getNumbers1_false-valid-deref.c valid-deref valid-free valid-memtrack true .28  8.1 1.9 
memsafety-ext3/getNumbers2_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .11  7.3 1.1 
memsafety-ext3/getNumbers4_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .16  7.0 1.7 
memsafety-ext3/naturalNumbers1_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .079 7.0 .69
memsafety-ext3/realloc1_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .19  7.6 1.9 
memsafety-ext3/scopes1_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .064 7.8 .35
memsafety-ext3/scopes2_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .057 7.4 .34
memsafety-ext3/scopes3_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .12  7.1 1.0 
memsafety-ext3/scopes4_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .066 11   .76
memsafety-ext3/scopes5_false-valid-deref.c valid-deref valid-free valid-memtrack false(valid-deref) .060 7.1 .39
memsafety-ext3/freeAlloca_false-valid-free.c valid-deref valid-free valid-memtrack false(valid-free) .24  9.0 1.5 
memsafety-ext3/getNumbers1_true-valid-memsafety.c valid-deref valid-free valid-memtrack true .10  6.6 .81
memsafety-ext3/getNumbers3_true-valid-memsafety.c valid-deref valid-free valid-memtrack true .096 6.2 .80
memsafety-ext3/getNumbers4_true-valid-memsafety.c valid-deref valid-free valid-memtrack true .16  6.5 1.8 
memsafety-ext3/scopes4_true-valid-memsafety.c valid-deref valid-free valid-memtrack true .11  6.0 .33
pthread-memsafety/fillarray1_false-valid-deref.i valid-deref valid-free valid-memtrack error (6) .096 7.7 1.3 
pthread-memsafety/fillarray_false-valid-deref.i valid-deref valid-free valid-memtrack error (6) .098 8.0 1.2 
pthread-memsafety/list1_false-valid-deref.i valid-deref valid-free valid-memtrack error (6) .11  7.8 1.3 
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i valid-memcleanup false(valid-memcleanup) .096 7.2 1.3 
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .34  26   5.1 
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .51  27   6.6 
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .55  43   7.0 
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .26  19   2.9 
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .25  18   3.1 
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .16  10   1.8 
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .12  7.6 1.2 
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .14  8.4 1.5 
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .38  16   5.5 
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .19  13   2.3 
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .18  12   2.0 
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .18  12   1.9 
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .22  14   2.0 
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .14  7.1 1.1 
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .14  7.9 1.4 
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .35  15   4.0 
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .20  12   1.7 
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .16  11   1.7 
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .16  11   1.5 
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .14  10   1.6 
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .10  7.7 1.2 
list-properties/list_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .15  10   1.6 
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .097 7.2 1.1 
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .20  8.4 2.1 
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .24  10   3.1 
list-properties/simple_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .090 7.1 .79
list-properties/splice_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .12  9.1 1.2 
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .26  12   3.2 
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .21  10   2.1 
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) .77  50   8.2 
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i valid-memcleanup false(valid-memcleanup) 16     640   200   
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 434 92000    760000 920000  
    correct results 190 1600    9700 16000  
        correct true 119 1600    8200 16000  
        correct false 71 28    1400 370  
    correct-unconfimed results 103 900    20000 10000  
        correct-unconfirmed true 0
        correct-unconfirmed false 103 900    20000 10000  
    incorrect results 8 1.4  87 13  
        incorrect true 2 .41 15 2.3
        incorrect false 6 .94 72 10  
Run set [sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup]