Tool PredatorHP 3.14 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* apollon001 apollon138 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-07 04:08:42 CET 2018-12-07 09:10:21 CET 2018-12-07 10:32:34 CET 2018-12-12 20:53:36 CET 2018-12-07 09:31:44 CET
Run set predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options --witness error-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/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2018-12-07_0408.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 .16 .30 35 1.2 .082 0      false(valid-memcleanup) 1 wit inspect 4.0 2.3 250 0   0   true -32 --- inspect 8.6 5.2 310 .62 0   true -32 --- inspect .68 .68 20 .078 0      - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .61 .31 45 6.0 .049 .094  false(valid-memcleanup) 1 wit inspect 4.6 2.5 250 0   0   error (7) 0 --- inspect 21   12   370 .68 0   error (2) 0 --- inspect .74 .74 20 .13  0      - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 2.8  1.3  63 27   .029 .45   error (recursion) 0 wit inspect 4.5 2.5 250 0   0   error (7) 0 --- inspect 20   12   320 .68 0   error (2) 0 --- inspect .71 .71 21 .12  .029  - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .16 .28 38 1.6 .074 .70   false(valid-memcleanup) 1 wit inspect 4.3 2.4 250 0   0   error (7) 0 --- inspect 20   12   330 .68 0   true -32 --- inspect .65 .65 20 .11  0      - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .79 .28 58 4.2 .025 19      false(valid-memcleanup) 1 wit inspect 4.2 2.3 250 0   0   error (7) 0 --- inspect 19   11   320 .68 0   error (2) 0 --- inspect .67 .67 20 .11  .025  - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .54 .28 50 4.1 .033 19      false(valid-memcleanup) 1 wit inspect 4.6 2.5 250 0   0   error (7) 0 --- inspect 17   10   320 .68 0   true -32 --- inspect .65 .65 20 .094 0      - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .16 .29 37 1.6 .082 .52   false(valid-memcleanup) 1 wit inspect 4.8 2.6 270 0   0   error (7) 0 --- inspect 20   12   320 .68 0   error (2) 0 --- inspect .67 .67 20 .094 0      - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .14 .29 38 1.3 .082 .59   false(valid-memcleanup) 1 wit inspect 4.0 2.2 250 0   0   error (7) 0 --- inspect 16   8.8 310 .68 0   timeout 0 --- inspect 96    96    20 .098 0      - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .16 .30 34 1.4 .082 0      false(valid-memcleanup) 1 wit inspect 4.5 2.4 270 0   0   error (7) 0 --- inspect 18   11   310 .68 0   error (2) 0 --- inspect .69 .69 20 .090 1.4    - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .39 .33 49 1.4 .057 18      false(valid-memcleanup) 1 wit inspect 4.6 2.5 250 0   0   error (7) 0 --- inspect 17   9.7 320 .68 0   true -32 --- inspect .71 .73 20 .094 0      - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .19 .31 36 1.3 .082 .13   false(valid-memcleanup) 1 wit inspect 4.3 2.3 250 0   0   error (7) 0 --- inspect 17   11   310 .68 0   error (2) 0 --- inspect .68 .68 20 .086 0      - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .44 .31 37 4.6 .057 0      false(valid-memcleanup) 1 wit inspect 4.9 2.6 270 0   0   error (7) 0 --- inspect 18   11   320 .68 0   error (2) 0 --- inspect .70 .70 20 .094 0      - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .16 .30 37 1.5 .082 .39   false(valid-memcleanup) 1 wit inspect 4.1 2.3 250 0   0   error (7) 0 --- inspect 16   9.2 310 .68 0   true -32 --- inspect .66 .65 20 .086 0      - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .18 .30 37 1.3 .082 .40   false(valid-memcleanup) 1 wit inspect 4.4 2.3 250 0   0   error (7) 0 --- inspect 18   10   320 .68 0   true -32 --- inspect .67 .68 20 .090 0      - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .17 .30 33 1.3 .082 .13   false(valid-memcleanup) 1 wit inspect 4.1 2.2 250 0   0   error (7) 0 --- inspect 16   9.1 310 .68 0   timeout 0 --- inspect 96    96    20 .090 0      - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .35 .29 49 1.3 .082 18      false(valid-memcleanup) 1 wit inspect 4.2 2.3 250 0   0   error (7) 0 --- inspect 16   9.2 310 .68 0   error (2) 0 --- inspect .67 .67 20 .078 .025  - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .18 .32 35 1.4 .082 .13   false(valid-memcleanup) 1 wit inspect 4.5 2.6 250 0   0   error (7) 0 --- inspect 17   9.4 320 .68 0   true -32 --- inspect .66 .66 20 .090 0      - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .37 .30 49 1.9 .082 18      false(valid-memcleanup) 1 wit inspect 4.7 2.6 250 0   0   error (7) 0 --- inspect 17   9.4 310 .68 0   true -32 --- inspect .68 .67 20 .086 0      - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .15 .29 34 1.5 .082 .13   false(valid-memcleanup) 1 wit inspect 4.1 2.4 250 0   0   error (7) 0 --- inspect 17   9.5 320 .68 0   error (2) 0 --- inspect .69 .69 20 .086 0      - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .50 .31 49 3.5 .057 18      false(valid-memcleanup) 1 wit inspect 4.6 2.5 260 0   0   error (7) 0 --- inspect 17   9.8 300 .68 0   error (2) 0 --- inspect .66 .66 20 .090 .025  - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .38 .32 49 1.2 .082 18      false(valid-memcleanup) 1 wit inspect 4.2 2.3 250 0   0   error (7) 0 --- inspect 16   9.6 310 .68 0   true -32 --- inspect .65 .65 20 .086 0      - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .16 .30 34 1.5 .082 .066  timeout 0 --- inspect 98   65   3800 0   0   true -32 --- inspect 13   7.5 470 .10 0   true -32 --- inspect .64 .64 20 .078 0      - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .21 .31 35 1.1 .082 .20   timeout 0 wit inspect 93   63   2900 0   0   false(valid-memtrack) 0 --- inspect 8.6 4.8 310 .66 0   error (2) 0 --- inspect .68 .68 20 .078 0      - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .16 .29 35 1.2 .082 .066  false(valid-memcleanup) 1 wit inspect 3.9 2.2 250 0   0   false(valid-memtrack) 0 --- inspect 8.9 5.0 310 .62 0   error (2) 0 --- inspect .65 .65 20 .078 0      - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .18 .31 37 1.5 .049 .0041 false(valid-memcleanup) 1 wit inspect 4.4 2.4 250 0   0   true -32 --- inspect 11   6.3 370 .62 0   true -32 --- inspect .67 .67 20 .078 .025  - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .17 .29 35 1.5 .057 .020  true -32 wit inspect 4.7 2.6 250 0   0   true -32 --- inspect 9.9 5.4 330 .62 0   true -32 --- inspect .71 .71 20 .098 .037  - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .33 .29 49 1.4 .082 19      timeout 0 wit inspect 97   66   3700 0   0   false(valid-memtrack) 0 --- inspect 11   6.5 370 .62 0   true -32 --- inspect .65 .65 20 .078 .0041 - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .28 .29 50 1.8 .041 19      timeout 0 wit inspect 94   63   3000 0   0   false(valid-memtrack) 0 --- inspect 8.6 4.9 310 .62 0   true -32 --- inspect .65 .65 20 .082 0      - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .17 .29 35 1.3 .057 .44   false(valid-memcleanup) 1 wit inspect 4.5 2.5 250 0   0   true -32 --- inspect 9.0 5.3 310 .62 0   error (2) 0 --- inspect .66 .66 21 .086 0      - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .22 .29 37 2.2 .082 0      false(valid-memcleanup) 1 wit inspect 4.4 2.4 250 0   0   true -32 --- inspect 59   47   740 .62 0   true -32 --- inspect .68 .68 20 .082 0      - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .46 .28 51 3.5 .074 19      false(valid-memcleanup) 1 wit inspect 4.7 2.6 250 0   0   true -32 --- inspect 68   51   940 .62 0   error (2) 0 --- inspect .69 .69 20 .098 .0041 - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .52 .29 36 5.0 .045 .13   false(valid-memcleanup) 1 wit inspect 5.3 2.9 250 0   0   true -32 --- inspect 8.8 5.0 320 .16 0   error (2) 0 --- inspect .66 .66 21 .10  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 26 12   11   1300 93 2.2  190 32 -6 510   330   20000 0   0   32 -256 580 360 11000 20   0   32 -480 210 210 650 2.9 1.6   0
    correct results 26 26 7.9 7.8 1100 58 1.8  150 26 26 110   63   6600 0   0   0 0 0
        correct true 0 0 0 0 0
        correct false 26 26 7.9 7.8 1100 58 1.8  150 26 26 110   63   6600 0   0   0 0 0
    correct-unconfimed results 6 0 3.9 2.8 270 34 .37 38 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 6 0 3.9 2.8 270 34 .37 38 0 0 0 0
    incorrect results 0 1 -32 4.7 2.6 250 0   0   8 -256 190 130 3800 4.0 0   15 -480 10 10 300 1.3 .066 0
        incorrect true 0 1 -32 4.7 2.6 250 0   0   8 -256 190 130 3800 4.0 0   15 -480 10 10 300 1.3 .066 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 26 -6 -256 -480 0
Run set predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-MemCleanup