Tool 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-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-06 10:57:45 CET 2018-12-12 19:32:16 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other
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 -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../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 (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 error 0 wit inspect 2.7 1.2 240 22 0   0   error (1) 0 --- inspect .89 .53 44 0   0   false(valid-deref) 1 --- inspect 8.0 4.6 310 .66 0   unknown 0 --- inspect .99 .64 49 0   0      error (1) 0 --- inspect .070 .070 11 0     0      - --- inspect
loop-acceleration/array3_false-valid-deref.i timeout 0 wit inspect 900   880   1600 11000 0   0   error (1) 0 --- inspect .74 .46 44 0   0   timeout 0 --- inspect 96   68   780 1.1  0   unknown 0 --- inspect 1.0  .67 50 0   0      error (1) 0 --- inspect .099 .098 11 0     0      - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 11   3.8 550 100 0   0   false(valid-deref) 1 wit inspect 12    6.7  580 0   0   false(valid-deref) 1 --- inspect 53   33   1000 .62 0   unknown 0 --- inspect 12    7.0  580 0   3.1    timeout 0 --- inspect 96     96     21 .28  0      - --- inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 5.6 1.8 290 46 0   0   false(valid-deref) 1 wit inspect 6.1  3.2  270 0   0   false(valid-deref) 1 --- inspect 25   15   550 .62 0   unknown 0 --- inspect 6.3  3.7  290 0   3.1    error (2) 0 --- inspect .97  .99  21 .52  0      - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 33   13   1700 260 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13     7.5   390   .62 0  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 36   13   1800 270 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13     7.4   390   .62 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout (segmentation fault) 0 --- inspect 900   730   7300 8700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 55   29   3200 470 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.4   330   .62 0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 51   29   3300 480 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12     7.1   330   .66 0  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 88   47   4300 770 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.7   350   .66 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 92   47   4300 730 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.3   340   .66 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.6 2.4 420 67 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.6   310   .66 0  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 19   5.0 760 150 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     5.8   320   .66 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 19   5.0 750 150 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.7   5.7   300   .66 0  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   190   11000 5600 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3   4.7   310   .62 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   190   11000 4400 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6   4.7   300   .66 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   190   11000 4900 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7   4.9   300   .66 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   190   11000 4700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.2   4.4   300   .62 0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   520   6300 7900 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0   4.8   310   .66 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   190   11000 4700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7   4.3   310   .66 0  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   500   4200 7200 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7   4.8   300   .66 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   190   11000 5300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.5   300   .66 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   200   11000 4600 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   4.0   300   .66 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   190   11000 5100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.9   4.3   300   .66 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   190   11000 4900 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4   4.6   310   .62 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 920   190   11000 5000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3   4.1   310   .66 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 930   190   11000 5500 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3   4.1   300   .66 0  
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect 2.7 1.3 240 22 0   0   false(valid-deref) 1 wit inspect 3.6  2.0  240 0   0   false(valid-deref) 1 --- inspect 8.6 4.7 320 .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/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect 2.9 1.3 240 29 0   0   false(valid-deref) 1 wit inspect 4.0  2.2  250 0   0   false(valid-deref) 1 --- inspect 12   6.8 410 .66 0   false(valid-deref) 1 --- inspect 4.2  2.4  250 0   .15   false(valid-deref) 1 --- inspect .61  .61  21 .049 0      - --- inspect
memsafety-ext3/derefInLoop1_false-valid-deref.c false(valid-deref) 1 wit inspect 2.9 1.2 250 22 0   0   false(valid-deref) 1 wit inspect 3.9  2.2  240 0   0   false(valid-deref) 1 --- inspect 7.0 4.4 300 .66 0   false(valid-deref) 1 --- inspect 3.7  2.2  240 0   0      true -32 --- inspect .59  .59  20 .049 0      - --- inspect
memsafety-ext3/getNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect 3.0 1.3 240 28 0   0   false(valid-deref) 1 wit inspect 4.1  2.3  250 0   0   out of memory 0 --- inspect 82   53   7000 1.6  0   unknown 0 --- inspect 4.2  2.4  250 0   .14   error (2) 0 --- inspect .59  .59  21 .061 0      - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c false(valid-deref) 1 wit inspect 3.6 1.4 280 29 0   0   false(valid-deref) 1 wit inspect 4.7  2.6  250 0   0   false(valid-deref) 1 --- inspect 10   5.6 430 .66 0   false(valid-deref) 1 --- inspect 4.9  2.8  270 0   3.1    false(valid-deref) 1 --- inspect .61  .62  21 .057 2.2    - --- inspect
memsafety-ext3/getNumbers4_false-valid-deref.c false(valid-deref) 1 wit inspect 3.4 1.4 250 30 0   0   false(valid-deref) 1 wit inspect 5.4  2.9  260 0   0   false(valid-deref) 1 --- inspect 12   6.7 520 .62 0   false(valid-deref) 1 --- inspect 4.9  2.8  260 0   0      false(valid-deref) 1 --- inspect .66  .66  21 .066 .0041 - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect 2.9 1.2 240 29 0   0   true -32 wit inspect 4.6  2.6  250 0   0   true -32 --- inspect 10   5.8 340 .66 0   unknown 0 --- inspect 3.8  2.1  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 3.1 1.4 240 28 0   0   false(valid-deref) 1 wit inspect 4.9  2.7  250 0   0   true -32 --- inspect 9.4 5.3 320 .62 0   unknown 0 --- inspect 4.2  2.5  250 0   0      false(valid-deref) 1 --- inspect .60  .61  21 .057 .46   - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c false(valid-deref) 1 wit inspect 2.9 1.3 250 25 0   0   false(valid-deref) 1 wit inspect 4.1  2.3  240 0   0   false(valid-deref) 1 --- inspect 7.0 4.4 310 .66 0   false(valid-deref) 1 --- inspect 3.7  2.3  260 0   .0041 error (2) 0 --- inspect .60  .60  20 .057 0      - --- inspect
memsafety-ext3/scopes2_false-valid-deref.c false(valid-deref) 1 wit inspect 2.7 1.2 250 25 0   0   false(valid-deref) 1 wit inspect 3.5  1.9  250 0   0   false(valid-deref) 1 --- inspect 7.4 4.7 320 .62 0   unknown 0 --- inspect 4.0  2.4  250 0   0      false(valid-deref) 1 --- inspect .60  .60  20 .061 0      - --- inspect
memsafety-ext3/scopes3_false-valid-deref.c false(valid-deref) 1 wit inspect 3.0 1.3 250 27 0   0   false(valid-deref) 1 wit inspect 4.7  2.6  250 0   0   out of memory 0 --- inspect 73   47   7000 .65 0   false(valid-deref) 1 --- inspect 4.2  2.4  250 0   .0041 error (2) 0 --- inspect .62  .62  21 .049 0      - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c false(valid-deref) 1 wit inspect 2.7 1.2 250 24 0   0   false(valid-deref) 1 wit inspect 3.7  2.0  250 0   0   false(valid-deref) 1 --- inspect 7.6 4.8 310 .62 0   false(valid-deref) 1 --- inspect 3.8  2.2  250 0   3.1    false(valid-deref) 1 --- inspect .59  .60  20 .057 0      - --- inspect
memsafety-ext3/scopes5_false-valid-deref.c false(valid-deref) 1 wit inspect 2.8 1.2 250 28 0   0   false(valid-deref) 1 wit inspect 4.1  2.3  240 0   0   true -32 --- inspect 6.7 3.9 300 .62 0   false(valid-deref) 1 --- inspect 3.6  2.1  250 0   3.1    error (2) 0 --- inspect .59  .59  20 .049 0      - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c false(valid-free) 1 wit inspect 2.9 1.3 250 29 0   0   false(valid-free) 1 wit inspect 4.5  2.5  250 0   0   true -32 --- inspect 17   11   470 .66 0   unknown 0 --- inspect 4.6  2.8  250 0   3.6    error (2) 0 --- inspect .64  .64  21 .061 .16   - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c true 2 wit inspect 3.0 1.3 250 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13     8.0   470   .62 0  
memsafety-ext3/getNumbers3_true-valid-memsafety.c true 2 wit inspect 3.1 1.3 270 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.4   380   .66 0  
memsafety-ext3/getNumbers4_true-valid-memsafety.c true 2 wit inspect 3.4 1.4 250 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 67     43     990   .62 0  
memsafety-ext3/scopes4_true-valid-memsafety.c true 2 wit inspect 2.8 1.2 250 23 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.8   340   .62 0  
pthread-memsafety/fillarray1_false-valid-deref.i error 0 wit inspect 4.4 1.5 290 41 0   0   error (1) 0 --- inspect .86 .52 44 0   0   error (7) 0 --- inspect 18   11   330 .68 0   unknown 0 --- inspect 1.0  .63 49 0   0      error (1) 0 --- inspect .079 .079 11 0     0      - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i error 0 wit inspect 4.2 1.5 280 36 0   0   error (1) 0 --- inspect .86 .53 44 0   0   error (7) 0 --- inspect 17   10   320 .71 0   unknown 0 --- inspect .98 .65 49 0   0      error (1) 0 --- inspect .078 .078 11 0     .049  - --- inspect
pthread-memsafety/list1_false-valid-deref.i error 0 wit inspect 4.2 1.4 280 39 0   0   error (1) 0 --- inspect .68 .42 43 0   0   error (7) 0 --- inspect 19   12   350 .71 0   unknown 0 --- inspect 1.0  .67 49 0   0      error (1) 0 --- inspect .070 .072 11 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 42 14000 5000 170000 94000 0   0   21 -17 82   45   4500 0   0   21 -117 510 320 22000 15   0   21 9 81 48 4600 0   20   21 -24 110    110    380 1.6   2.9 27 52 300 180 9200 17 0  
    correct results 29 42 470 220 26000 4000 0   0   15 15 73   40   4100 0   0   11 11 160 94 4800 7.0 0   9 9 37 22 2300 0   9.5 8 8 4.9  4.9  160 .45  2.7 26 52 300 180 9200 17 0  
        correct true 13 26 410 190 22000 3500 0   0   0 0 0 0 26 52 300 180 9200 17 0  
        correct false 16 16 58 24 4300 520 0   0   15 15 73   40   4100 0   0   11 11 160 94 4800 7.0 0   9 9 37 22 2300 0   9.5 8 8 4.9  4.9  160 .45  2.7 0
    incorrect results 0 1 -32 4.6 2.6 250 0   0   4 -128 44 26 1400 2.6 0   0 1 -32 .59 .59 20 .049 0   0
        incorrect true 0 1 -32 4.6 2.6 250 0   0   4 -128 44 26 1400 2.6 0   0 1 -32 .59 .59 20 .049 0   0
        incorrect false 0 0 0 0 0 0
score (48 tasks, max score: 75) 42 -17 -117 9 -24 52
Run set cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-Other