Tool CBMC Path 5.10 () 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:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-12 19:23:37 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-cbmc-path.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 out of memory 0 --- inspect 330     330     15000   3600    1200     0      error (invalid witness file) 0 --- inspect .64 .42 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .0024 .0031 .53 0     0      - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i out of memory 0 --- inspect 450     450     15000   5800    2100     0      error (invalid witness file) 0 --- inspect .80 .50 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0057 .0073 .53 0     0      - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .12  .12  9.4 1.4  .012 0      error (invalid witness file) 0 --- inspect .71 .43 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0035 .0045 .53 0     0      - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .12  .11  7.7 1.0  .012 0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .0017 .0021 .52 0     0      - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .097 .097 8.2 .88 .037 0      error (invalid witness file) 0 --- inspect .67 .40 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .0047 .0057 .54 0     0      - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .10  .10  7.9 .96 .012 0      error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0055 .0071 .53 0     0      - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  8.8 1.0  .053 0      error (invalid witness file) 0 --- inspect .66 .42 43 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .0017 .0024 .53 0     0      - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  8.0 .99 .098 0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .022 .022 5.5 0    0   error (invalid witness file) 0 --- inspect .0063 .0078 .53 0     0      - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  8.0 1.1  .053 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .0048 .0058 .40 0     0      - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .12  .12  9.6 1.6  .16  0      error (invalid witness file) 0 --- inspect .67 .40 41 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .0051 .0065 .53 0     0      - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .12  .12  8.6 .98 .057 0      error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0053 .0067 .53 0     0      - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .12  .12  8.9 1.5  .11  0      error (invalid witness file) 0 --- inspect .69 .41 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0049 .0065 .54 0     0      - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  7.9 1.1  .041 0      error (invalid witness file) 0 --- inspect .66 .41 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .0055 .0074 .54 0     0      - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .10  .10  8.4 .96 .012 0      error (invalid witness file) 0 --- inspect .77 .46 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .0046 .0057 .53 0     0      - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .092 .092 8.0 1.1  .094 0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .0038 .0047 .53 0     0      - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .099 .099 8.0 1.1  .053 0      error (invalid witness file) 0 --- inspect .62 .37 43 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0056 .0094 .49 0     0      - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .15  .15  8.8 1.2  .14  0      error (invalid witness file) 0 --- inspect .68 .41 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0   error (invalid witness file) 0 --- inspect .0055 .0072 .53 0     0      - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .092 .091 8.5 .88 .037 0      error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0061 .0092 .54 0     0      - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .095 .093 8.2 .82 .049 0      error (invalid witness file) 0 --- inspect .67 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .0049 .0060 .41 0     0      - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  8.6 1.1  .094 0      error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0035 .0046 .54 0     0      - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .087 .086 7.8 1.1  .037 0      error (invalid witness file) 0 --- inspect .79 .47 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0021 .0027 .53 0     0      - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i out of memory 0 --- inspect 570     570     15000   7100    2300     .0041 error (invalid witness file) 0 --- inspect .65 .41 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .0049 .0063 .54 0     0      - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .090 .088 7.9 .50 .029 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .0048 .0060 .53 0     0      - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .069 .070 7.5 .48 .012 0      error (invalid witness file) 0 --- inspect .63 .37 40 0   0   error (2) 0 --- inspect .028 .029 5.8 0    0   error (invalid witness file) 0 --- inspect .0062 .0078 .53 0     0      - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .20  .20  16   2.2  .43  0      error (invalid witness file) 0 --- inspect .76 .45 41 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .0020 .0026 .54 0     0      - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 430     430     2200   5900    1900     .0041 true -32 wit inspect 5.9  3.2  250 0   0   true -32 --- inspect 10     6.0   410   .62 0   true -32 --- inspect .70   .70   21    .098 0      - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .14  .14  7.2 1.2  .20  0      timeout (exception) 0 wit inspect 93    63    3100 0   0   true -32 --- inspect 8.4   5.0   310   .66 0   true -32 --- inspect .65   .67   21    .078 1.1    - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .096 .092 8.0 .88 .061 0      timeout 0 wit inspect 94    59    2900 0   0   false(valid-memtrack) 0 --- inspect 10     5.9   320   .18 0   true -32 --- inspect .65   .65   20    .082 .0041 - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i error (42) 0 --- inspect 880     880     7100   9900    2200     0      error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .0045 .0050 .40 0     0      - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i error (42) 0 --- inspect 870     880     7500   13000    3900     0      error (invalid witness file) 0 --- inspect .66 .40 41 0   0   error (2) 0 --- inspect .020 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0062 .0083 .53 0     0      - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i out of memory 0 --- inspect 580     580     15000   7200    2700     .0041 error (invalid witness file) 0 --- inspect .77 .47 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .0022 .0047 .53 0     0      - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .087 .085 8.9 .64 .012 0      error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .023 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .0048 .0063 .52 0     0      - --- inspect
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 4100 4100 77000 52000 16000 .012  32 -32 210   140   7400 0   0   32 -64 30 18 1200 1.5 0   32 -96 2.1 2.2 77 .26 1.1 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 3 0 430 430 2200 5900 1900 .0041 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 3 0 430 430 2200 5900 1900 .0041 0 0 0 0
    incorrect results 0 1 -32 5.9 3.2 250 0   0   2 -64 19 11 720 1.3 0   3 -96 2.0 2.0 62 .26 1.1 0
        incorrect true 0 1 -32 5.9 3.2 250 0   0   2 -64 19 11 720 1.3 0   3 -96 2.0 2.0 62 .26 1.1 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 0 -32 -64 -96 0
Run set cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-MemCleanup