Tool CBMC CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
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 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-12 19:29:48 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu wall mem energy blkio-w blkio-r
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 0 .096 .092 7.2 1.3  .012 0   -32 6.1 3.3 260 0   0     -32 9.6 5.3 310 .66 0   -32 .64 .64 21 .078 .025  -
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i 0 .34  .33  26   5.1  .012 0   0 96   64   2700 0   0     0 22   12   360 .68 0   0 .74 .74 21 .13  0      -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 .51  .50  27   6.6  .012 0   0 6.8 3.6 270 0   0     0 21   12   340 .68 0   0 .70 .70 22 .13  0      -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 0 .55  .54  43   7.0  .012 0   0 96   59   3700 0   0     0 20   11   320 .71 0   0 .68 .68 21 .11  0      -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 .26  .26  19   2.9  .012 0   0 96   63   2800 0   0     0 23   13   340 .68 0   0 .67 .67 21 .12  0      -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 0 .25  .24  18   3.1  .012 0   0 98   62   2900 0   0     0 21   12   320 .75 0   0 .67 .66 21 .098 0      -
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 0 .16  .16  10   1.8  .012 0   0 97   68   2500 0   0     0 17   10   310 .75 0   0 .58 .58 21 .020 0      -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 0 .12  .11  7.6 1.2  .012 0   0 94   66   2700 0   0     0 16   8.8 310 .68 0   0 96    96    20 .090 0      -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 0 .14  .14  8.4 1.5  .012 0   0 94   65   2500 0   .057 0 17   10   310 .75 0   -32 .67 .67 20 .090 .13   -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 0 .38  .37  16   5.5  .14  0   0 96   58   3900 0   0     0 19   11   310 .71 0   0 .69 .68 22 .094 .025  -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 0 .19  .18  13   2.3  .012 0   0 94   63   2300 0   0     0 18   10   310 .75 0   -32 .66 .67 21 .082 0      -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 0 .18  .17  12   2.0  .012 0   0 95   65   2300 0   0     0 21   12   320 .75 0   0 .67 .67 21 .094 0      -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 0 .18  .17  12   1.9  .012 0   0 93   58   2700 0   0     0 21   12   310 .75 0   -32 .65 .65 21 .086 0      -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 0 .22  .22  14   2.0  .012 0   0 96   73   2500 0   0     0 22   13   310 .75 0   0 .58 .60 21 .020 0      -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 0 .14  .13  7.1 1.1  .012 0   0 94   63   2600 0   0     0 17   10   320 .75 0   -32 .65 .65 21 .086 .53   -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 0 .14  .13  7.9 1.4  .012 0   0 95   71   2300 0   0     0 17   10   310 .68 0   -32 .66 .66 20 .090 0      -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 0 .35  .35  15   4.0  .090 0   0 95   58   3300 0   0     0 19   10   330 .71 0   0 .67 .68 21 .094 2.0    -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 0 .20  .19  12   1.7  .012 0   0 96   60   2400 0   0     0 17   10   310 .71 0   -32 .67 .66 21 .090 0      -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 0 .16  .16  11   1.7  .012 0   0 93   70   2500 0   0     0 20   11   310 .75 0   -32 .67 .67 21 .086 0      -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 0 .16  .15  11   1.5  .012 0   0 96   77   2200 0   0     0 18   9.8 310 .75 0   0 .67 .67 21 .090 0      -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 0 .14  .14  10   1.6  .012 0   0 94   63   2900 0   0     0 16   9.8 310 .75 0   -32 .65 .65 21 .086 .025  -
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 0 .10  .099 7.7 1.2  .012 0   0 93   63   3100 0   0     -32 8.3 5.1 310 .66 0   -32 .65 .67 21 .078 .029  -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 0 .15  .14  10   1.6  .012 0   0 96   59   3800 0   0     0 9.3 5.2 330 .66 0   -32 .66 .68 21 .070 .13   -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 0 .097 .093 7.2 1.1  .012 0   0 98   65   3600 0   0     -32 10   6.1 310 .66 0   -32 .65 .65 21 .078 .10   -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 0 .20  .19  8.4 2.1  .070 0   -32 5.8 3.1 270 0   0     -32 11   6.2 320 .66 0   -32 .67 .67 21 .078 .20   -
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 0 .24  .24  10   3.1  .10  0   -32 6.4 3.4 260 0   0     -32 13   7.0 420 .66 0   -32 .69 .69 21 .098 0      -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 0 .090 .086 7.1 .79 .012 0   0 95   65   3200 0   0     -32 7.8 4.8 310 .66 0   -32 .66 .66 21 .078 .13   -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 0 .12  .11  9.1 1.2  .012 0   0 94   62   2900 0   0     0 9.5 5.8 320 .62 0   -32 .65 .65 20 .082 0      -
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i 0 .26  .25  12   3.2  .12  0   -32 14   7.4 460 0   0     -32 11   6.0 470 .62 0   -32 .67 .67 21 .090 0      -
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i 0 .21  .20  10   2.1  .078 0   -32 64   34   3100 0   0     -32 9.4 5.5 320 .66 0   -32 .65 .65 21 .082 0      -
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i 0 .77  .76  50   8.2  .098 0   0 98   66   2600 0   0     -32 9.6 5.3 320 .66 0   0 .67 .68 21 .098 1.0    -
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i 0 16     16     640   200    .55  0   -32 25   13   640 0   0     -32 17   9.4 820 .66 0   0 .74 .74 25 .057 .0041 -
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu wall mem energy blkio-w blkio-r
total 32 0 23 23 1100 280 1.5 0   32 -192 2500 1700 76000 0   .057 32 -320 510 290 11000 22   0   32 -576 120 120 670 2.7 4.4 0
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 0 0 0 0 0
    correct-unconfimed results 32 0 23 23 1100 280 1.5 0   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 32 0 23 23 1100 280 1.5 0   0 0 0 0
    incorrect results 0 6 -192 120 64 5000 0   0     10 -320 110 61 3900 6.5 0   18 -576 12 12 370 1.5 1.3 0
        incorrect true 0 6 -192 120 64 5000 0   0     10 -320 110 61 3900 6.5 0   18 -576 12 12 370 1.5 1.3 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 0 -192 -320 -576 0
Run set cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-MemCleanup