Tool DIVINE CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 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-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other
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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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 (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)
loops/invert_string_false-valid-deref.c unknown 0 --- inspect 1.6 1.6 200 21 0      0     error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .026 .026 5.6 0    0      error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0      error (invalid witness file) 0 --- inspect .0068 .0085 .52 0     0      - --- inspect
loop-acceleration/array3_false-valid-deref.i false(valid-memtrack) -16 wit inspect 8.4 8.4 430 89 0      0     timeout (exception) 0 wit inspect 95    65    3100 0   0     true -32 --- inspect 9.8   5.6   320   .66 0      timeout 0 --- inspect 92    85    1900 0   0      false(valid-deref) 1 --- inspect .61   .61   20    .061 0      - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c error - divine failed with exitcode 1 0 --- inspect 1.3 1.3 170 16 0      0     error (invalid witness file) 0 --- inspect .79 .49 41 0   0     error (2) 0 --- inspect .026 .027 5.8 0    0      error (invalid witness file) 0 --- inspect 1.1  .72 47 0   0      error (invalid witness file) 0 --- inspect .0020 .0025 .41 0     0      - --- inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c error - divine failed with exitcode 1 0 --- inspect 1.2 1.2 170 16 0      0     error (invalid witness file) 0 --- inspect .78 .48 42 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .92 .61 47 0   0      error (invalid witness file) 0 --- inspect .0060 .0077 .40 0     0      - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0    0  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      .049 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0    0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.8 0    0  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 18 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   410 9200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   400 8400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.5 0    0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   400 8600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.8 0    0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   400 9000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.5 0    0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   410 9400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   400 9200 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   410 8000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   400 10000 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0    0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c false(valid-memtrack) -16 wit inspect 420   170   480 4600 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   3.7   300   .62 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   430 8500 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0    0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   420 8600 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   410 9400 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 --- inspect 900   230   410 8900 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.5 0    0  
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect 8.4 8.4 430 110 0      0     false(valid-deref) 1 wit inspect 4.4  2.5  240 0   0     true -32 --- inspect 7.4   4.3   310   .66 0      false(valid-deref) 1 --- inspect 4.6  2.7  240 0   2.9    false(valid-deref) 1 --- inspect .61   .61   20    .049 2.3    - --- inspect
memsafety-ext3/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect 8.0 8.0 430 110 0      0     false(valid-deref) 1 wit inspect 4.8  2.6  250 0   0     true -32 --- inspect 10     6.3   330   .62 0      false(valid-deref) 1 --- inspect 5.7  3.3  250 0   0      false(valid-deref) 1 --- inspect .62   .62   20    .049 0      - --- inspect
memsafety-ext3/derefInLoop1_false-valid-deref.c true -32 wit inspect 8.1 8.1 370 93 0      0     error (1) 0 --- inspect .72 .44 43 0   0     false(valid-deref) 1 --- inspect 7.6   4.3   310   .66 0      unknown 0 --- inspect 1.3  .83 50 0   0      error (1) 0 --- inspect .098  .095  11    0     0      - --- inspect
memsafety-ext3/getNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect 8.2 8.2 430 100 0      0     false(valid-deref) 1 wit inspect 5.1  2.8  250 0   0     true -32 --- inspect 9.9   5.9   310   .66 0      unknown 0 --- inspect 4.6  2.6  250 0   0      error (2) 0 --- inspect .59   .59   20    .061 0      - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c false(valid-deref) 1 wit inspect 8.1 8.2 430 110 0      0     false(valid-deref) 1 wit inspect 4.8  2.6  250 0   0     true -32 --- inspect 8.4   5.1   300   .66 0      false(valid-deref) 1 --- inspect 4.7  2.8  250 0   3.0    false(valid-deref) 1 --- inspect .60   .60   20    .057 0      - --- inspect
memsafety-ext3/getNumbers4_false-valid-deref.c false(valid-deref) 1 wit inspect 8.4 8.4 430 110 0      0     false(valid-deref) 1 wit inspect 5.5  3.0  250 0   0     true -32 --- inspect 9.2   5.3   310   .66 .0041 false(valid-deref) 1 --- inspect 5.4  3.2  250 0   .0041 false(valid-deref) 1 --- inspect .65   .69   20    .049 .0041 - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect 8.2 8.2 430 100 0      0     false(valid-deref) 1 wit inspect 4.7  2.6  250 0   0     true -32 --- inspect 12     7.1   340   .66 0      false(valid-deref) 1 --- inspect 4.9  2.8  250 0   0      false(valid-deref) 1 --- inspect .60   .60   20    .057 0      - --- inspect
memsafety-ext3/realloc1_false-valid-deref.c unknown 0 --- inspect 1.5 1.6 200 18 0      0     error (invalid witness file) 0 --- inspect .60 .38 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .97 .63 48 0   0      error (invalid witness file) 0 --- inspect .0057 .0077 .41 0     0      - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c false(valid-deref) 1 wit inspect 8.1 8.1 430 120 0      0     false(valid-deref) 1 wit inspect 3.5  1.9  240 0   0     true -32 --- inspect 9.9   5.8   310   .66 0      false(valid-deref) 1 --- inspect 3.7  2.2  250 0   0      error (2) 0 --- inspect .60   .60   20    .057 0      - --- inspect
memsafety-ext3/scopes2_false-valid-deref.c false(valid-deref) 1 wit inspect 8.5 8.5 430 120 0      0     false(valid-deref) 1 wit inspect 3.9  2.2  240 0   0     true -32 --- inspect 8.1   5.0   310   .66 0      unknown 0 --- inspect 4.8  2.9  240 0   3.1    false(valid-deref) 1 --- inspect .61   .61   20    .061 0      - --- inspect
memsafety-ext3/scopes3_false-valid-deref.c false(valid-deref) 1 wit inspect 8.2 8.2 430 120 0      .17  false(valid-deref) 1 wit inspect 4.5  2.5  250 0   0     true -32 --- inspect 8.3   4.6   310   .66 0      false(valid-deref) 1 --- inspect 4.6  2.7  250 0   0      error (2) 0 --- inspect .60   .60   20    .049 0      - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c false(valid-deref) 1 wit inspect 8.1 8.1 430 110 0      0     false(valid-deref) 1 wit inspect 4.2  2.4  250 0   0     true -32 --- inspect 7.4   4.6   320   .66 0      false(valid-deref) 1 --- inspect 4.0  2.4  250 0   0      false(valid-deref) 1 --- inspect .59   .59   20    .057 0      - --- inspect
memsafety-ext3/scopes5_false-valid-deref.c false(valid-deref) 1 wit inspect 8.2 8.2 430 110 0      0     false(valid-deref) 1 wit inspect 3.5  2.0  240 0   .45  true -32 --- inspect 8.7   5.2   300   .66 0      false(valid-deref) 1 --- inspect 3.9  2.3  240 0   .43   error (2) 0 --- inspect .60   .60   20    .049 0      - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c false(valid-memtrack) -16 wit inspect 8.3 8.3 430 110 0      0     false(valid-free) 1 wit inspect 4.9  2.7  250 0   0     true -32 --- inspect 13     7.2   340   .66 0      unknown 0 --- inspect 5.0  3.0  250 0   0      error (2) 0 --- inspect .60   .60   20    .061 0      - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c true 2 wit inspect 8.2 8.2 370 120 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15     8.5   490   .66 0  
memsafety-ext3/getNumbers3_true-valid-memsafety.c true 2 wit inspect 8.1 8.1 370 110 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.3   380   .66 0  
memsafety-ext3/getNumbers4_true-valid-memsafety.c true 2 wit inspect 8.3 8.2 370 94 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 66     42     850   .62 0  
memsafety-ext3/scopes4_true-valid-memsafety.c true 2 wit inspect 8.2 8.2 370 130 0      .17  - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12     7.1   360   .62 0  
pthread-memsafety/fillarray1_false-valid-deref.i unknown 0 --- inspect 1.6 1.6 200 21 0      0     error (invalid witness file) 0 --- inspect .75 .45 40 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0      error (invalid witness file) 0 --- inspect 1.0  .69 46 0   0      error (invalid witness file) 0 --- inspect .0021 .0023 .40 0     0      - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i unknown 0 --- inspect 1.6 1.6 200 20 0      0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0      error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0      error (invalid witness file) 0 --- inspect .0048 .0061 .41 0     0      - --- inspect
pthread-memsafety/list1_false-valid-deref.i false(valid-memtrack) -16 wit inspect 8.9 8.8 450 92 0      0     error 0 wit inspect 7.0  3.8  250 0   .029 error (7) 0 --- inspect 24     13     340   .75 0      error 0 --- inspect 6.2  3.4  260 0   0      true -32 --- inspect .72   .72   20    .11  .21   - --- 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 (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)
total 48 -77 11000   3100   16000 110000 .049 .39 21 12 160 100 6600 0   .48 21 -415 150   90   4800 9.9  .0041 21 9 160 130 5400 0   9.5 21 -24 8.7  8.7  300 .83 2.5  27 10 110 68 2500 3.2 0  
    correct results 15 19 120   120   6200 1700 0     .34 12 12 54 30 3000 0   .45 1 1 7.6 4.3 310 .66 0      9 9 41 24 2200 0   6.4 8 8 4.9  4.9  160 .44 2.3  5 10 110 67 2400 3.2 0  
        correct true 4 8 33   33   1500 450 0     .17 0 0 0 0 5 10 110 67 2400 3.2 0  
        correct false 11 11 90   91   4700 1200 0     .17 12 12 54 30 3000 0   .45 1 1 7.6 4.3 310 .66 0      9 9 41 24 2200 0   6.4 8 8 4.9  4.9  160 .44 2.3  0
    incorrect results 5 -96 460   200   2100 5000 0     0    0 13 -416 120   72   4100 8.5  .0041 0 1 -32 .72 .72 20 .11 .21 0
        incorrect true 1 -32 8.1 8.1 370 93 0     0    0 13 -416 120   72   4100 8.5  .0041 0 1 -32 .72 .72 20 .11 .21 0
        incorrect false 4 -64 450   190   1800 4900 0     0    0 0 0 0 0
score (48 tasks, max score: 75) -77 12 -415 9 -24 10
Run set divine-smt.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-Other