Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other
Options --witness 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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 false(valid-deref) 1 wit inspect .75  .74  18 7.9  0   0    false(valid-deref) 1 wit inspect 3.9  2.1  240 0   0    false(valid-deref) 1 --- inspect 7.8   4.9   310   .62  0   false(valid-deref) 1 --- inspect 4.0  2.4  250 0   .88 true -32 --- inspect .63   .62   20    .070 0      - --- inspect
loop-acceleration/array3_false-valid-deref.i false(valid-deref) 1 wit inspect 13     13     21 190    0   0    timeout 0 wit inspect 96    70    3500 0   0    true -32 --- inspect 8.6   5.4   310   .62  0   timeout 0 --- inspect 92    85    1800 0   0    false(valid-deref) 1 --- inspect .62   .62   20    .061 .0041 - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c error(unknown, verification-finished) 0 --- inspect 1.9   1.8   110 26    0   .28 error (invalid witness file) 0 --- inspect .59 .36 40 0   0    error (2) 0 --- inspect .022 .023 5.6 0     0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0    error (invalid witness file) 0 --- inspect .0029 .0037 .53 0     0      - --- inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect .94  .93  31 13    0   0    false(valid-deref) 1 wit inspect 8.0  4.2  270 0   0    false(valid-deref) 1 --- inspect 25     15     540   .62  0   unknown 0 --- inspect 5.6  3.2  270 0   .13 error (2) 0 --- inspect .96   .96   21    .62  .13   - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.0   1.0   120 13    0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14   8.2 390 .66 0     
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.0   1.0   120 11    0   .94 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   6.7 390 .62 0     
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .44  .44  39 5.1  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.6 320 .62 0     
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .39  .39  36 4.5  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.9 320 .66 0     
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .38  .37  36 4.7  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   6.8 330 .66 0     
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .53  .53  52 6.6  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   6.8 350 .66 0     
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .53  .53  52 6.6  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   6.2 330 .62 0     
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .24  .24  17 3.1  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.9 4.5 310 .66 0     
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .31  .31  22 5.0  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.1 5.3 320 .66 0     
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .31  .31  22 3.8  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7 5.0 310 .66 0     
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .20  .20  17 2.4  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.8 5.1 300 .66 0     
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .20  16 2.7  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9 5.2 310 .66 0     
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .21  16 2.3  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9 4.9 300 .66 0     
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .20  16 2.4  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.4 5.1 300 .66 0     
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .21  16 2.5  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1 4.5 310 .66 0     
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .21  16 2.7  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.6 4.2 300 .66 .0082
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .21  16 2.6  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0 3.9 300 .62 0     
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .21  16 2.3  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.5 310 .62 0     
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .19  .19  16 2.7  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.4 300 .66 0     
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .19  .19  17 2.2  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6 4.7 300 .66 0     
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .22  .22  16 2.5  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0 3.9 300 .66 0     
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .21  .20  16 2.5  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.5 4.6 300 .66 0     
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .20  .19  17 2.1  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.0 5.3 300 .66 0     
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect .18  .17  16 1.7  0   0    false(valid-deref) 1 wit inspect 3.3  1.8  240 0   0    false(valid-deref) 1 --- inspect 8.0   4.5   310   .62  0   false(valid-deref) 1 --- inspect 3.7  2.2  250 0   3.1  false(valid-deref) 1 --- inspect .60   .61   20    .049 0      - --- inspect
memsafety-ext3/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect .17  .16  15 1.8  0   0    false(valid-deref) 1 wit inspect 3.9  2.2  250 0   0    true -32 --- inspect 8.6   5.0   310   .62  0   false(valid-deref) 1 --- inspect 3.9  2.3  250 0   0    false(valid-deref) 1 --- inspect .60   .60   20    .049 0      - --- inspect
memsafety-ext3/derefInLoop1_false-valid-deref.c false(valid-deref) 1 wit inspect .17  .17  16 1.6  0   0    false(valid-deref) 1 wit inspect 3.5  1.9  240 0   0    false(valid-deref) 1 --- inspect 8.1   4.6   320   .66  0   false(valid-deref) 1 --- inspect 3.7  2.2  240 0   0    true -32 --- inspect .59   .59   20    .049 .0041 - --- inspect
memsafety-ext3/getNumbers1_false-valid-deref.c error(unknown, verification-finished) 0 --- inspect .24  .23  17 2.6  0   0    error (invalid witness file) 0 --- inspect .76 .47 43 0   0    error (2) 0 --- inspect .022 .024 5.7 0     0   error (invalid witness file) 0 --- inspect .90 .59 47 0   0    error (invalid witness file) 0 --- inspect .0017 .0021 .52 0     0      - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c false(valid-deref) 1 wit inspect .18  .17  16 1.8  0   0    false(valid-deref) 1 wit inspect 5.1  2.7  270 0   0    true -32 --- inspect 9.2   5.7   320   .62  0   false(valid-deref) 1 --- inspect 4.1  2.4  250 0   .66 false(valid-deref) 1 --- inspect .60   .60   20    .057 0      - --- inspect
memsafety-ext3/getNumbers4_false-valid-deref.c false(valid-deref) 1 wit inspect .18  .17  15 2.0  0   0    false(valid-deref) 1 wit inspect 4.5  2.4  250 0   0    true -32 --- inspect 8.9   5.5   320   .62  0   false(valid-deref) 1 --- inspect 5.2  3.0  250 0   0    false(valid-deref) 1 --- inspect .60   .61   20    .066 0      - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect .17  .16  15 1.9  0   0    false(valid-deref) 1 wit inspect 3.7  2.1  250 0   .58 true -32 --- inspect 10     6.3   340   .62  0   false(valid-deref) 1 --- inspect 3.9  2.3  250 0   0    false(valid-deref) 1 --- inspect .62   .62   20    .057 0      - --- inspect
memsafety-ext3/realloc1_false-valid-deref.c false(valid-deref) 1 wit inspect .19  .18  16 3.2  0   0    false(valid-deref) 1 wit inspect 3.7  2.1  250 0   0    true -32 --- inspect 9.1   5.2   320   .62  0   unknown 0 --- inspect 4.1  2.5  250 0   0    false(valid-deref) 1 --- inspect .61   .61   20    .057 0      - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c false(valid-deref) 1 wit inspect .16  .15  16 2.0  0   0    false(valid-deref) 1 wit inspect 3.7  2.1  240 0   0    false(valid-deref) 1 --- inspect 7.3   4.1   320   .62  0   false(valid-deref) 1 --- inspect 3.6  2.1  250 0   0    error (2) 0 --- inspect .61   .61   20    .057 0      - --- inspect
memsafety-ext3/scopes2_false-valid-deref.c false(valid-deref) 1 wit inspect .22  .21  18 2.5  0   0    false(valid-deref) 1 wit inspect 3.3  1.9  240 0   0    false(valid-deref) 1 --- inspect 7.3   4.4   300   .62  0   unknown 0 --- inspect 3.7  2.2  240 0   3.2  false(valid-deref) 1 --- inspect .62   .63   20    .061 0      - --- inspect
memsafety-ext3/scopes3_false-valid-deref.c false(valid-deref) 1 wit inspect .16  .15  16 2.0  0   0    false(valid-deref) 1 wit inspect 3.7  2.1  250 0   0    true -32 --- inspect 7.9   4.5   310   .094 0   false(valid-deref) 1 --- inspect 4.0  2.3  250 0   0    error (2) 0 --- inspect .61   .61   20    .049 0      - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c false(valid-deref) 1 wit inspect .16  .15  16 1.9  0   0    false(valid-deref) 1 wit inspect 3.5  2.0  250 0   0    true -32 --- inspect 7.2   4.1   300   .62  0   false(valid-deref) 1 --- inspect 3.6  2.2  250 0   0    false(valid-deref) 1 --- inspect .62   .63   20    .057 0      - --- inspect
memsafety-ext3/scopes5_false-valid-deref.c false(valid-deref) 1 wit inspect .15  .15  16 2.0  0   0    false(valid-deref) 1 wit inspect 4.1  2.3  240 0   0    false(valid-deref) 1 --- inspect 6.9   4.4   300   .66  0   false(valid-deref) 1 --- inspect 3.7  2.1  250 0   .80 error (2) 0 --- inspect .59   .59   20    .049 0      - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c error(unknown, verification-finished) 0 --- inspect .23  .23  18 2.8  0   0    error (invalid witness file) 0 --- inspect .61 .38 41 0   0    error (2) 0 --- inspect .022 .024 5.6 0     0   error (invalid witness file) 0 --- inspect .97 .64 47 0   0    error (invalid witness file) 0 --- inspect .0043 .0055 .40 0     0      - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c true 2 wit inspect .14  .14  15 1.4  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.8 480 .66 0     
memsafety-ext3/getNumbers3_true-valid-memsafety.c true 2 wit inspect .14  .13  15 1.5  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.2 380 .66 0     
memsafety-ext3/getNumbers4_true-valid-memsafety.c true 2 wit inspect .15  .15  16 1.9  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 63   39   930 .62 0     
memsafety-ext3/scopes4_true-valid-memsafety.c true 2 wit inspect .13  .13  17 1.6  0   0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.3 340 .66 0     
pthread-memsafety/fillarray1_false-valid-deref.i unknown 0 --- inspect .089 .088 14 1.0  0   0    error (invalid witness file) 0 --- inspect .73 .44 40 0   0    error (2) 0 --- inspect .021 .022 5.6 0     0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0    error (invalid witness file) 0 --- inspect .0022 .0036 .40 0     0      - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i unknown 0 --- inspect .086 .089 15 .93 0   .59 error (invalid witness file) 0 --- inspect .60 .36 42 0   0    error (2) 0 --- inspect .022 .024 5.6 0     0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0   0    error (invalid witness file) 0 --- inspect .0027 .0035 .40 0     0      - --- inspect
pthread-memsafety/list1_false-valid-deref.i unknown 0 --- inspect .11  .12  19 1.2  0   4.7  error (invalid witness file) 0 --- inspect .60 .38 40 0   0    error (2) 0 --- inspect .021 .022 5.6 0     0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0    error (invalid witness file) 0 --- inspect .0039 .0051 .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 (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 69 28   27   1200 370 0   6.5  21 14 160 100 7200 0   .58 21 -249 140 83 5000 8.9 0   21 11 150 120 5600 0   8.8 21 -55 9.5 9.5 310 1.4  .14   27 54 310 180 9400 17 .0082
    correct results 42 69 25   25   1000 340 0   .94 14 14 58 32 3500 0   .58 7 7 70 41 2400 4.4 0   11 11 43 25 2700 0   5.5 9 9 5.5 5.5 180 .52 .0041 27 54 310 180 9400 17 .0082
        correct true 27 54 8.4 8.3 780 100 0   .94 0 0 0 0 27 54 310 180 9400 17 .0082
        correct false 15 15 17   17   260 240 0   0    14 14 58 32 3500 0   .58 7 7 70 41 2400 4.4 0   11 11 43 25 2700 0   5.5 9 9 5.5 5.5 180 .52 .0041 0
    incorrect results 0 0 8 -256 69 42 2600 4.5 0   0 2 -64 1.2 1.2 40 .12 .0041 0
        incorrect true 0 0 8 -256 69 42 2600 4.5 0   0 2 -64 1.2 1.2 40 .12 .0041 0
        incorrect false 0 0 0 0 0 0
score (48 tasks, max score: 75) 69 14 -249 11 -55 54
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Other