Tool Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 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* [apollon053; apollon130] 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-06 12:20:21 CET 2018-12-07 01:02:57 CET 2018-12-07 02:56:49 CET 2018-12-12 20:36:04 CET 2018-12-07 01:25:40 CET
Run set map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options -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/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2018-12-06_1220.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 unknown 0 --- inspect 84    43    4300 730   470     0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0063 .0087 .53 0   0     - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    83 11000   .029 0      error (invalid witness file) 0 --- inspect .59 .40 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0068 .0086 .53 0   0     - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    210 11000   .029 0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0054 .0069 .53 0   0     - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    180 11000   .016 0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .030 .031 5.6 0    0   error (invalid witness file) 0 --- inspect .0049 .0064 .53 0   0     - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    140 11000   .18  0      error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0032 .0040 .52 0   0     - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    170 11000   .016 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0014 .0018 .54 0   0     - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    170 12000   .016 0      error (invalid witness file) 0 --- inspect .66 .41 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0054 .0068 .53 0   0     - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    75 9400   .012 0      error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.8 0    0   error (invalid witness file) 0 --- inspect .0016 .0021 .53 0   0     - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    170 10000   .016 0      error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0053 .0064 .54 0   0     - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    170 12000   .016 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .0016 .0020 .54 0   0     - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    170 10000   .016 0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0050 .0065 .53 0   0     - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    180 11000   .012 0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .0016 .0020 .53 0   0     - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    170 10000   .016 0      error (invalid witness file) 0 --- inspect .60 .38 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0050 .0061 .54 0   0     - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    160 10000   .016 0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0050 .0063 .53 0   0     - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    75 9300   .012 0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .033 .035 5.5 0    0   error (invalid witness file) 0 --- inspect .0015 .0018 .41 0   0     - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    170 9400   .016 0      error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.8 0    0   error (invalid witness file) 0 --- inspect .0048 .0058 .54 0   0     - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    180 11000   .016 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 .0055 .0077 .53 0   0     - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    190 11000   .016 0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .0016 .0020 .53 0   0     - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    180 9900   .016 0      error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0048 .0062 .53 0   0     - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    190 12000   .012 .029  error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0013 .0015 .41 0   0     - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    190 10000   .016 0      error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0040 .0050 .52 0   0     - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    180 9500   .016 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 .0062 .0084 .41 0   0     - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .45 .44 83 5.6 .037 0      error (1) 0 --- inspect .68 .41 44 0   0   false(valid-memtrack) 0 --- inspect 13     8.0   510   .66 0   error (1) 0 --- inspect .069  .069  11    0   .025 - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .46 .44 82 6.6 .033 0      error (1) 0 --- inspect .68 .42 43 0   0   false(valid-memtrack) 0 --- inspect 9.7   5.5   320   .66 0   error (1) 0 --- inspect .069  .070  11    0   0     - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i unknown 0 --- inspect 40    20    4500 460   860     .0041 error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0018 .0035 .52 0   0     - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    450    75 9600   .016 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.8 0    0   error (invalid witness file) 0 --- inspect .0057 .0078 .53 0   0     - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .44 .42 83 5.5 .033 0      error (1) 0 --- inspect .66 .39 44 0   0   false(valid-memtrack) 0 --- inspect 13     7.3   480   .66 0   error (1) 0 --- inspect .072  .073  11    0   0     - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .46 .45 83 6.5 .041 0      error (1) 0 --- inspect .69 .41 44 0   0   false(valid-memtrack) 0 --- inspect 11     6.5   350   .66 0   error (1) 0 --- inspect .082  .084  11    0   0     - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    2100 7000   8.8   0      error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .0056 .0070 .53 0   0     - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i unknown 0 --- inspect 19    19    83 290   0     0      error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0029 .0041 .52 0   0     - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    570 10000   1.0   .0041 error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0049 .0060 .53 0   0     - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    120 13000   .11  0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .0044 .0056 .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 23000   14000   15000 260000 1300    .037 32 0 19 12 1300 0   0   32 0 47 28 1800 2.6 0   32 0 .41 .44 60 0   .025 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 4 0 1.8 1.7 330 24 .14 0     0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 4 0 1.8 1.7 330 24 .14 0     0 0 0 0
    incorrect results 0 0 0 0 0
        incorrect true 0 0 0 0 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 0 0 0 0 0
Run set map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-map2check.sv-comp19_prop-memsafety.MemSafety-MemCleanup