Tool DepthK 3.1 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; apollon005; apollon039; apollon053; apollon087; apollon091] 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 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-12 19:35:41 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-depthk.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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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(unreach-call) 0 wit inspect .16 .16 34 2.0 .85 0      false(valid-memcleanup) 1 wit inspect 4.3  2.4  250 0   0   true -32 --- inspect 8.5   5.1   310   .66 0   true -32 --- inspect .67   .67   20    .078 0     - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .24 .23 35 3.1 1.0  0      false(valid-memcleanup) 1 wit inspect 4.9  2.7  250 0   0   error (7) 0 --- inspect 22     13     360   .68 0   error (2) 0 --- inspect .71   .71   20    .13  0     - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i unknown 0 --- inspect 900    900    12000 5700   11    0      error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .021 .021 5.7 0    0   error (invalid witness file) 0 --- inspect .0040 .0059 .53 0     0     - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .70 .69 38 9.1 31    0      false(valid-memcleanup) 1 wit inspect 4.5  2.5  250 0   0   error (7) 0 --- inspect 21     12     330   .68 0   error (2) 0 --- inspect .67   .67   20    .11  0     - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .19 .19 35 2.3 1.0  0      false(valid-memcleanup) 1 wit inspect 5.6  3.0  260 0   0   error (7) 0 --- inspect 19     11     310   .71 0   error (2) 0 --- inspect .68   .68   20    .11  .025 - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .47 .47 36 6.0 26    0      false(valid-memcleanup) 1 wit inspect 4.5  2.5  260 0   0   error (7) 0 --- inspect 17     10     310   .68 0   true -32 --- inspect .67   .68   20    .086 0     - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .21 .21 35 2.5 1.0  0      false(valid-memcleanup) 1 wit inspect 4.6  2.5  260 0   0   error (7) 0 --- inspect 17     10     310   .68 0   error (2) 0 --- inspect .69   .69   20    .057 0     - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .16 .16 34 1.8 1.0  0      false(valid-memcleanup) 1 wit inspect 4.8  2.6  250 0   0   error (7) 0 --- inspect 17     9.6   310   .68 0   timeout 0 --- inspect 96      96      20    .098 0     - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .16 .16 34 1.8 .85 0      false(valid-memcleanup) 1 wit inspect 4.7  2.5  260 0   0   error (7) 0 --- inspect 17     9.6   310   .71 0   error (2) 0 --- inspect .66   .67   20    .090 .80  - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.3  1.3  37 16   92    0      false(valid-memcleanup) 1 wit inspect 4.8  2.6  250 0   0   error (7) 0 --- inspect 17     10     310   .71 0   true -32 --- inspect .68   .68   20    .094 0     - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .18 .18 35 2.0 1.0  0      false(valid-memcleanup) 1 wit inspect 4.8  2.6  270 0   0   error (7) 0 --- inspect 16     9.1   320   .71 0   error (2) 0 --- inspect .68   .68   20    .086 0     - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .51 .51 36 5.8 31    0      false(valid-memcleanup) 1 wit inspect 5.3  2.9  260 0   0   error (7) 0 --- inspect 18     10     320   .68 0   error (2) 0 --- inspect .69   .69   20    .094 0     - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .19 .19 34 2.2 1.0  0      false(valid-memcleanup) 1 wit inspect 5.0  2.7  250 0   0   error (7) 0 --- inspect 17     9.9   310   .68 0   true -32 --- inspect .66   .67   20    .086 .13  - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .65 .65 36 9.9 31    0      false(valid-memcleanup) 1 wit inspect 5.1  2.8  280 0   0   error (7) 0 --- inspect 17     10     310   .68 0   true -32 --- inspect .67   .67   20    .090 0     - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .17 .17 34 1.8 1.0  0      false(valid-memcleanup) 1 wit inspect 5.3  2.8  270 0   0   error (7) 0 --- inspect 16     9.8   310   .75 0   timeout 0 --- inspect 96      97      20    .090 0     - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .19 .19 35 1.7 1.0  0      false(valid-memcleanup) 1 wit inspect 5.1  2.8  250 0   0   error (7) 0 --- inspect 17     9.9   310   .75 0   error (2) 0 --- inspect .66   .67   20    .090 1.7   - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.3  1.3  37 17   77    0      false(valid-memcleanup) 1 wit inspect 4.8  2.6  260 0   0   error (7) 0 --- inspect 17     9.9   310   .71 0   true -32 --- inspect .67   .67   20    .090 0     - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .53 .53 36 7.0 31    0      false(valid-memcleanup) 1 wit inspect 5.0  2.7  280 0   0   error (7) 0 --- inspect 17     9.8   310   .68 0   true -32 --- inspect .66   .66   20    .086 .79  - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .18 .18 34 1.9 1.0  0      false(valid-memcleanup) 1 wit inspect 4.6  2.5  270 0   0   error (7) 0 --- inspect 16     9.3   310   .68 0   error (2) 0 --- inspect .67   .67   20    .086 0     - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .49 .48 35 5.9 31    0      false(valid-memcleanup) 1 wit inspect 5.1  2.8  250 0   0   error (7) 0 --- inspect 17     10     320   .38 0   error (2) 0 --- inspect .67   .67   20    .090 0     - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .18 .17 34 2.0 1.0  0      false(valid-memcleanup) 1 wit inspect 4.6  2.5  280 0   0   error (7) 0 --- inspect 16     9.7   310   .71 0   true -32 --- inspect .66   .69   20    .086 0     - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .48 .48 35 4.8 31    0      false(valid-memcleanup) 1 wit inspect 4.2  2.3  250 0   0   true -32 --- inspect 9.1   5.5   320   .62 0   true -32 --- inspect .68   .68   20    .078 .16  - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .68 .67 36 8.6 31    0      false(valid-memcleanup) 1 wit inspect 5.2  2.9  250 0   0   true -32 --- inspect 8.4   4.7   310   .66 0   error (2) 0 --- inspect .66   .66   20    .078 .41  - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .51 .50 35 5.7 31    0      false(valid-memcleanup) 1 wit inspect 5.8  3.1  270 0   0   true -32 --- inspect 8.7   4.9   320   .62 0   error (2) 0 --- inspect .65   .65   20    .078 0     - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.0  .98 36 14   77    .0041 false(valid-memcleanup) 1 wit inspect 4.4  2.4  250 0   0   true -32 --- inspect 8.0   4.5   320   .66 0   true -32 --- inspect .64   .64   20    .078 0     - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true -32 wit inspect 1.4  1.4  37 18   120    .0041 error (1) 0 --- inspect .70 .41 44 0   0   timeout 0 --- inspect 96     81     640   1.3  0   error (1) 0 --- inspect .091  .090  11    0     0     - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .47 .47 35 6.0 31    0      false(valid-memcleanup) 1 wit inspect 4.2  2.3  250 0   0   true -32 --- inspect 9.4   5.2   310   .62 0   true -32 --- inspect .64   .64   20    .078 0     - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .49 .48 36 6.1 31    0      false(valid-memcleanup) 1 wit inspect 5.7  3.1  250 0   0   true -32 --- inspect 8.7   5.3   330   .62 0   true -32 --- inspect .65   .65   20    .082 .14  - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 2.2  2.2  39 28   150    0      false(valid-memcleanup) 1 wit inspect 8.7  4.6  370 0   0   true -32 --- inspect 8.5   4.7   310   .62 0   true -32 --- inspect .68   .68   21    .090 0     - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.2  1.2  36 14   92    0      false(valid-memcleanup) 1 wit inspect 5.8  3.1  260 0   0   true -32 --- inspect 8.6   4.9   320   .62 0   true -32 --- inspect .65   .65   20    .082 0     - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.3  1.3  39 20   62    0      false(valid-memcleanup) 1 wit inspect 5.1  2.8  250 0   0   true -32 --- inspect 9.9   5.8   320   .62 0   error (2) 0 --- inspect .66   .66   20    .098 0     - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 68    68    1200 730   120    0      timeout 0 --- inspect 98    61    3100 0   0   true -32 --- inspect 9.4   5.5   310   .62 0   error (2) 0 --- inspect .67   .67   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 -32 980   980   14000 6700 1200 .0082 32 29 250 140 11000 0   0   32 -352 530 330 10000 21   0   32 -448 210   210   620 2.7 4.1 0
    correct results 0 29 29 150 79 7600 0   0   0 0 0
        correct true 0 0 0 0 0
        correct false 0 29 29 150 79 7600 0   0   0 0 0
    incorrect results 1 -32 1.4 1.4 37 18 120 .0041 0 11 -352 97 56 3500 6.9 0   14 -448 9.3 9.3 290 1.2 1.2 0
        incorrect true 1 -32 1.4 1.4 37 18 120 .0041 0 11 -352 97 56 3500 6.9 0   14 -448 9.3 9.3 290 1.2 1.2 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) -32 29 -352 -448 0
Run set depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-MemCleanup