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 false(valid-deref) 2.8   2.9  49 wit assertion 18   9.5 740 true 81 49   1800
memsafety/test-0137_false-valid-deref.i false(valid-deref) .82  .83 64 wit assertion 6.0 3.4 250 timeout 91 79   610
memsafety/test-0235_false-valid-deref.i true 850     850    1300 wit - -
memsafety/960521-1_false-valid-free.i false(valid-free) 2.7   2.7  49 wit assertion 17   9.0 720 timeout 91 69   1200
memsafety/test-0158_false-valid-free.i false(valid-free) .23  .24 28 wit true 5.5 3.2 220 false(valid-free) 15 8.4 350
memsafety/test-0232_false-valid-free.i false(valid-free) .28  .29 28 wit assertion 5.8 3.4 220 error 43 33   500
memsafety/20020406-1_false-valid-memtrack.i false(valid-memtrack) .51  .52 41 wit assertion 7.1 4.1 250 timeout 90 75   680
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 3.5   3.5  75 wit exception 6.4 3.6 210 true 20 11   830
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 4.6   4.6  120 wit assertion 7.3 4.0 250 true 18 9.5 370
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) .27  .28 28 wit assertion 6.6 3.6 230 true 14 8.0 360
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 4.3   4.3  120 wit assertion 6.9 3.9 250 true 16 9.0 380
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) .27  .28 27 wit true 4.7 2.7 220 true 12 7.5 330
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) .51  .52 39 wit exception 5.5 3.1 200 true 17 9.0 360
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) .24  .25 27 wit true 5.6 3.1 220 true 11 6.1 320
memsafety/test-0220_false-valid-memtrack.i true 850     850    6300 wit - -
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) .29  .30 27 wit assertion 5.5 3.2 220 true 13 7.2 350
memsafety/test-0234_false-valid-memtrack.i true 850     850    1200 wit - -
memsafety/test-0235_false-valid-memtrack.i true 850     850    1200 wit - -
memsafety/960521-1_true-valid-memsafety.i true 28     28    14000 wit - -
memsafety/lockfree-3.0_true-valid-memsafety.i true 850     850    2300 wit - -
memsafety/test-0019_true-valid-memsafety.i true 1.7   1.7  28 wit - -
memsafety/test-0102_true-valid-memsafety.i false(valid-free) 14     14    640 wit - -
memsafety/test-0134_true-valid-memsafety.i false(valid-deref) 1.0   1.0  63 wit - -
memsafety/test-0158_true-valid-memsafety.i true 1.7   1.8  27 wit - -
memsafety/test-0214_true-valid-memsafety.i true 90     90    13000 wit - -
memsafety/test-0217_true-valid-memsafety.i true 100     100    13000 wit - -
memsafety/test-0218_true-valid-memsafety.i true 83     83    13000 wit - -
memsafety/test-0219_true-valid-memsafety.i true 850     850    7400 wit - -
memsafety/test-0232_true-valid-memsafety.i true 150     150    5400 wit - -
memsafety/test-0234_true-valid-memsafety.i true 850     850    1300 wit - -
memsafety/test-0235_true-valid-memsafety.i true 850     850    1200 wit - -
memsafety/test-0236_true-valid-memsafety.i true 850     850    1300 wit - -
memsafety/test-0237_true-valid-memsafety.i true 850     850    1300 wit - -
memsafety/test-0504_true-valid-memsafety.i true 610     610    13000 wit - -
memsafety/test-0513_true-valid-memsafety.i true 850     850    5400 wit - -
memsafety/test-0521_true-valid-memsafety.i false(valid-deref) 150     150    3600 wit - -
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i true 850     850    5600 wit - -
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i true 850     850    2300 wit - -
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i true 850     850    2200 wit - -
memsafety-ext/tree_cnstr_true-valid-memsafety.i true 850     850    2300 wit - -
memsafety-ext/tree_dsw_true-valid-memsafety.i true 850     850    2000 wit - -
memsafety-ext/tree_of_cslls_true-valid-memsafety.i true 850     850    200 wit - -
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i true 850     850    2400 wit - -
memsafety-ext/tree_stack_true-valid-memsafety.i true 850     850    1800 wit - -
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) .22  .23 28 wit assertion 5.7 3.2 230 true 30 22   440
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) .34  .35 28 wit assertion 4.9 2.8 220 false(valid-free) 12 6.7 350
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) .29  .31 27 wit true 5.7 3.2 230 false(valid-free) 14 8.1 340
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) .23  .24 27 wit true 5.1 2.9 230 true 13 7.4 340
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) .26  .27 27 wit true 5.2 3.0 220 true 11 6.6 330
list-ext-properties/test-0232_1_false-valid-memtrack.i false(valid-memtrack) .32  .33 27 wit assertion 5.7 3.2 240 true 17 9.1 360
list-ext-properties/960521-1_1_true-valid-memsafety.i true 160     160    14000 wit - -
list-ext-properties/list-ext_1_true-valid-memsafety.i true 250     250    2100 wit - -
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 530     530    1900 wit - -
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 140     140    1900 wit - -
list-ext-properties/test-0019_1_true-valid-memsafety.i true 2.1   2.2  28 wit - -
list-ext-properties/test-0158_1_true-valid-memsafety.i true 2.0   2.0  28 wit - -
list-ext-properties/test-0214_1_true-valid-memsafety.i true 850     850    12000 wit - -
list-ext-properties/test-0217_1_true-valid-memsafety.i true 370     370    13000 wit - -
list-ext-properties/test-0232_1_true-valid-memsafety.i true 270     270    410 wit - -
list-ext-properties/test-0504_1_true-valid-memsafety.i true 240     240    12000 wit - -
list-ext-properties/test-0513_1_true-valid-memsafety.i true 300     300    13000 wit - -
memory-alloca/c.03-alloca_true-valid-memsafety.i true 8.6   8.7  140 wit - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) .14  .15 25 wit true 4.4 2.5 190 false(valid-deref) 15 10   350
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(reach) .097 .11 25 wit - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(reach) .17  .19 24 wit - -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(reach) .14  .16 24 wit - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 1.6   1.7  39 wit true 18   9.5 760 timeout 92 60   1400
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(reach) 1.4   1.5  39 wit - -
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 1.6   1.7  25 wit true 4.2 2.5 190 true 25 13   540
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1.7   1.8  25 wit true 4.8 2.7 210 true 31 19   1200
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1.3   1.4  25 wit true 3.9 2.3 190 true 26 14   540
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1.6   1.7  25 wit true 4.5 2.6 210 true 32 20   1200
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1.6   1.7  25 wit true 4.6 2.6 200 true 34 19   1100
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1.6   1.7  25 wit true 4.1 2.4 200 true 29 16   1200
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c true 10     11    310 wit - -
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c true 2.3   2.4  29 wit - -
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 1.6   1.7  27 wit - -
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c true 2.4   2.5  29 wit - -
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 5.4   5.4  240 wit - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c true 1.8   1.9  27 wit - -
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true .97  1.0  24 wit - -
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true .88  .94 24 wit - -
ldv-memsafety/StructInitialization_true-valid-memsafety.c true .78  .82 24 wit - -
ldv-memsafety/memset2_true-valid-memsafety.c true 1.8   1.9  25 wit - -
ldv-memsafety/memset3_true-valid-memsafety.c true 1.9   2.0  25 wit - -
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true 1.4   1.4  25 wit - -
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 1.9   2.0  25 wit - -
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 1.9   1.9  25 wit - -
ldv-memsafety/memset_true-valid-memsafety.c true 1.9   1.9  25 wit - -
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) .44  .45 38 wit assertion 7.8 4.3 260 true 19 11   420
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 1.8   1.8  36 wit assertion 7.5 4.1 250 true 17 9.1 370
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 1.7   1.8  37 wit assertion 7.4 4.2 250 true 17 9.2 380
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-memtrack) 55     55    720 wit - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(reach) 56     56    720 wit - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) .42  .43 36 wit assertion 6.4 3.5 250 error 31 21   490
ldv-memsafety/memleaks_test12_false-valid-free.i false(valid-deref) 2.3   2.3  210 wit - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 1.9   1.9  50 wit true 74   39   1800 error 48 36   710
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) .33  .34 29 wit true 9.3 5.1 290 false(valid-free) 23 14   430
ldv-memsafety/memleaks_test2_false-valid-free.i false(valid-free) .31  .32 29 wit true 6.5 3.6 250 true 13 7.5 330
ldv-memsafety/memleaks_test3_false-valid-free.i false(reach) .31  .32 29 wit - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) .32  .33 29 wit true 7.1 3.9 260 false(valid-free) 18 11   350
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) .27  .28 29 wit true 6.8 3.7 250 false(valid-free) 17 10   390
ldv-memsafety/memleaks_test10_false-valid-memtrack.i false(valid-memtrack) .35  .37 29 wit assertion 7.3 4.0 250 true 15 9.2 370
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i false(valid-memtrack) .43  .44 36 wit assertion 6.4 3.5 260 true 16 8.6 360
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i false(valid-memtrack) .33  .35 29 wit assertion 6.9 3.8 250 true 13 7.5 340
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-deref) .48  .49 36 wit - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i false(valid-memtrack) .33  .35 29 wit assertion 7.4 4.0 250 true 13 7.0 340
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-deref) .48  .49 36 wit - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-free) .44  .45 30 wit - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i false(valid-memtrack) .30  .31 29 wit assertion 6.7 3.7 250 false(valid-memtrack) 16 9.3 420
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i false(valid-memtrack) .30  .31 29 wit assertion 6.9 3.8 240 true 12 6.8 340
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(valid-memtrack) 2.6   2.7  56 wit true 46   25   1500 error 44 31   650
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 1.6   1.7  52 wit true 46   24   1500 error 64 48   700
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i false(valid-memtrack) .32  .33 32 wit assertion 7.7 4.3 250 true 14 8.4 360
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i false(valid-memtrack) 1.6   1.6  44 wit assertion 7.3 4.0 280 true 15 8.2 360
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i false(valid-memtrack) 1.1   1.1  34 wit assertion 8.1 4.5 270 true 13 7.3 350
ldv-memsafety/memleaks_test1_false-valid-memtrack.i false(valid-memtrack) .20  .21 29 wit true 6.1 3.4 240 true 12 8.3 320
ldv-memsafety/memleaks_test20_false-valid-memtrack.i false(valid-memtrack) .32  .33 29 wit assertion 6.5 3.7 240 true 12 6.6 330
ldv-memsafety/memleaks_test21_false-valid-memtrack.i false(valid-memtrack) .30  .31 29 wit assertion 6.3 3.5 240 true 10 5.6 340
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i false(valid-memtrack) 1.7   1.8  37 wit assertion 7.5 4.3 260 true 17 9.0 380
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i false(valid-memtrack) 1.5   1.5  34 wit assertion 7.6 4.1 280 true 16 8.5 390
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i false(valid-memtrack) 1.7   1.8  36 wit assertion 7.5 4.0 260 true 17 9.4 370
ldv-memsafety/memleaks_test4_false-valid-memtrack.i false(valid-memtrack) .21  .21 29 wit true 7.5 4.1 290 true 12 6.7 330
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i false(valid-memtrack) .28  .29 30 wit true 6.1 3.4 240 true 12 6.6 340
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i false(valid-memtrack) .20  .21 29 wit true 6.9 3.8 290 true 11 6.7 330
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i false(valid-memtrack) .28  .29 29 wit true 7.2 3.9 260 true 11 6.5 330
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i false(valid-memtrack) .32  .33 29 wit true 7.6 4.1 260 true 11 7.7 310
ldv-memsafety/memleaks_test7_false-valid-memtrack.i false(valid-memtrack) .31  .32 29 wit true 8.5 4.7 310 true 14 7.3 350
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i false(valid-memtrack) .27  .28 29 wit true 6.4 3.5 240 true 11 6.0 340
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i false(valid-memtrack) .30  .31 29 wit true 7.1 3.9 250 true 11 6.2 340
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i false(valid-memtrack) .29  .30 29 wit true 6.6 3.6 240 true 11 6.1 330
ldv-memsafety/memleaks_test10_true-valid-memsafety.i true 2.6   2.7  32 wit - -
ldv-memsafety/memleaks_test11_true-valid-memsafety.i true 3.3   3.3  36 wit - -
ldv-memsafety/memleaks_test12_true-valid-memsafety.i false(valid-deref) 2.6   2.6  210 wit - -
ldv-memsafety/memleaks_test13_true-valid-memsafety.i false(valid-deref) .45  .46 38 wit - -
ldv-memsafety/memleaks_test14_true-valid-memsafety.i false(valid-deref) .47  .48 38 wit - -
ldv-memsafety/memleaks_test15_true-valid-memsafety.i true 3.6   3.7  39 wit - -
ldv-memsafety/memleaks_test16_true-valid-memsafety.i true 2.4   2.4  29 wit - -
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i true 200     200    2200 wit - -
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i false(reach) .55  .56 40 wit - -
ldv-memsafety/memleaks_test18_true-valid-memsafety.i true 18     18    530 wit - -
ldv-memsafety/memleaks_test19_true-valid-memsafety.i true 2.3   2.3  29 wit - -
ldv-memsafety/memleaks_test1_true-valid-memsafety.i true 2.3   2.3  29 wit - -
ldv-memsafety/memleaks_test20_true-valid-memsafety.i true 2.4   2.4  29 wit - -
ldv-memsafety/memleaks_test21_true-valid-memsafety.i true 2.3   2.4  29 wit - -
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i true 3.5   3.5  36 wit - -
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i true 3.5   3.5  39 wit - -
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i true 3.9   3.9  39 wit - -
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i false(valid-memtrack) 92     92    740 wit - -
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i false(valid-memtrack) 92     92    740 wit - -
ldv-memsafety/memleaks_test2_true-valid-memsafety.i true 2.3   2.4  29 wit - -
ldv-memsafety/memleaks_test3_true-valid-memsafety.i true 2.3   2.3  29 wit - -
ldv-memsafety/memleaks_test4_true-valid-memsafety.i true 2.3   2.3  29 wit - -
ldv-memsafety/memleaks_test5_true-valid-memsafety.i true 2.3   2.4  29 wit - -
ldv-memsafety/memleaks_test6_true-valid-memsafety.i true 2.4   2.5  29 wit - -
ldv-memsafety/memleaks_test7_true-valid-memsafety.i true 2.4   2.4  29 wit - -
ldv-memsafety/memleaks_test8_true-valid-memsafety.i true 2.1   2.1  29 wit - -
ldv-memsafety/memleaks_test9_true-valid-memsafety.i true 2.3   2.4  29 wit - -
../../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