Tool ULTIMATE Kojak 0.1.23-635dfa2a 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-08 11:04:44 CET 2018-12-09 20:15:59 CET 2018-12-09 20:59:07 CET 2018-12-09 21:01:30 CET 2018-12-12 21:11:08 CET 2018-12-09 20:36:45 CET
Run set ukojak.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other
Options --full-output -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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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) 0 wit inspect 9.4 3.1 380 80 .66 0      error 0 wit inspect 4.6  2.5  240 0   0      true -32 --- inspect 12     6.9   430   .62 0      error 0 --- inspect 3.4  1.9  240 0   0     true -32 --- inspect .61   .61   20    .070 0      - --- inspect
loop-acceleration/array3_false-valid-deref.i timeout 0 --- inspect 900   750   1900 7200 .65 0      error (invalid witness file) 0 --- inspect .69 .42 41 0   .0041 error (2) 0 --- inspect .022 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .92 .60 47 0   0     error (invalid witness file) 0 --- inspect .0016 .0022 .41 0     0      - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 64   25   1600 570 .66 0      false(valid-deref) 1 wit inspect 13    7.6  550 0   .50   false(valid-deref) 1 --- inspect 53     32     1000   .62 0      unknown 0 --- inspect 11    6.5  550 0   0     timeout 0 --- inspect 96      97      21    .27  0      - --- inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 25   7.8 770 200 .66 .0041 false(valid-deref) 1 wit inspect 6.0  3.2  270 0   0      false(valid-deref) 1 --- inspect 30     17     660   .66 0      unknown 0 --- inspect 6.1  3.5  280 0   0     error (2) 0 --- inspect .96   .96   21    .62  0      - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 25   7.5 690 210 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14     7.9   390   .66 0     
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 23   7.1 810 210 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13     7.7   400   .62 0     
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 21   6.4 790 180 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.8   5.8   320   .66 0     
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 14   4.4 560 110 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12     7.0   330   .66 0     
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 14   4.3 510 100 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.5   330   .62 0     
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 16   5.2 530 120 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12     6.8   350   .62 .049 
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 16   4.9 600 130 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12     6.8   350   .62 0     
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 12   3.5 500 97 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6   4.9   310   .62 0     
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 15   4.3 600 120 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10     5.6   310   .66 .033 
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 13   4.2 570 110 .66 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 true 2 wit inspect 8.7 2.9 360 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1   4.4   300   .66 .0041
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 9.0 2.8 370 76 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4   4.1   300   .66 0     
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 9.3 2.9 370 70 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.6   4.4   300   .54 0     
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.6 2.7 350 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2   4.5   310   .66 0     
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.6 2.8 370 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0   4.9   300   .62 0     
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.7 2.8 360 67 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.6   5.4   320   .62 0     
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 9.7 3.0 370 74 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.1   5.4   310   .66 0     
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.3 3.2 360 71 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3   4.2   300   .66 0     
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.8 2.6 360 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.2   4.5   300   .62 0     
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.2 2.7 370 63 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1   4.4   300   .66 0     
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.5 2.8 370 61 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1   4.5   300   .62 0     
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.1 2.8 340 59 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.6   4.6   320   .66 0     
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.3 2.8 360 77 .66 .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   4.4   300   .62 .0041
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect 8.0 3.1 340 60 .66 0      false(valid-deref) 1 wit inspect 3.5  2.0  240 0   .59   true -32 --- inspect 7.3   4.2   310   .62 0      false(valid-deref) 1 --- inspect 3.7  2.2  250 0   .025 false(valid-deref) 1 --- inspect .59   .59   20    .049 0      - --- inspect
memsafety-ext3/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect 40   23   730 350 .66 0      false(valid-deref) 1 wit inspect 4.4  2.5  250 0   .037  true -32 --- inspect 7.8   4.9   320   .66 0      false(valid-deref) 1 --- inspect 3.8  2.3  250 0   1.0   false(valid-deref) 1 --- inspect .62   .61   20    .049 0      - --- inspect
memsafety-ext3/derefInLoop1_false-valid-deref.c false(valid-deref) 1 wit inspect 7.6 3.1 350 62 .66 0      false(valid-deref) 1 wit inspect 3.8  2.1  240 0   0      true -32 --- inspect 12     8.0   350   .62 0      false(valid-deref) 1 --- inspect 3.7  2.2  250 0   3.5   true -32 --- inspect .61   .60   20    .049 0      - --- inspect
memsafety-ext3/getNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect 18   7.7 720 140 .66 0      false(valid-deref) 1 wit inspect 4.1  2.3  250 0   0      false(valid-deref) 1 --- inspect 7.6   4.3   320   .62 0      unknown 0 --- inspect 5.1  2.9  250 0   .12  error (2) 0 --- inspect .58   .58   20    .061 0      - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c false(valid-deref) 1 wit inspect 60   36   1100 630 .62 0      false(valid-deref) 1 wit inspect 4.9  2.7  250 0   .049  true -32 --- inspect 8.3   5.1   320   .62 0      false(valid-deref) 1 --- inspect 4.2  2.5  250 0   0     false(valid-deref) 1 --- inspect .60   .60   21    .057 0      - --- inspect
memsafety-ext3/getNumbers4_false-valid-deref.c false(valid-deref) 1 wit inspect 320   260   1100 3400 .62 0      false(valid-deref) 1 wit inspect 5.4  2.9  250 0   0      true -32 --- inspect 9.7   5.4   370   .62 0      false(valid-deref) 1 --- inspect 4.4  2.6  250 0   0     false(valid-deref) 1 --- inspect .61   .62   21    .066 0      - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c true -32 wit inspect 11   4.3 490 110 .66 0      error (1) 0 --- inspect .83 .50 44 0   0      true -32 --- inspect 10     6.4   340   .18 .0041 unknown 0 --- inspect 1.0  .65 49 0   0     error (1) 0 --- inspect .074  .075  11    0     0      - --- inspect
memsafety-ext3/realloc1_false-valid-deref.c false(valid-deref) 1 wit inspect 71   46   1000 810 .62 .020  false(valid-deref) 1 wit inspect 4.6  2.5  250 0   0      true -32 --- inspect 8.2   5.1   310   .62 0      unknown 0 --- inspect 3.9  2.4  250 0   0     false(valid-deref) 1 --- inspect .61   .61   21    .057 0      - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c false(valid-deref) 0 wit inspect 8.1 2.7 350 65 .66 0      true -32 wit inspect 4.6  2.5  240 0   0      true -32 --- inspect 7.5   4.3   310   .62 0      unknown 0 --- inspect 3.5  2.0  240 0   0     error (2) 0 --- inspect .61   .60   20    .057 0      - --- inspect
memsafety-ext3/scopes2_false-valid-deref.c false(valid-deref) 1 wit inspect 7.4 2.7 350 55 .66 0      false(valid-deref) 1 wit inspect 4.3  2.4  250 0   0      true -32 --- inspect 8.8   5.0   320   .66 0      unknown 0 --- inspect 3.7  2.2  250 0   0     false(valid-deref) 1 --- inspect .62   .62   20    .061 0      - --- inspect
memsafety-ext3/scopes3_false-valid-deref.c false(valid-deref) 1 wit inspect 13   4.6 500 110 .66 0      false(valid-deref) 1 wit inspect 4.4  2.4  250 0   0      out of memory 0 --- inspect 59     38     7000   .64 0      false(valid-deref) 1 --- inspect 3.8  2.2  250 0   1.0   error (2) 0 --- inspect .63   .62   21    .049 .0041 - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c false(valid-deref) 1 wit inspect 8.6 2.9 370 72 .66 0      false(valid-deref) 1 wit inspect 3.6  2.0  240 0   .0041 false(valid-deref) 1 --- inspect 6.9   4.3   300   .62 0      false(valid-deref) 1 --- inspect 3.8  2.2  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 7.6 2.7 370 67 .66 0      false(valid-deref) 1 wit inspect 4.4  2.4  240 0   0      true -32 --- inspect 7.1   4.4   300   .62 0      false(valid-deref) 1 --- inspect 3.7  2.2  250 0   0     error (2) 0 --- inspect .59   .61   20    .049 0      - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c true -32 wit inspect 27   15   680 290 .66 0      error (1) 0 --- inspect .82 .49 44 0   0      true -32 --- inspect 15     9.9   400   .62 0      unknown 0 --- inspect 1.1  .67 50 0   0     error (1) 0 --- inspect .070  .070  11    0     0      - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c true 2 wit inspect 25   12   800 230 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15     9.4   480   .62 0     
memsafety-ext3/getNumbers3_true-valid-memsafety.c true 2 wit inspect 11   4.7 540 100 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14     7.7   390   .66 0     
memsafety-ext3/getNumbers4_true-valid-memsafety.c timeout 0 --- inspect 900   770   1100 7100 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0     
memsafety-ext3/scopes4_true-valid-memsafety.c true 2 wit inspect 11   3.4 410 95 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12     7.1   370   .66 0     
pthread-memsafety/fillarray1_false-valid-deref.i error (7) 0 --- inspect 16   5.4 370 140 .75 0      error (invalid witness file) 0 --- inspect .70 .43 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0      error (invalid witness file) 0 --- inspect .99 .64 48 0   0     error (invalid witness file) 0 --- inspect .0019 .0024 .52 0     0      - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i error (7) 0 --- inspect 15   5.7 370 120 .75 0      error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .61 46 0   0     error (invalid witness file) 0 --- inspect .0057 .0068 .53 0     0      - --- inspect
pthread-memsafety/list1_false-valid-deref.i error (7) 0 --- inspect 16   6.1 360 140 .75 0      error (invalid witness file) 0 --- inspect .74 .47 40 0   0      error (2) 0 --- inspect .023 .025 5.7 0    0      error (invalid witness file) 0 --- inspect .98 .63 47 0   0     error (invalid witness file) 0 --- inspect .0059 .0078 .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 1 2900 2100   28000 25000 32   .033  21 -19 80   45   4300 0   1.2 21 -380 270 170 13000 10   .0041 21 8 74 44 4300 0   5.7 21 -57 110   110   330 1.6  .0041 27 52 250 150 8600 17 .090
    correct results 39 65 980 540   22000 9300 25   .033  13 13 66   37   3500 0   1.2 4 4 97 58 2300 2.5 0      8 8 31 18 2000 0   5.6 7 7 4.3 4.3 140 .40 0      26 52 250 150 8600 17 .090
        correct true 26 52 330 110   13000 2700 17   .0082 0 0 0 0 26 52 250 150 8600 17 .090
        correct false 13 13 650 430   9200 6600 8.4 .025  13 13 66   37   3500 0   1.2 4 4 97 58 2300 2.5 0      8 8 31 18 2000 0   5.6 7 7 4.3 4.3 140 .40 0      0
    correct-unconfimed results 2 0 18 5.8 730 140 1.3 0      0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 2 0 18 5.8 730 140 1.3 0      0 0 0 0 0
    incorrect results 2 -64 38 19   1200 400 1.3 0      1 -32 4.6 2.5 240 0   0   12 -384 110 69 4100 7.1 .0041 0 2 -64 1.2 1.2 41 .12 0      0
        incorrect true 2 -64 38 19   1200 400 1.3 0      1 -32 4.6 2.5 240 0   0   12 -384 110 69 4100 7.1 .0041 0 2 -64 1.2 1.2 41 .12 0      0
        incorrect false 0 0 0 0 0 0
score (48 tasks, max score: 75) 1 -19 -380 8 -57 52
Run set ukojak.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-Other