Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-23-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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.HeapMemSafety
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.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) 4.7   5.1   57   wit timeout 91   82   2200 true 13   6.9 330
memsafety/test-0137_false-valid-deref.i out of memory 50     50     15000   wit - -
memsafety/test-0235_false-valid-deref.i unknown 890     900     23   wit - -
memsafety/960521-1_false-valid-free.i false(valid-free) 4.8   5.1   57   wit timeout 91   82   2300 true 13   8.0 330
memsafety/test-0158_false-valid-free.i unknown .097 .10  20   wit - -
memsafety/test-0232_false-valid-free.i unknown 17     17     3200   wit - -
memsafety/20020406-1_false-valid-memtrack.i out of memory 110     110     15000   wit - -
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 3.7   4.1   57   wit timeout 91   84   2200 timeout 91   67   4300
memsafety/lockfree-3.1_false-valid-memtrack.i unknown 900     900     12000   wit - -
memsafety/lockfree-3.2_false-valid-memtrack.i unknown 900     900     11000   wit - -
memsafety/lockfree-3.3_false-valid-memtrack.i unknown 900     900     12000   wit - -
memsafety/test-0019_false-valid-memtrack.i false(valid-memtrack) 1.2   1.6   19   wit timeout 90   85   2000 true 10   5.6 340
memsafety/test-0102_false-valid-memtrack.i out of memory 480     480     15000   wit - -
memsafety/test-0158_false-valid-memtrack.i false(valid-memtrack) 1.2   1.5   19   wit timeout 92   80   3900 true 13   7.3 350
memsafety/test-0220_false-valid-memtrack.i out of memory 550     550     15000   wit - -
memsafety/test-0232_false-valid-memtrack.i unknown 900     900     4600   wit - -
memsafety/test-0234_false-valid-memtrack.i unknown 890     900     23   wit - -
memsafety/test-0235_false-valid-memtrack.i unknown 890     900     23   wit - -
memsafety/960521-1_true-valid-memsafety.i true .43  .44  21   wit - -
memsafety/lockfree-3.0_true-valid-memsafety.i unknown 900     900     11000   wit - -
memsafety/test-0019_true-valid-memsafety.i true .12  .13  18   wit - -
memsafety/test-0102_true-valid-memsafety.i out of memory 480     480     15000   wit - -
memsafety/test-0134_true-valid-memsafety.i out of memory 50     50     15000   wit - -
memsafety/test-0158_true-valid-memsafety.i unknown .12  .13  18   wit - -
memsafety/test-0214_true-valid-memsafety.i out of memory 95     94     15000   wit - -
memsafety/test-0217_true-valid-memsafety.i out of memory 490     490     15000   wit - -
memsafety/test-0218_true-valid-memsafety.i out of memory 700     700     15000   wit - -
memsafety/test-0219_true-valid-memsafety.i out of memory 540     540     15000   wit - -
memsafety/test-0232_true-valid-memsafety.i unknown 4.9   4.9   600   wit - -
memsafety/test-0234_true-valid-memsafety.i unknown 890     900     23   wit - -
memsafety/test-0235_true-valid-memsafety.i unknown 900     900     23   wit - -
memsafety/test-0236_true-valid-memsafety.i unknown 890     900     22   wit - -
memsafety/test-0237_true-valid-memsafety.i unknown 890     900     23   wit - -
memsafety/test-0504_true-valid-memsafety.i out of memory 540     540     15000   wit - -
memsafety/test-0513_true-valid-memsafety.i out of memory 80     79     15000   wit - -
memsafety/test-0521_true-valid-memsafety.i unknown 900     900     10000   wit - -
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i unknown 23     23     6100   wit - -
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i out of memory 48     47     15000   wit - -
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i out of memory 47     47     15000   wit - -
memsafety-ext/tree_cnstr_true-valid-memsafety.i out of memory 65     65     15000   wit - -
memsafety-ext/tree_dsw_true-valid-memsafety.i out of memory 63     63     15000   wit - -
memsafety-ext/tree_of_cslls_true-valid-memsafety.i out of memory 350     350     15000   wit - -
memsafety-ext/tree_parent_ptr_true-valid-memsafety.i out of memory 66     66     15000   wit - -
memsafety-ext/tree_stack_true-valid-memsafety.i out of memory 64     63     15000   wit - -
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 2.5   2.8   50   wit timeout 91   85   2200 true 10   5.9 330
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 2.4   2.8   49   wit timeout 92   85   3300 true 12   7.5 320
list-ext-properties/test-0158_1_false-valid-free.i unknown .11  .12  18   wit - -
list-ext-properties/test-0019_1_false-valid-memtrack.i false(valid-memtrack) 1.2   1.6   19   wit timeout 91   84   2200 true 12   6.9 340
list-ext-properties/test-0158_1_false-valid-memtrack.i false(valid-memtrack) 1.0   1.4   18   wit timeout 92   84   3900 true 13   7.3 360
list-ext-properties/test-0232_1_false-valid-memtrack.i unknown .40  .41  52   wit - -
list-ext-properties/960521-1_1_true-valid-memsafety.i true 1.6   1.6   49   wit - -
list-ext-properties/list-ext_1_true-valid-memsafety.i unknown 890     900     270   wit - -
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i unknown 890     900     220   wit - -
list-ext-properties/simple-ext_1_true-valid-memsafety.i unknown 890     900     190   wit - -
list-ext-properties/test-0019_1_true-valid-memsafety.i true .15  .16  18   wit - -
list-ext-properties/test-0158_1_true-valid-memsafety.i unknown .12  .14  18   wit - -
list-ext-properties/test-0214_1_true-valid-memsafety.i unknown 4.7   4.7   520   wit - -
list-ext-properties/test-0217_1_true-valid-memsafety.i unknown 890     900     2900   wit - -
list-ext-properties/test-0232_1_true-valid-memsafety.i unknown .42  .43  52   wit - -
list-ext-properties/test-0504_1_true-valid-memsafety.i unknown 900     900     13000   wit - -
list-ext-properties/test-0513_1_true-valid-memsafety.i out of memory 50     49     15000   wit - -
memory-alloca/c.03-alloca_true-valid-memsafety.i true 2.5   2.5   80   wit - -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 130     130     1100   wit timeout 90   46   2700 error 17   9.6 410
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 130     130     1100   wit timeout 90   46   3700 error 16   9.6 430
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 9.8   9.9   370   wit timeout 91   67   3700 error 14   7.8 340
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 10     10     370   wit timeout 91   67   3700 error 17   9.9 340
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) .90  .94  40   wit timeout 90   77   3600 true 16   8.9 380
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) .58  .61  40   wit timeout 91   76   3600 true 14   8.4 340
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) .37  .40  13   wit false(valid-deref) 5.9 3.4 240 false(valid-deref) 13   7.6 340
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1.6   1.6   14   wit false(valid-deref) 15   8.8 680 false(valid-deref) 11   7.7 340
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) .30  .33  13   wit false(valid-deref) 6.5 3.7 250 false(valid-deref) 13   8.2 330
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1.6   1.6   14   wit false(valid-deref) 16   9.2 700 false(valid-deref) 11   6.0 320
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1.6   1.6   14   wit false(valid-deref) 6.1 3.5 260 false(valid-deref) 9.9 5.6 320
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1.5   1.6   14   wit false(valid-deref) 6.3 3.6 250 false(valid-deref) 13   8.7 330
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c true 4.1   4.1   45   wit - -
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety.c true .53  .54  13   wit - -
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true .29  .30  13   wit - -
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety.c true .51  .52  13   wit - -
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2.3   2.3   26   wit - -
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety.c true .32  .32  13   wit - -
ldv-memsafety/StructInitialization1_true-valid-memsafety.c unknown .042 .052 4.9 wit - -
ldv-memsafety/StructInitialization2_true-valid-memsafety.c unknown .060 .070 5.0 wit - -
ldv-memsafety/StructInitialization_true-valid-memsafety.c true .063 .069 13   wit - -
ldv-memsafety/memset2_true-valid-memsafety.c true .29  .30  13   wit - -
ldv-memsafety/memset3_true-valid-memsafety.c true 1.5   1.5   13   wit - -
ldv-memsafety/memsetNonZero2_true-valid-memsafety.c true .35  .36  13   wit - -
ldv-memsafety/memsetNonZero3_true-valid-memsafety.c true 1.4   1.5   13   wit - -
ldv-memsafety/memsetNonZero_true-valid-memsafety.c true 1.4   1.4   14   wit - -
ldv-memsafety/memset_true-valid-memsafety.c true 1.5   1.5   13   wit - -
ldv-memsafety/memleaks_test14_3_false-valid-deref.i unknown .025 .037 8.0 wit - -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i unknown .023 .033 8.2 wit - -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i unknown .020 .029 8.0 wit - -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i unknown .017 .026 8.2 wit - -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i unknown .028 .041 8.2 wit - -
ldv-memsafety/memleaks_test11_1_false-valid-free.i unknown .022 .030 8.3 wit - -
ldv-memsafety/memleaks_test12_false-valid-free.i unknown .026 .036 8.1 wit - -
ldv-memsafety/memleaks_test17_2_false-valid-free.i unknown .042 .052 8.2 wit - -
ldv-memsafety/memleaks_test19_false-valid-free.i unknown .040 .054 8.1 wit - -
ldv-memsafety/memleaks_test2_false-valid-free.i unknown .031 .041 8.1 wit - -
ldv-memsafety/memleaks_test3_false-valid-free.i unknown .022 .031 8.1 wit - -
ldv-memsafety/memleaks_test6_2_false-valid-free.i unknown .033 .044 8.0 wit - -
ldv-memsafety/memleaks_test8_2_false-valid-free.i unknown .045 .058 8.3 wit - -
ldv-memsafety/memleaks_test10_false-valid-memtrack.i unknown .040 .050 8.1 wit - -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack.i unknown .039 .049 8.4 wit - -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack.i unknown .042 .054 8.2 wit - -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i unknown .022 .032 8.1 wit - -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack.i unknown .022 .034 8.0 wit - -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i unknown .045 .058 8.0 wit - -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i unknown .035 .049 8.1 wit - -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack.i unknown .027 .036 8.2 wit - -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack.i unknown .044 .055 8.0 wit - -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i unknown .023 .031 8.1 wit - -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i unknown .027 .034 8.1 wit - -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack.i unknown .034 .046 8.0 wit - -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack.i unknown .045 .057 8.1 wit - -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack.i unknown .034 .045 8.1 wit - -
ldv-memsafety/memleaks_test1_false-valid-memtrack.i unknown .038 .052 8.1 wit - -
ldv-memsafety/memleaks_test20_false-valid-memtrack.i unknown .036 .049 8.1 wit - -
ldv-memsafety/memleaks_test21_false-valid-memtrack.i unknown .018 .025 7.8 wit - -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack.i unknown .031 .040 8.1 wit - -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack.i unknown .030 .041 8.2 wit - -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack.i unknown .017 .025 7.8 wit - -
ldv-memsafety/memleaks_test4_false-valid-memtrack.i unknown .023 .032 8.0 wit - -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack.i unknown .015 .024 8.0 wit - -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack.i unknown .019 .024 8.2 wit - -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack.i unknown .021 .029 7.9 wit - -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack.i unknown .021 .030 8.1 wit - -
ldv-memsafety/memleaks_test7_false-valid-memtrack.i unknown .038 .053 8.1 wit - -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack.i unknown .030 .038 8.1 wit - -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack.i unknown .024 .030 8.1 wit - -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack.i unknown .034 .047 7.9 wit - -
ldv-memsafety/memleaks_test10_true-valid-memsafety.i unknown .022 .029 8.1 wit - -
ldv-memsafety/memleaks_test11_true-valid-memsafety.i unknown .024 .035 8.3 wit - -
ldv-memsafety/memleaks_test12_true-valid-memsafety.i unknown .027 .040 8.1 wit - -
ldv-memsafety/memleaks_test13_true-valid-memsafety.i unknown .023 .033 8.0 wit - -
ldv-memsafety/memleaks_test14_true-valid-memsafety.i unknown .018 .028 8.1 wit - -
ldv-memsafety/memleaks_test15_true-valid-memsafety.i unknown .039 .048 8.0 wit - -
ldv-memsafety/memleaks_test16_true-valid-memsafety.i unknown .023 .036 8.0 wit - -
ldv-memsafety/memleaks_test17_1_true-valid-memsafety.i unknown .035 .045 8.1 wit - -
ldv-memsafety/memleaks_test17_2_true-valid-memsafety.i unknown .030 .041 8.1 wit - -
ldv-memsafety/memleaks_test18_true-valid-memsafety.i unknown .031 .042 8.3 wit - -
ldv-memsafety/memleaks_test19_true-valid-memsafety.i unknown .025 .035 8.1 wit - -
ldv-memsafety/memleaks_test1_true-valid-memsafety.i unknown .021 .030 8.2 wit - -
ldv-memsafety/memleaks_test20_true-valid-memsafety.i unknown .027 .035 8.2 wit - -
ldv-memsafety/memleaks_test21_true-valid-memsafety.i unknown .027 .036 8.1 wit - -
ldv-memsafety/memleaks_test22_1_true-valid-memsafety.i unknown .021 .030 8.0 wit - -
ldv-memsafety/memleaks_test22_2_true-valid-memsafety.i unknown .030 .040 8.1 wit - -
ldv-memsafety/memleaks_test22_3_true-valid-memsafety.i unknown .031 .040 8.1 wit - -
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i unknown .020 .030 8.1 wit - -
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i unknown .022 .033 8.1 wit - -
ldv-memsafety/memleaks_test2_true-valid-memsafety.i unknown .032 .041 8.0 wit - -
ldv-memsafety/memleaks_test3_true-valid-memsafety.i unknown .019 .026 8.1 wit - -
ldv-memsafety/memleaks_test4_true-valid-memsafety.i unknown .029 .039 8.1 wit - -
ldv-memsafety/memleaks_test5_true-valid-memsafety.i unknown .039 .053 8.2 wit - -
ldv-memsafety/memleaks_test6_true-valid-memsafety.i unknown .040 .051 8.3 wit - -
ldv-memsafety/memleaks_test7_true-valid-memsafety.i unknown .021 .030 8.2 wit - -
ldv-memsafety/memleaks_test8_true-valid-memsafety.i unknown .038 .051 8.2 wit - -
ldv-memsafety/memleaks_test9_true-valid-memsafety.i unknown .035 .047 8.2 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 390000 158 1400   1200   48000   158 350   220   11000  
    correct results 39 340 340 3900 6 1400   1200   48000   16 350   220   11000  
        correct true 18 19 20 400 0 0   0   0   10 0   0   0  
        correct false 21 320 320 3500 6 1400   1200   48000   6 350   220   11000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (158 tasks, max score: 238) 57
Run set sv-comp16.HeapMemSafety