Tool ULTIMATE Taipan 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 14:19:36 CET 2018-12-09 20:52:23 CET 2018-12-09 21:15:16 CET 2018-12-09 21:17:48 CET 2018-12-12 21:23:28 CET 2018-12-09 20:55:36 CET
Run set utaipan.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-utaipan.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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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 8.0 2.7 360 63 .66 0      error 0 wit inspect 3.5  1.9  240 0   0      true -32 --- inspect 12     7.2   420   .62 0      error 0 --- inspect 3.6  2.1  240 0   0      true -32 --- inspect .62   .62   20    .070 0      - --- inspect
loop-acceleration/array3_false-valid-deref.i timeout 0 --- inspect 900   780   2400 11000 .64 0      error (invalid witness file) 0 --- inspect .66 .42 43 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .61 46 0   0      error (invalid witness file) 0 --- inspect .0017 .0020 .39 0     0      - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 53   23   1100 460 .66 0      false(valid-deref) 1 wit inspect 11    6.2  570 0   0      false(valid-deref) 1 --- inspect 62     38     1000   .62 0      unknown 0 --- inspect 12    6.9  560 0   0      timeout 0 --- inspect 96      96      21    .27  0      - --- inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 27   9.8 800 230 .66 0      false(valid-deref) 1 wit inspect 5.9  3.1  270 0   0      false(valid-deref) 1 --- inspect 27     15     640   .62 0      unknown 0 --- inspect 7.2  4.1  270 0   0      error (2) 0 --- inspect .97   .97   21    .62  0      - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 13   3.9 460 90 .66 1.2    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.9 390 .56 .070 
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 12   3.7 450 90 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   7.4 390 .66 0     
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 10   3.2 360 77 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.8 330 .62 0     
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   3.2 380 84 .66 .020  - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.7 320 .62 0     
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   3.5 370 87 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.8 310 .62 0     
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 12   3.8 430 88 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.8 340 .62 .049 
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   3.5 410 92 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   6.6 350 .62 0     
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.3 3.2 380 78 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6 5.2 310 .62 0     
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 10   3.2 380 73 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.5 5.3 310 .66 0     
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.7 3.0 380 82 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.9 310 .66 0     
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.6 2.6 350 66 .66 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.4 5.0 300 .66 0     
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.1 2.7 370 66 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3 4.5 300 .66 0     
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.0 2.9 400 63 .66 38      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.4 300 .66 0     
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.3 2.6 370 65 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.2 4.1 290 .66 0     
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.1 2.7 360 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4 4.2 310 .66 0     
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.1 3.1 370 61 .66 .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3 4.5 300 .62 0     
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.3 3.0 370 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.5 4.2 310 .66 0     
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.3 2.7 350 61 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7 4.3 310 .66 .0082
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.7 2.6 370 67 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3 4.1 300 .66 0     
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.3 2.9 340 59 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.3 300 .62 0     
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.8 2.9 370 67 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.0 300 .62 0     
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.3 2.7 370 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7 5.2 300 .66 0     
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.1 2.9 330 58 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.9 4.4 300 .66 0     
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect 7.6 2.7 360 64 .66 0      false(valid-deref) 1 wit inspect 3.5  2.0  240 0   0      true -32 --- inspect 9.5   5.6   310   .62 0      false(valid-deref) 1 --- inspect 4.5  2.6  250 0   2.9    false(valid-deref) 1 --- inspect .59   .59   20    .049 .0041 - --- inspect
memsafety-ext3/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect 11   4.0 510 83 .66 0      false(valid-deref) 1 wit inspect 3.9  2.2  250 0   0      true -32 --- inspect 8.9   4.9   320   .62 0      false(valid-deref) 1 --- inspect 5.3  3.1  250 0   0      false(valid-deref) 1 --- inspect .63   .63   20    .049 0      - --- inspect
memsafety-ext3/derefInLoop1_false-valid-deref.c false(valid-deref) 1 wit inspect 8.8 3.0 390 73 .66 0      false(valid-deref) 1 wit inspect 3.5  2.0  240 0   0      true -32 --- inspect 13     8.6   340   .62 .0041 false(valid-deref) 1 --- inspect 3.9  2.3  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 13   4.6 490 110 .66 0      false(valid-deref) 1 wit inspect 3.9  2.2  250 0   0      false(valid-deref) 1 --- inspect 8.5   4.8   310   .62 0      unknown 0 --- inspect 4.2  2.4  250 0   .0041 error (2) 0 --- inspect .60   .60   20    .061 0      - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c false(valid-deref) 1 wit inspect 25   9.7 730 220 .66 0      false(valid-deref) 1 wit inspect 4.3  2.4  250 0   .0041 true -32 --- inspect 8.8   5.3   320   .62 .0041 false(valid-deref) 1 --- inspect 5.4  3.1  260 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 60   28   900 620 .66 0      false(valid-deref) 1 wit inspect 5.4  3.0  260 0   0      true -32 --- inspect 9.9   6.0   370   .62 0      false(valid-deref) 1 --- inspect 6.0  3.4  270 0   0      false(valid-deref) 1 --- inspect .64   .64   21    .066 0      - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c true -32 wit inspect 10   3.3 410 92 .66 0      error (1) 0 --- inspect .68 .43 45 0   0      true -32 --- inspect 12     6.9   340   .62 .0041 unknown 0 --- inspect .99 .62 49 0   0      error (1) 0 --- inspect .082  .080  11    0     0      - --- inspect
memsafety-ext3/realloc1_false-valid-deref.c false(valid-deref) 1 wit inspect 15   5.4 600 130 .66 0      false(valid-deref) 1 wit inspect 5.4  3.0  260 0   0      true -32 --- inspect 9.0   5.0   310   .62 0      unknown 0 --- inspect 4.5  2.7  250 0   0      false(valid-deref) 1 --- inspect .62   .63   20    .066 0      - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c false(valid-deref) 0 wit inspect 7.9 2.7 370 57 .66 0      true -32 wit inspect 3.5  2.0  240 0   0      true -32 --- inspect 7.7   4.4   310   .62 0      unknown 0 --- inspect 3.4  1.9  240 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.1 2.7 370 61 .66 0      true -32 wit inspect 3.7  2.1  240 0   0      true -32 --- inspect 9.7   5.5   310   .62 0      unknown 0 --- inspect 3.6  2.0  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 13   4.4 570 120 .66 0      false(valid-deref) 1 wit inspect 4.6  2.6  250 0   0      true -32 --- inspect 77     49     6800   .62 0      false(valid-deref) 1 --- inspect 4.1  2.4  250 0   0      error (2) 0 --- inspect .60   .60   21    .049 0      - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c false(valid-deref) 1 wit inspect 8.6 2.9 370 67 .66 0      false(valid-deref) 1 wit inspect 3.6  2.1  240 0   0      false(valid-deref) 1 --- inspect 7.5   4.5   310   .62 0      false(valid-deref) 1 --- inspect 4.5  2.7  250 0   0      false(valid-deref) 1 --- inspect .60   .60   20    .057 0      - --- inspect
memsafety-ext3/scopes5_false-valid-deref.c false(valid-deref) 1 wit inspect 6.9 2.6 330 57 .66 0      false(valid-deref) 1 wit inspect 4.0  2.2  240 0   0      true -32 --- inspect 7.1   4.0   310   .62 0      false(valid-deref) 1 --- inspect 3.7  2.2  250 0   .0041 error (2) 0 --- inspect .61   .60   20    .049 0      - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c true -32 wit inspect 17   9.6 480 160 .66 0      error (1) 0 --- inspect .82 .50 46 0   0      true -32 --- inspect 17     12     400   .62 0      unknown 0 --- inspect 1.1  .69 52 0   0      error (1) 0 --- inspect .072  .072  11    0     0      - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c true 2 wit inspect 12   4.2 500 94 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14   8.2 490 .62 0     
memsafety-ext3/getNumbers3_true-valid-memsafety.c true 2 wit inspect 10   3.8 470 94 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   6.9 380 .62 0     
memsafety-ext3/getNumbers4_true-valid-memsafety.c true 2 wit inspect 44   20   1100 400 .66 .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 58   37   910 .62 0     
memsafety-ext3/scopes4_true-valid-memsafety.c true 2 wit inspect 15   4.2 530 120 .66 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.4 340 .66 0     
pthread-memsafety/fillarray1_false-valid-deref.i false(valid-deref) 0 wit inspect 16   4.8 680 120 .66 0      error 0 wit inspect 5.0  2.7  260 0   0      error (7) 0 --- inspect 18     10     330   .68 .070  error 0 --- inspect 4.6  2.5  260 0   0      true -32 --- inspect .70   .70   20    .11  0      - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i false(valid-deref) 0 wit inspect 15   4.6 500 120 .66 0      error 0 wit inspect 5.1  2.7  250 0   0      error (7) 0 --- inspect 21     12     330   .71 0      error 0 --- inspect 5.8  3.2  260 0   0      true -32 --- inspect .70   .70   20    .098 0      - --- inspect
pthread-memsafety/list1_false-valid-deref.i unknown 0 --- inspect 60   34   820 580 .71 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .025 .034 5.8 0    0      error (invalid witness file) 0 --- inspect 1.0  .64 48 0   0      error (invalid witness file) 0 --- inspect .0049 .0062 .52 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 3 1600 1000 25000 17000 31   39   21 -52 82   46   4800 0   .0041 21 -412 350 210 14000 12   .082 21 8 90 52 4800 0   2.9 21 -121 110   110   370 1.8  .0041 27 54 300 180 9400 17 .13
    correct results 40 67 550 210 19000 4700 26   39   12 12 59   33   3300 0   .0041 4 4 110 63 2300 2.5 0     8 8 37 22 2000 0   2.9 7 7 4.3 4.3 140 .41 .0041 27 54 300 180 9400 17 .13
        correct true 27 54 290 100 11000 2400 18   39   0 0 0 0 27 54 300 180 9400 17 .13
        correct false 13 13 260 100 7500 2300 8.5 0   12 12 59   33   3300 0   .0041 4 4 110 63 2300 2.5 0     8 8 37 22 2000 0   2.9 7 7 4.3 4.3 140 .41 .0041 0
    correct-unconfimed results 4 0 48 15 1900 360 2.6 0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 4 0 48 15 1900 360 2.6 0   0 0 0 0 0
    incorrect results 2 -64 27 13 890 260 1.3 0   2 -64 7.2 4.1 490 0   0      13 -416 200 120 11000 8.1 .012 0 4 -128 2.6 2.6 81 .32 0      0
        incorrect true 2 -64 27 13 890 260 1.3 0   2 -64 7.2 4.1 490 0   0      13 -416 200 120 11000 8.1 .012 0 4 -128 2.6 2.6 81 .32 0      0
        incorrect false 0 0 0 0 0 0
score (48 tasks, max score: 75) 3 -52 -412 8 -121 54
Run set utaipan.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-Other