Tool 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-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-12 19:32:16 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options -svcomp19 -heap 10000M -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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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 false(valid-memcleanup) 1 wit inspect 3.2 1.3 260 29 0   0   false(valid-memcleanup) 1 wit inspect 4.8 2.7  250 0   0   true -32 --- inspect 17   10   480 .62 0   true -32 --- inspect .66  .66  20 .078 0     - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.0 1.5 260 33 0   0   false(valid-memcleanup) 1 wit inspect 5.2 2.8  250 0   0   error (7) 0 --- inspect 21   12   360 .75 0   error (2) 0 --- inspect .71  .71  21 .13  0     - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (recursion) 0 wit inspect 3.6 1.4 260 35 0   0   error (1) 0 --- inspect 1.0 .59 46 0   0   timeout 0 --- inspect 96   76   750 1.5  0   error (1) 0 --- inspect .080 .080 11 0     0     - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.9 1.5 270 36 0   0   false(valid-memcleanup) 1 wit inspect 5.9 3.2  260 0   0   error (7) 0 --- inspect 22   13   340 .68 0   true -32 --- inspect .69  .69  20 .11  .074 - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.9 1.6 260 32 0   0   false(valid-memcleanup) 1 wit inspect 5.0 2.7  250 0   0   error (7) 0 --- inspect 18   11   320 .68 0   error (2) 0 --- inspect .69  .69  20 .11  0     - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 1.4 260 39 0   0   false(valid-memcleanup) 1 wit inspect 4.8 2.6  260 0   0   error (7) 0 --- inspect 17   9.7 310 .71 0   true -32 --- inspect .66  .67  21 .094 .44  - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 1.4 270 35 0   0   false(valid-memcleanup) 1 wit inspect 5.0 2.7  250 0   0   error (7) 0 --- inspect 18   11   310 .68 0   error (2) 0 --- inspect .67  .67  21 .094 0     - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.5 1.4 260 32 0   0   false(valid-memcleanup) 1 wit inspect 4.5 2.5  250 0   0   error (7) 0 --- inspect 17   10   310 .75 0   timeout 0 --- inspect 96     96     20 .090 0     - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 1.4 280 36 0   0   false(valid-memcleanup) 1 wit inspect 4.3 2.4  250 0   0   error (7) 0 --- inspect 17   9.6 310 .75 0   error (2) 0 --- inspect .69  .69  21 .090 .025 - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.2 1.6 270 39 0   0   false(valid-memcleanup) 1 wit inspect 5.5 3.0  260 0   0   error (7) 0 --- inspect 18   11   310 .71 0   true -32 --- inspect .67  .67  21 .094 0     - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.5 1.4 250 32 0   0   false(valid-memcleanup) 1 wit inspect 4.8 2.6  260 0   0   error (7) 0 --- inspect 17   10   300 .71 0   error (2) 0 --- inspect .68  .68  20 .086 .025 - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.2 1.5 270 34 0   0   false(valid-memcleanup) 1 wit inspect 4.8 2.6  260 0   0   error (7) 0 --- inspect 20   12   310 .71 0   error (2) 0 --- inspect .67  .67  21 .094 0     - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.4 1.4 250 32 0   0   false(valid-memcleanup) 1 wit inspect 5.4 2.9  270 0   0   error (7) 0 --- inspect 17   9.6 310 .68 0   true -32 --- inspect .66  .67  20 .086 .13  - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.1 1.5 280 33 0   0   false(valid-memcleanup) 1 wit inspect 4.5 2.5  260 0   0   error (7) 0 --- inspect 18   10   320 .68 0   true -32 --- inspect .72  .73  20 .090 .13  - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.4 1.4 260 29 0   0   false(valid-memcleanup) 1 wit inspect 5.0 2.7  250 0   0   error (7) 0 --- inspect 18   11   320 .71 0   timeout 0 --- inspect 96     96     20 .090 .025 - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.5 1.4 260 30 0   0   false(valid-memcleanup) 1 wit inspect 4.7 2.6  250 0   0   error (7) 0 --- inspect 17   10   310 .68 0   error (2) 0 --- inspect .70  .69  20 .090 0     - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.1 1.5 270 33 0   0   false(valid-memcleanup) 1 wit inspect 6.2 3.3  280 0   0   error (7) 0 --- inspect 17   9.8 310 .71 0   true -32 --- inspect .67  .67  21 .090 .025 - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.1 1.5 260 39 0   0   false(valid-memcleanup) 1 wit inspect 6.2 3.3  280 0   0   error (7) 0 --- inspect 16   9.6 310 .75 0   true -32 --- inspect .67  .67  21 .086 0     - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.6 1.4 250 33 0   0   false(valid-memcleanup) 1 wit inspect 5.3 2.9  250 0   0   error (7) 0 --- inspect 16   9.1 310 .75 0   error (2) 0 --- inspect .66  .66  20 .086 .025 - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 10   3.0 480 86 0   0   false(valid-memcleanup) 1 wit inspect 6.4 3.4  260 0   0   error (7) 0 --- inspect 17   10   310 .68 0   error (2) 0 --- inspect .68  .70  21 .090 0     - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.4 1.4 260 33 0   0   false(valid-memcleanup) 1 wit inspect 4.5 2.5  260 0   0   error (7) 0 --- inspect 18   10   310 .68 0   true -32 --- inspect .66  .69  20 .086 .025 - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.5 1.4 260 32 0   0   false(valid-memcleanup) 1 wit inspect 5.0 2.7  270 0   0   true -32 --- inspect 18   11   580 .62 0   true -32 --- inspect .68  .68  21 .078 .13  - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 1.4 260 34 0   0   false(valid-memcleanup) 1 wit inspect 5.7 3.1  260 0   0   timeout 0 --- inspect 97   74   1200 1.0  0   error (2) 0 --- inspect .65  .65  21 .078 .082 - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.4 1.4 250 32 0   0   false(valid-memcleanup) 1 wit inspect 4.3 2.4  250 0   0   false(valid-memtrack) 0 --- inspect 9.1 5.1 310 .62 0   error (2) 0 --- inspect .66  .66  20 .078 0     - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.8 1.4 270 36 0   0   false(valid-memcleanup) 1 wit inspect 5.9 3.1  250 0   0   true -32 --- inspect 18   11   510 .62 0   true -32 --- inspect .66  .66  21 .078 0     - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.9 1.5 260 38 0   0   false(valid-memcleanup) 1 wit inspect 5.6 3.0  260 0   0   timeout 0 --- inspect 96   81   950 .70 0   true -32 --- inspect .71  .71  21 .098 0     - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.4 1.4 250 32 0   0   false(valid-memcleanup) 1 wit inspect 5.2 2.9  250 0   0   true -32 --- inspect 19   12   630 .62 0   true -32 --- inspect .64  .64  20 .078 0     - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 3.7 1.5 260 32 0   0   false(valid-memcleanup) 1 wit inspect 5.8 3.2  260 0   0   true -32 --- inspect 62   43   880 .62 0   true -32 --- inspect .67  .67  21 .082 0     - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 6.8 2.1 300 56 0   0   false(valid-memcleanup) 1 wit inspect 6.7 3.6  260 0   0   true -32 --- inspect 31   19   630 .62 0   true -32 --- inspect .73  .75  21 .094 0     - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.4 1.5 290 35 0   0   false(valid-memcleanup) 1 wit inspect 4.7 2.6  250 0   0   true -32 --- inspect 44   35   620 .62 0   true -32 --- inspect .66  .66  21 .082 0     - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 4.5 1.6 290 38 0   0   false(valid-memcleanup) 1 wit inspect 6.4 3.4  260 0   0   true -32 --- inspect 45   31   790 .62 0   error (2) 0 --- inspect .66  .66  21 .098 0     - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 7.2 2.3 370 59 0   0   false(valid-memcleanup) 1 wit inspect 6.2 3.3  280 0   0   timeout 0 --- inspect 96   66   7000 1.5  0   error (2) 0 --- inspect .66  .66  21 .057 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 31 130 50 8800 1200 0   0   32 31 170 90 8100 0   0   32 -256 990 670 21000 24   0   32 -512 210 210 650 2.8 1.1  0
    correct results 31 31 130 48 8500 1100 0   0   31 31 160 89 8000 0   0   0 0 0
        correct true 0 0 0 0 0
        correct false 31 31 130 48 8500 1100 0   0   31 31 160 89 8000 0   0   0 0 0
    incorrect results 0 0 8 -256 250 170 5100 5.0 0   16 -512 11 11 330 1.4 .96 0
        incorrect true 0 0 8 -256 250 170 5100 5.0 0   16 -512 11 11 330 1.4 .96 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 31 31 -256 -512 0
Run set cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-MemCleanup