Tool PeSCo 1.7-svn b8d6131600+ 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* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] 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:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-12 20:37:42 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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 error (1) 0 --- inspect .55 .29 44 5.5 0   0   error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0017 .0022 .53 0   0   - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .50 .28 42 5.3 0   0   error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .021 .022 5.5 0   0   error (invalid witness file) 0 --- inspect .0019 .0024 .54 0   0   - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .48 .26 42 4.5 0   0   error (invalid witness file) 0 --- inspect .60 .37 42 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/merge_sort_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .49 .27 42 5.4 0   0   error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0045 .0065 .41 0   0   - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .27 43 4.8 0   0   error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0044 .0057 .53 0   0   - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .28 42 5.2 0   0   error (invalid witness file) 0 --- inspect .60 .38 42 0   0   error (2) 0 --- inspect .022 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .0050 .0061 .53 0   0   - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .53 .29 43 4.6 0   0   error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0   0   error (invalid witness file) 0 --- inspect .0049 .0060 .53 0   0   - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .28 42 4.4 0   0   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 .0017 .0023 .54 0   0   - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .27 42 5.2 0   0   error (invalid witness file) 0 --- inspect .69 .44 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .0026 .0038 .40 0   0   - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .49 .26 43 5.3 0   0   error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .0022 .0029 .53 0   0   - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .54 .29 43 5.4 0   0   error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0017 .0024 .53 0   0   - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .29 42 5.1 0   0   error (invalid witness file) 0 --- inspect .61 .38 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .0025 .0039 .53 0   0   - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .55 .30 42 5.4 0   0   error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0017 .0024 .53 0   0   - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .50 .28 43 4.7 0   0   error (invalid witness file) 0 --- inspect .74 .46 42 0   0   error (2) 0 --- inspect .024 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0059 .0073 .53 0   0   - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .49 .27 42 5.4 0   0   error (invalid witness file) 0 --- inspect .68 .41 42 0   0   error (2) 0 --- inspect .025 .027 5.6 0   0   error (invalid witness file) 0 --- inspect .0047 .0063 .53 0   0   - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .48 .27 43 4.9 0   0   error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .0049 .0062 .53 0   0   - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .54 .30 42 5.0 0   0   error (invalid witness file) 0 --- inspect .66 .42 42 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0059 .0076 .53 0   0   - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .52 .30 44 4.8 0   0   error (invalid witness file) 0 --- inspect .63 .39 40 0   0   error (2) 0 --- inspect .020 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .0062 .0084 .53 0   0   - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .28 43 4.7 0   0   error (invalid witness file) 0 --- inspect .67 .41 42 0   0   error (2) 0 --- inspect .021 .022 5.8 0   0   error (invalid witness file) 0 --- inspect .0059 .0076 .53 0   0   - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .49 .27 42 4.6 0   0   error (invalid witness file) 0 --- inspect .69 .43 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .0052 .0066 .53 0   0   - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .50 .27 42 4.4 0   0   error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .024 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0018 .0029 .53 0   0   - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .29 44 5.0 0   0   error (invalid witness file) 0 --- inspect .61 .38 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0062 .0077 .53 0   0   - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .52 .29 44 5.1 0   0   error (invalid witness file) 0 --- inspect .71 .42 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0019 .0024 .53 0   0   - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .28 42 5.3 0   0   error (invalid witness file) 0 --- inspect .66 .45 41 0   0   error (2) 0 --- inspect .026 .027 5.5 0   0   error (invalid witness file) 0 --- inspect .0056 .0072 .53 0   0   - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .52 .28 42 4.9 0   0   error (invalid witness file) 0 --- inspect .63 .38 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0052 .0063 .54 0   0   - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .50 .27 42 4.9 0   0   error (invalid witness file) 0 --- inspect .63 .39 42 0   0   error (2) 0 --- inspect .023 .026 5.6 0   0   error (invalid witness file) 0 --- inspect .0041 .0052 .54 0   0   - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .49 .28 42 4.9 0   0   error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .0053 .0065 .52 0   0   - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .26 42 4.4 0   0   error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .0020 .0026 .52 0   0   - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .50 .27 42 4.7 0   0   error (invalid witness file) 0 --- inspect .75 .45 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0052 .0067 .53 0   0   - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .52 .29 43 5.0 0   0   error (invalid witness file) 0 --- inspect .58 .35 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .0051 .0062 .53 0   0   - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .53 .29 42 5.3 0   0   error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0021 .0027 .50 0   0   - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .51 .28 41 4.8 0   0   error (invalid witness file) 0 --- inspect .69 .43 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0058 .0068 .53 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 16 9.0 1400 160 0   0   32 0 20 13 1300 0   0   32 0 .70 .74 180 0   0   32 0 .13 .16 17 0   0   0
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 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 pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-MemCleanup