Tool CBMC
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.HeapMemSafety
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
memsafety/960521-1_false-valid-deref.i 2.8   2.9  49 18   9.5 740 81 49   1800
memsafety/test-0137_false-valid-deref.i .82  .83 64 6.0 3.4 250 91 79   610
memsafety/test-0235_false-valid-deref.i 850     850    1300
memsafety/960521-1_false-valid-free.i 2.7   2.7  49 17   9.0 720 91 69   1200
memsafety/test-0158_false-valid-free.i .23  .24 28 5.5 3.2 220 15 8.4 350
memsafety/test-0232_false-valid-free.i .28  .29 28 5.8 3.4 220 43 33   500
memsafety/20020406-1_false-valid-memtrack.i .51  .52 41 7.1 4.1 250 90 75   680
memsafety/20051113-1.c_false-valid-memtrack.i 3.5   3.5  75 6.4 3.6 210 20 11   830
memsafety/lockfree-3.1_false-valid-memtrack.i 4.6   4.6  120 7.3 4.0 250 18 9.5 370
memsafety/lockfree-3.2_false-valid-memtrack.i .27  .28 28 6.6 3.6 230 14 8.0 360
memsafety/lockfree-3.3_false-valid-memtrack.i 4.3   4.3  120 6.9 3.9 250 16 9.0 380
memsafety/test-0019_false-valid-memtrack.i .27  .28 27 4.7 2.7 220 12 7.5 330
memsafety/test-0102_false-valid-memtrack.i .51  .52 39 5.5 3.1 200 17 9.0 360
memsafety/test-0158_false-valid-memtrack.i .24  .25 27 5.6 3.1 220 11 6.1 320
memsafety/test-0220_false-valid-memtrack.i 850     850    6300
memsafety/test-0232_false-valid-memtrack.i .29  .30 27 5.5 3.2 220 13 7.2 350
memsafety/test-0234_false-valid-memtrack.i 850     850    1200
memsafety/test-0235_false-valid-memtrack.i 850     850    1200
memsafety/960521-1_true-valid-memsafety.i 28     28    14000
memsafety/lockfree-3.0_true-valid-memsafety.i 850     850    2300
memsafety/test-0019_true-valid-memsafety.i 1.7   1.7  28
memsafety/test-0102_true-valid-memsafety.i 14     14    640
memsafety/test-0134_true-valid-memsafety.i 1.0   1.0  63
memsafety/test-0158_true-valid-memsafety.i 1.7   1.8  27
memsafety/test-0214_true-valid-memsafety.i 90     90    13000
memsafety/test-0217_true-valid-memsafety.i 100     100    13000
memsafety/test-0218_true-valid-memsafety.i 83     83    13000
memsafety/test-0219_true-valid-memsafety.i 850     850    7400
memsafety/test-0232_true-valid-memsafety.i 150     150    5400
memsafety/test-0234_true-valid-memsafety.i 850     850    1300
memsafety/test-0235_true-valid-memsafety.i 850     850    1200
memsafety/test-0236_true-valid-memsafety.i 850     850    1300
memsafety/test-0237_true-valid-memsafety.i 850     850    1300
memsafety/test-0504_true-valid-memsafety.i 610     610    13000
memsafety/test-0513_true-valid-memsafety.i 850     850    5400
memsafety/test-0521_true-valid-memsafety.i 150     150    3600
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i 850     850    5600
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i 850     850    2300
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i 850     850    2200
memsafety-ext/tree_cnstr_true-valid-memsafety.i 850     850    2300
memsafety-ext/tree_dsw_true-valid-memsafety.i 850     850    2000
memsafety-ext/tree_of_cslls_true-valid-memsafety.i 850     850    200
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i 850     850    2400
memsafety-ext/tree_stack_true-valid-memsafety.i 850     850    1800
list-ext-properties/960521-1_1_false-valid-deref.i .22  .23 28 5.7 3.2 230 30 22   440
list-ext-properties/960521-1_1_false-valid-free.i .34  .35 28 4.9 2.8 220 12 6.7 350
list-ext-properties/test-0158_1_false-valid-free.i .29  .31 27 5.7 3.2 230 14 8.1 340
list-ext-properties/test-0019_1_false-valid-memtrack.i .23  .24 27 5.1 2.9 230 13 7.4 340
list-ext-properties/test-0158_1_false-valid-memtrack.i .26  .27 27 5.2 3.0 220 11 6.6 330
list-ext-properties/test-0232_1_false-valid-memtrack.i .32  .33 27 5.7 3.2 240 17 9.1 360
list-ext-properties/960521-1_1_true-valid-memsafety.i 160     160    14000
list-ext-properties/list-ext_1_true-valid-memsafety.i 250     250    2100
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i 530     530    1900
list-ext-properties/simple-ext_1_true-valid-memsafety.i 140     140    1900
list-ext-properties/test-0019_1_true-valid-memsafety.i 2.1   2.2  28
list-ext-properties/test-0158_1_true-valid-memsafety.i 2.0   2.0  28
list-ext-properties/test-0214_1_true-valid-memsafety.i 850     850    12000
list-ext-properties/test-0217_1_true-valid-memsafety.i 370     370    13000
list-ext-properties/test-0232_1_true-valid-memsafety.i 270     270    410
list-ext-properties/test-0504_1_true-valid-memsafety.i 240     240    12000
list-ext-properties/test-0513_1_true-valid-memsafety.i 300     300    13000
memory-alloca/c.03-alloca_true-valid-memsafety.i 8.6   8.7  140
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c .14  .15 25 4.4 2.5 190 15 10   350
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c .097 .11 25
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c .17  .19 24
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c .14  .16 24
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c 1.6   1.7  39 18   9.5 760 92 60   1400
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c 1.4   1.5  39
ldv-memsafety/memset2_false-valid-deref-write.c 1.6   1.7  25 4.2 2.5 190 25 13   540
ldv-memsafety/memset3_false-valid-deref-write.c 1.7   1.8  25 4.8 2.7 210 31 19   1200
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c 1.3   1.4  25 3.9 2.3 190 26 14   540
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c 1.6   1.7  25 4.5 2.6 210 32 20   1200
ldv-memsafety/memsetNonZero_false-valid-deref-write.c 1.6   1.7  25 4.6 2.6 200 34 19   1100
ldv-memsafety/memset_false-valid-deref-write.c 1.6   1.7  25 4.1 2.4 200 29 16   1200
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c 10     11    310
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c 2.3   2.4  29
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c 1.6   1.7  27
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c 2.4   2.5  29
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c 5.4   5.4  240
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c 1.8   1.9  27
ldv-memsafety/StructInitialization1_true-valid-memsafety.c .97  1.0  24
ldv-memsafety/StructInitialization2_true-valid-memsafety.c .88  .94 24
ldv-memsafety/StructInitialization_true-valid-memsafety.c .78  .82 24
ldv-memsafety/memset2_true-valid-memsafety.c 1.8   1.9  25
ldv-memsafety/memset3_true-valid-memsafety.c 1.9   2.0  25
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c 1.4   1.4  25
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c 1.9   2.0  25
ldv-memsafety/memsetNonZero_true-valid-memsafety.c 1.9   1.9  25
ldv-memsafety/memset_true-valid-memsafety.c 1.9   1.9  25
ldv-memsafety/memleaks_test14_3_false-valid-deref.i .44  .45 38 7.8 4.3 260 19 11   420
ldv-memsafety/memleaks_test22_3_false-valid-deref.i 1.8   1.8  36 7.5 4.1 250 17 9.1 370
ldv-memsafety/memleaks_test22_5_false-valid-deref.i 1.7   1.8  37 7.4 4.2 250 17 9.2 380
ldv-memsafety/memleaks_test23_2_false-valid-deref.i 55     55    720
ldv-memsafety/memleaks_test23_4_false-valid-deref.i 56     56    720
ldv-memsafety/memleaks_test11_1_false-valid-free.i .42  .43 36 6.4 3.5 250 31 21   490
ldv-memsafety/memleaks_test12_false-valid-free.i 2.3   2.3  210
ldv-memsafety/memleaks_test17_2_false-valid-free.i 1.9   1.9  50 74   39   1800 48 36   710
ldv-memsafety/memleaks_test19_false-valid-free.i .33  .34 29 9.3 5.1 290 23 14   430
ldv-memsafety/memleaks_test2_false-valid-free.i .31  .32 29 6.5 3.6 250 13 7.5 330
ldv-memsafety/memleaks_test3_false-valid-free.i .31  .32 29
ldv-memsafety/memleaks_test6_2_false-valid-free.i .32  .33 29 7.1 3.9 260 18 11   350
ldv-memsafety/memleaks_test8_2_false-valid-free.i .27  .28 29 6.8 3.7 250 17 10   390
ldv-memsafety/memleaks_test10_false-valid-memtrack.i .35  .37 29 7.3 4.0 250 15 9.2 370
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i .43  .44 36 6.4 3.5 260 16 8.6 360
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i .33  .35 29 6.9 3.8 250 13 7.5 340
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i .48  .49 36
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i .33  .35 29 7.4 4.0 250 13 7.0 340
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i .48  .49 36
ldv-memsafety/memleaks_test15_false-valid-memtrack.i .44  .45 30
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i .30  .31 29 6.7 3.7 250 16 9.3 420
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i .30  .31 29 6.9 3.8 240 12 6.8 340
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i 2.6   2.7  56 46   25   1500 44 31   650
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i 1.6   1.7  52 46   24   1500 64 48   700
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i .32  .33 32 7.7 4.3 250 14 8.4 360
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i 1.6   1.6  44 7.3 4.0 280 15 8.2 360
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i 1.1   1.1  34 8.1 4.5 270 13 7.3 350
ldv-memsafety/memleaks_test1_false-valid-memtrack.i .20  .21 29 6.1 3.4 240 12 8.3 320
ldv-memsafety/memleaks_test20_false-valid-memtrack.i .32  .33 29 6.5 3.7 240 12 6.6 330
ldv-memsafety/memleaks_test21_false-valid-memtrack.i .30  .31 29 6.3 3.5 240 10 5.6 340
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i 1.7   1.8  37 7.5 4.3 260 17 9.0 380
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i 1.5   1.5  34 7.6 4.1 280 16 8.5 390
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i 1.7   1.8  36 7.5 4.0 260 17 9.4 370
ldv-memsafety/memleaks_test4_false-valid-memtrack.i .21  .21 29 7.5 4.1 290 12 6.7 330
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i .28  .29 30 6.1 3.4 240 12 6.6 340
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i .20  .21 29 6.9 3.8 290 11 6.7 330
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i .28  .29 29 7.2 3.9 260 11 6.5 330
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i .32  .33 29 7.6 4.1 260 11 7.7 310
ldv-memsafety/memleaks_test7_false-valid-memtrack.i .31  .32 29 8.5 4.7 310 14 7.3 350
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i .27  .28 29 6.4 3.5 240 11 6.0 340
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i .30  .31 29 7.1 3.9 250 11 6.2 340
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i .29  .30 29 6.6 3.6 240 11 6.1 330
ldv-memsafety/memleaks_test10_true-valid-memsafety.i 2.6   2.7  32
ldv-memsafety/memleaks_test11_true-valid-memsafety.i 3.3   3.3  36
ldv-memsafety/memleaks_test12_true-valid-memsafety.i 2.6   2.6  210
ldv-memsafety/memleaks_test13_true-valid-memsafety.i .45  .46 38
ldv-memsafety/memleaks_test14_true-valid-memsafety.i .47  .48 38
ldv-memsafety/memleaks_test15_true-valid-memsafety.i 3.6   3.7  39
ldv-memsafety/memleaks_test16_true-valid-memsafety.i 2.4   2.4  29
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i 200     200    2200
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i .55  .56 40
ldv-memsafety/memleaks_test18_true-valid-memsafety.i 18     18    530
ldv-memsafety/memleaks_test19_true-valid-memsafety.i 2.3   2.3  29
ldv-memsafety/memleaks_test1_true-valid-memsafety.i 2.3   2.3  29
ldv-memsafety/memleaks_test20_true-valid-memsafety.i 2.4   2.4  29
ldv-memsafety/memleaks_test21_true-valid-memsafety.i 2.3   2.4  29
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i 3.5   3.5  36
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i 3.5   3.5  39
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i 3.9   3.9  39
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i 92     92    740
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i 92     92    740
ldv-memsafety/memleaks_test2_true-valid-memsafety.i 2.3   2.4  29
ldv-memsafety/memleaks_test3_true-valid-memsafety.i 2.3   2.3  29
ldv-memsafety/memleaks_test4_true-valid-memsafety.i 2.3   2.3  29
ldv-memsafety/memleaks_test5_true-valid-memsafety.i 2.3   2.4  29
ldv-memsafety/memleaks_test6_true-valid-memsafety.i 2.4   2.5  29
ldv-memsafety/memleaks_test7_true-valid-memsafety.i 2.4   2.4  29
ldv-memsafety/memleaks_test8_true-valid-memsafety.i 2.1   2.1  29
ldv-memsafety/memleaks_test9_true-valid-memsafety.i 2.3   2.4  29
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 158 21000 21000 200000 158 580   320   21000   158 1500   1000   32000  
    correct results 134 17000 17000 190000 31 580   320   21000   54 1500   1000   32000  
        correct true 71 17000 17000 180000 31 0   0   0   46 0   0   0  
        correct false 63 59 60 2300 0 580   320   21000   8 1500   1000   32000  
    incorrect results 24 3900 3900 18000 0 0   0   0   0 0   0   0  
        incorrect true 4 3400 3400 10000 0 0   0   0   0 0   0   0  
        incorrect false 20 470 470 8000 0 0   0   0   0 0   0   0  
score (158 tasks, max score: 238) -243
Run set sv-comp16.HeapMemSafety