Tool CBMC 5.8
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 08:19:34 CET
Run set [sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other]
Options --graphml-witness witness.graphml
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) .48 37 4.2
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) .25 33 2.0
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) .49 36 4.4
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) .26 33 2.3
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) .45 36 4.3
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) .46 36 4.4
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) .24 33 2.0
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) .25 35 2.3
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) .47 36 4.2
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) .27 33 2.4
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1.1  93 10  
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) .48 36 4.4
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) .54 38 5.1
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) .65 47 6.8
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) .69 47 5.9
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) .24 33 2.1
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) .24 33 2.5
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i error (42) 880    13000 3400  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i error (134) 130    13000 1200  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i error (134) 480    13000 3200  
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i error (134) 160    13000 1500  
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i error (42) 870    5200 4300  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i error (134) 160    13000 1300  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i error (134) 91    14000 950  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i error (42) 870    3800 7300  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i error (42) 870    1900 8700  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) 96    13000 980  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i error (42) 870    7000 7600  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i error (42) 870    4100 4700  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) 260    14000 1700  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i error (42) 870    2000 8900  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) 260    14000 2600  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (42) 870    7300 6900  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i error (42) 870    7500 6000  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i error (42) 880    11000 4700  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i error (42) 880    12000 4200  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i error (42) 870    5200 5500  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i error (42) 870    2500 5600  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i error (134) 73    13000 830  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i error (134) 83    13000 990  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i error (42) 870    1300 5400  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i false(valid-deref) .47 36 3.4
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i error (134) 82    13000 850  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i error (134) 91    13000 1000  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i error (134) 240    14000 2600  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i error (134) 89    14000 910  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i error (42) 870    2200 8400  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) 94    13000 1200  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i error (42) 870    430 4000  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i error (42) 880    8200 4500  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i error (42) 870    4300 6100  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) 250    14000 2100  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i error (42) 870    1700 7200  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) 230    14000 2300  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i error (42) 870    2000 5700  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (42) 870    280 5100  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i error (42) 870    2600 10000  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i error (42) 870    4000 6200  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i error (42) 870    9400 5000  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i error (134) 72    14000 750  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i error (42) 870    2400 3600  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i error (134) 220    13000 2100  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i error (42) 880    12000 4200  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i error (42) 870    1200 5300  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i error (42) 870    7800 6500  
array-examples/relax_false-valid-deref.i false(valid-deref) .49 37 4.4
array-examples/sanfoundry_24_false-valid-deref.i error (42) 870    6100 5300  
array-examples/standard_strcpy_false-valid-deref_ground.i out of memory 67    15000 980  
array-examples/standard_strcpy_original_false-valid-deref.i out of memory 67    15000 980  
memsafety/960521-1_false-valid-deref.i false(valid-deref) 6.2  48 57  
memsafety/test-0137_false-valid-deref.i false(valid-deref) .69 44 5.8
memsafety/test-0235_false-valid-deref.i false(valid-deref) 23    790 230  
memsafety/960521-1_false-valid-free.i false(valid-free) 5.9  48 66  
memsafety/test-0158_false-valid-free.i false(valid-free) .48 36 4.4
memsafety/test-0232_false-valid-free.i witness invalid (false(valid-free)) .53 37 4.6
memsafety/20020406-1_false-valid-memtrack.i false(unreach-call) .60 38 5.1
memsafety/20051113-1.c_false-valid-memtrack.i false(unreach-call) 1.3  36 16  
memsafety/lockfree-3.1_false-valid-memtrack.i false(unreach-call) 5.1  140 58  
memsafety/lockfree-3.2_false-valid-memtrack.i false(unreach-call) .46 36 5.0
memsafety/lockfree-3.3_false-valid-memtrack.i false(unreach-call) 5.1  150 49  
memsafety/test-0019_false-valid-memtrack_true-termination.i false(unreach-call) .45 36 4.4
memsafety/test-0102_false-valid-memtrack.i false(unreach-call) .58 36 6.3
memsafety/test-0158_false-valid-memtrack_true-termination.i false(unreach-call) .47 36 4.0
memsafety/test-0220_false-valid-memtrack.i false(unreach-call) .60 38 5.9
memsafety/test-0232_false-valid-memtrack.i false(unreach-call) .51 36 4.2
memsafety/test-0234_false-valid-memtrack.i false(unreach-call) 7.8  270 84  
memsafety/test-0235_false-valid-memtrack.i false(unreach-call) 13    460 150  
memsafety/960521-1_true-valid-memsafety.i out of memory 120    15000 1700  
memsafety/lockfree-3.0_true-valid-memsafety.i error (42) 870    2200 5200  
memsafety/test-0019_true-valid-memsafety_true-termination.i true .88 37 7.7
memsafety/test-0102_true-valid-memsafety.i error (42) 870    2400 7000  
memsafety/test-0134_true-valid-memsafety.i error (42) 870    990 6900  
memsafety/test-0158_true-valid-memsafety_true-termination.i true .81 36 8.7
memsafety/test-0214_true-valid-memsafety_false-termination.i error (42) 870    1800 4500  
memsafety/test-0217_true-valid-memsafety_false-termination.i error (134) 46    13000 550  
memsafety/test-0218_true-valid-memsafety_false-termination.i error (42) 870    3700 6200  
memsafety/test-0219_true-valid-memsafety.i error (42) 870    1500 7300  
memsafety/test-0232_true-valid-memsafety.i error (42) 870    2200 6900  
memsafety/test-0234_true-valid-memsafety.i error (42) 870    1300 7000  
memsafety/test-0235_true-valid-memsafety.i error (42) 870    970 6500  
memsafety/test-0236_true-valid-memsafety.i error (42) 870    1400 6400  
memsafety/test-0237_true-valid-memsafety.i error (42) 870    1400 6500  
memsafety/test-0504_true-valid-memsafety.i error (42) 870    2100 6700  
memsafety/test-0513_true-valid-memsafety.i error (42) 870    1900 7500  
memsafety/test-0521_true-valid-memsafety.i error (134) 380    12000 3200  
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i true .88 36 8.1
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i error (42) 870    4100 5500  
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i error (42) 870    420 7300  
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i error (42) 870    620 7100  
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i error (42) 870    2100 5400  
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i error (42) 870    1700 5200  
memsafety-ext/tree_of_cslls_true-valid-memsafety.i error (42) 870    1200 8800  
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i error (42) 870    2100 5500  
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i error (42) 870    1500 6000  
memsafety-ext2/split_list_test05_false-valid-deref.i out of memory 370    15000 4400  
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i false(unreach-call) 22    630 250  
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i false(unreach-call) 3.1  110 35  
memsafety-ext2/length_test03_false-valid-memtrack.i false(unreach-call) 3.1  43 36  
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(unreach-call) 19    280 260  
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i error (42) 870    2500 8200  
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i error (42) 870    1300 8800  
memsafety-ext2/length_test03_true-valid-memsafety.i error (42) 870    2000 4000  
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i error (134) 440    13000 4800  
memsafety-ext2/split_list_test05_true-valid-memsafety.i out of memory 250    15000 3700  
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) .46 36 4.7
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 110    380 1300  
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) .49 36 5.4
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) .49 36 4.4
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) .44 36 4.1
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i false(unreach-call) .46 36 4.2
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i false(unreach-call) .47 36 3.7
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i false(unreach-call) .51 36 4.4
list-ext-properties/960521-1_1_true-valid-memsafety.i true 35    1200 400  
list-ext-properties/list-ext_1_true-valid-memsafety.i true 110    290 1100  
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 48    140 620  
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 52    270 650  
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i true .84 36 11  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i true .83 36 7.3
list-ext-properties/test-0214_1_true-valid-memsafety.i true 610    480 5700  
list-ext-properties/test-0217_1_true-valid-memsafety.i true 510    400 3900  
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i true 9.1  62 120  
list-ext-properties/test-0504_1_true-valid-memsafety.i true 5.6  80 78  
list-ext-properties/test-0513_1_true-valid-memsafety.i true 11    290 130  
memory-alloca/c.03-alloca_true-valid-memsafety.i error (42) 870    1800 4900  
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) .25 33 2.2
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) .27 33 2.1
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) .26 33 2.1
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) .27 33 2.0
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 3.6  34 42  
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 3.6  34 35  
ldv-memsafety/memset2_false-valid-deref-write.c witness invalid (false(valid-deref)) .45 34 4.0
ldv-memsafety/memset3_false-valid-deref-write.c witness invalid (false(valid-deref)) .41 34 4.6
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c witness invalid (false(valid-deref)) .46 34 4.0
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c witness invalid (false(valid-deref)) .43 34 4.3
ldv-memsafety/memsetNonZero_false-valid-deref-write.c witness invalid (false(valid-deref)) .43 34 4.6
ldv-memsafety/memset_false-valid-deref-write.c witness invalid (false(valid-deref)) .42 34 4.3
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c error (42) 870    5300 5400  
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c true 3.9  34 43  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 4.1  33 59  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c true 3.9  35 42  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 13    80 160  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c true 3.7  35 38  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true .44 33 3.9
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true .44 33 3.4
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c true .44 33 4.1
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c true .81 35 8.9
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c true .80 34 7.4
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c true .82 35 7.5
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c true .85 34 7.5
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c true .84 34 7.6
ldv-memsafety/memset_true-valid-memsafety_true-termination.c true .81 34 6.5
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) .53 37 6.5
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) .55 37 4.8
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) .54 37 5.5
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 11    220 160  
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 11    220 110  
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) .56 37 4.9
ldv-memsafety/memleaks_test12_false-valid-free.i error (6) .67 38 6.9
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 3.2  65 33  
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) .54 37 5.1
ldv-memsafety/memleaks_test1_false-valid-free.i false(valid-free) .50 37 4.0
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) .49 37 4.2
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) .49 37 5.4
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) .47 37 5.3
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i false(unreach-call) .53 37 6.8
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i false(unreach-call) .55 37 5.6
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i false(unreach-call) .49 37 4.5
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(unreach-call) .57 39 5.6
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i false(unreach-call) .49 37 4.3
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(unreach-call) .58 38 5.4
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(unreach-call) .54 37 5.7
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i false(unreach-call) .49 37 4.1
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i false(unreach-call) .47 37 4.5
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(unreach-call) 3.6  72 47  
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(unreach-call) 3.4  65 35  
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i false(unreach-call) .54 37 5.1
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i false(unreach-call) 3.0  53 32  
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i false(unreach-call) 2.4  38 33  
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i false(unreach-call) .50 37 4.0
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i false(unreach-call) .47 37 4.5
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i false(unreach-call) .50 37 3.7
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i false(unreach-call) .54 37 6.0
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i false(unreach-call) .55 37 5.1
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i false(unreach-call) .53 38 5.1
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i false(unreach-call) .52 37 4.8
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i false(unreach-call) .47 37 4.4
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i false(unreach-call) .49 37 4.2
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i false(unreach-call) .54 37 4.9
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i false(unreach-call) .49 38 5.0
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i false(unreach-call) .51 37 4.3
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i false(unreach-call) .51 37 4.1
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i false(unreach-call) .51 37 4.4
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i false(unreach-call) .49 37 4.5
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i true 1.1  38 11  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i true 1.1  39 9.2
ldv-memsafety/memleaks_test12_true-valid-memsafety.i error (6) .63 37 7.7
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 1.0  37 9.3
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 1.0  39 11  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i true 1.1  41 12  
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i true .93 37 8.4
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i true 5.0  71 53  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i error (134) 280    14000 1800  
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i true 3.8  53 43  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i true .99 38 9.4
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i true .91 37 8.4
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i true .89 37 9.5
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i true .90 37 8.6
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i true .97 37 12  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i true 1.0  38 8.9
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i true 1.0  37 12  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i error (42) 870    10000 8200  
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i error (42) 870    10000 8400  
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i true .90 37 9.5
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i true .91 37 9.6
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i true .90 37 9.5
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i true .93 37 8.2
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i true .94 37 8.7
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i true .91 37 8.9
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i true .97 37 8.9
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i true .80 34 9.0
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i true .79 35 8.4
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i true .85 36 6.6
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i true .85 35 8.0
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i true .86 34 8.6
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) .45 34 3.6
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i witness invalid (false(valid-deref)) .46 35 3.9
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i witness invalid (false(valid-deref)) .46 35 3.7
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i witness invalid (false(valid-deref)) .47 35 3.8
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i witness invalid (false(valid-free)) .44 34 4.4
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (42) 870    720 8500  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 870    3300 8700  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 440    13000 4700  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 870    4300 5500  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) .75 46 7.7
heap-manipulation/tree_false-valid-deref.i false(valid-deref) .76 47 8.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(unreach-call) .56 36 4.8
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) .70 44 7.1
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) .59 39 5.6
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) .56 36 5.3
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 870    4400 6200  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(unreach-call) .48 37 5.6
list-properties/list_true-unreach-call_false-valid-memtrack.i false(unreach-call) .56 38 5.0
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(unreach-call) .45 36 4.3
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(unreach-call) .51 36 4.4
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(unreach-call) .54 37 4.7
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 71    920 740  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 58    910 730  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 64    910 690  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 50    1100 540  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(unreach-call) 50    1100 550  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 49    1100 600  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(unreach-call) 50    1100 550  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 51    1100 510  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 51    1100 560  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 49    1100 540  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(unreach-call) 50    1100 530  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 49    1100 650  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(unreach-call) 51    1100 610  
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (42) 880    3800 9700  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 420    15000 4400  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (42) 870    5200 5500  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (42) 870    2200 4600  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 870    3100 5800  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 870    3300 5000  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (42) 870    5400 6400  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 870    1000 7500  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (42) 870    970 9600  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (42) 870    700 10000  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (42) 870    970 7600  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 410    15000 4900  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (42) 880    4800 6500  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (42) 870    1900 7000  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 870    2100 5200  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 870    2300 7100  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (42) 870    2400 4700  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 870    800 7600  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (42) 870    970 9000  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) .67 42 6.5
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) .57 36 5.1
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) .59 37 5.1
loop-acceleration/array3_false-valid-deref.i false(valid-deref) 19    1000 250  
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 4.6  210 55  
ntdrivers/kbfiltr_false-valid-deref.i.cil.c error (6) 1.1  44 12  
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.8  42 20  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.8  42 21  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error (42) 880    5200 4600  
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .71 36 7.6
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .73 36 8.5
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.1  38 12  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.1  38 12  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .53 34 5.3
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .65 36 6.4
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .68 36 6.0
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    3100 5100  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    3700 6700  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    4300 6200  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    1400 5900  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    1800 7300  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    1600 6000  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    2000 9300  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    1800 6400  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    1300 5800  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    1500 6100  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    1700 5500  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    2100 7300  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c error (42) 870    2600 7800  
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J)
total 326 89000    760000 680000  
    correct results 103 1800    9800 17000  
        correct true 67 1700    8100 16000  
        correct false 36 130    1700 1600  
    correct-unconfimed results 18 86    3000 990  
        correct-unconfirmed true 0
        correct-unconfirmed false 18 86    3000 990  
    incorrect results 1 .47 36 3.4
        incorrect true 0
        incorrect false 1 .47 36 3.4
Run set [sv-comp18.MemSafety-Arrays; sv-comp18.MemSafety-Heap; sv-comp18.MemSafety-LinkedLists; sv-comp18.MemSafety-Other]