Tool ULTIMATE Taipan 0.1.23-635dfa2a 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-08 14:19:36 CET 2018-12-09 20:52:23 CET 2018-12-09 21:15:16 CET 2018-12-12 21:23:28 CET 2018-12-09 20:55:36 CET
Run set utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options --full-output -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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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 true -32 wit inspect 33   21   650 400 .62 .0041 error (1) 0 --- inspect .72 .43 45 0   0      true -32 --- inspect 22     13     580   .62 0      error (1) 0 --- inspect .079  .079  11    0     0   - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   850   1300 9700 .73 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0      error (invalid witness file) 0 --- inspect .0020 .0025 .54 0     0   - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   840   1000 11000 .69 0      error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .0042 .0064 .54 0     0   - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 25   9.2 580 190 .66 0      error (1) 0 --- inspect .85 .50 46 0   0      true -32 --- inspect 31     19     700   .62 0      error (1) 0 --- inspect .11   .11   11    0     0   - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   860   970 12000 .72 0      error (invalid witness file) 0 --- inspect .59 .37 40 0   .0041 error (2) 0 --- inspect .028 .028 5.6 0    0      error (invalid witness file) 0 --- inspect .0039 .0057 .53 0     0   - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   860   930 9800 .63 0      error (invalid witness file) 0 --- inspect .58 .38 40 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .0052 .0090 .49 0     0   - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   800   880 11000 .70 .0082 error (invalid witness file) 0 --- inspect .58 .37 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0      error (invalid witness file) 0 --- inspect .0056 .0075 .53 0     0   - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   2000 10000 .70 15      error (invalid witness file) 0 --- inspect .63 .40 40 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0      error (invalid witness file) 0 --- inspect .0016 .0022 .53 0     0   - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   820   960 11000 .64 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .028 .028 5.6 0    0      error (invalid witness file) 0 --- inspect .0049 .0060 .39 0     0   - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   770   960 10000 .63 0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0      error (2) 0 --- inspect .051 .053 5.5 0    0      error (invalid witness file) 0 --- inspect .0017 .0022 .52 0     0   - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   840   2200 11000 .63 0      error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .0061 .0076 .52 0     0   - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   850   970 12000 .63 0      error (invalid witness file) 0 --- inspect .62 .39 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .0019 .0028 .53 0     0   - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   1000 10000 .64 0      error (invalid witness file) 0 --- inspect .62 .38 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0      error (invalid witness file) 0 --- inspect .0022 .0029 .40 0     0   - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   850   970 12000 .63 0      error (invalid witness file) 0 --- inspect .60 .38 40 0   .0041 error (2) 0 --- inspect .020 .020 5.6 0    0      error (invalid witness file) 0 --- inspect .0054 .0067 .41 0     0   - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   840   2100 10000 .63 .0082 error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0      error (invalid witness file) 0 --- inspect .0056 .0069 .52 0     0   - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   750   820 10000 .63 0      error (invalid witness file) 0 --- inspect .72 .44 40 0   .0041 error (2) 0 --- inspect .027 .029 5.7 0    0      error (invalid witness file) 0 --- inspect .0059 .0075 .53 0     0   - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   730   820 11000 .63 .029  error (invalid witness file) 0 --- inspect .61 .39 41 0   .0041 error (2) 0 --- inspect .027 .028 5.6 0    0      error (invalid witness file) 0 --- inspect .0016 .0025 .53 0     0   - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   1000 10000 .63 0      error (invalid witness file) 0 --- inspect .66 .41 42 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0      error (invalid witness file) 0 --- inspect .0054 .0080 .53 0     0   - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   820   1400 11000 .63 0      error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0      error (invalid witness file) 0 --- inspect .0024 .0031 .53 0     0   - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   750   1000 11000 .65 .029  error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .026 .026 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 timeout 0 --- inspect 900   810   720 12000 .64 0      error (invalid witness file) 0 --- inspect .58 .37 41 0   0      error (2) 0 --- inspect .031 .031 5.5 0    0      error (invalid witness file) 0 --- inspect .0033 .0043 .53 0     0   - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 47   32   640 480 .62 0      error (1) 0 --- inspect .92 .56 45 0   0      true -32 --- inspect 31     20     660   .62 0      error (1) 0 --- inspect .10   .098  11    0     0   - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 13   4.4 580 110 .66 0      timeout (exception) 0 wit inspect 92    62    3300 0   .025  false(valid-memtrack) 0 --- inspect 8.4   4.6   310   .62 .0082 error (2) 0 --- inspect .65   .66   20    .078 0   - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 9.8 3.3 390 71 .66 0      false(valid-memcleanup) 1 wit inspect 4.9  2.6  260 0   0      false(valid-memtrack) 0 --- inspect 8.4   5.1   320   .62 0      error (2) 0 --- inspect .66   .66   20    .078 0   - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 910   240   14000 5300 .63 0      error (invalid witness file) 0 --- inspect .59 .38 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .0047 .0055 .41 0     0   - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   880   2500 7600 .65 0      error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0      error (invalid witness file) 0 --- inspect .0050 .0061 .54 0     0   - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 14   4.6 590 120 .66 0      timeout 0 wit inspect 93    66    3300 0   .0082 false(valid-memtrack) 0 --- inspect 8.8   5.3   310   .62 0      true -32 --- inspect .70   .69   20    .078 0   - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 9.6 3.3 370 70 .66 0      false(valid-memcleanup) 1 wit inspect 4.8  2.6  250 0   .0082 false(valid-memtrack) 0 --- inspect 8.5   5.2   320   .62 0      true -32 --- inspect .65   .65   20    .082 0   - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   1400 11000 .63 0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0      error (invalid witness file) 0 --- inspect .0060 .0075 .52 0     0   - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 910   680   12000 11000 .63 0      error (invalid witness file) 0 --- inspect .73 .44 42 0   0      error (2) 0 --- inspect .021 .030 5.6 0    0      error (invalid witness file) 0 --- inspect .0016 .0021 .52 0     0   - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   860   1700 12000 .64 0      error (invalid witness file) 0 --- inspect .71 .44 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .0062 .0078 .54 0     0   - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   870   1000 11000 .69 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .026 .028 5.6 0    0      error (invalid witness file) 0 --- inspect .0042 .0047 .40 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 -96 23000 20000 58000 260000 21   15      32 2 210   140   8300 0   .057  32 -96 120 72 3300 4.4 .0082 32 -64 3.0 3.1 130 .32 0   0
    correct results 0 2 2 9.6 5.3 510 0   .0082 0 0 0
        correct true 0 0 0 0 0
        correct false 0 2 2 9.6 5.3 510 0   .0082 0 0 0
    incorrect results 3 -96 110 62 1900 1100 1.9 .0041 0 3 -96 84 52 1900 1.9 0      2 -64 1.3 1.3 41 .16 0   0
        incorrect true 3 -96 110 62 1900 1100 1.9 .0041 0 3 -96 84 52 1900 1.9 0      2 -64 1.3 1.3 41 .16 0   0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) -96 2 -96 -64 0
Run set utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-MemCleanup