Tool ULTIMATE Automizer 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 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET 2018-12-09 21:08:07 CET 2018-12-12 21:10:19 CET 2018-12-09 20:42:29 CET
Run set uautomizer.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-uautomizer.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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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.3 2.9 350 63 .66 0      error 0 wit inspect 4.5  2.5  250 0   .45  true -32 --- inspect 12     7.2   430   .62 0      error 0 --- inspect 3.6  2.1  240 0   0      true -32 --- inspect .64   .64   20    .070 0      - --- inspect
loop-acceleration/array3_false-valid-deref.i timeout 0 --- inspect 900   840   850 9700 .64 0      error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .97 .62 48 0   0      error (invalid witness file) 0 --- inspect .0019 .0024 .54 0     0      - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 69   30   1400 560 .66 0      false(valid-deref) 1 wit inspect 12    6.6  570 0   0     false(valid-deref) 1 --- inspect 56     33     1000   .62 0      unknown 0 --- inspect 12    7.4  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 26   10   830 240 .66 0      false(valid-deref) 1 wit inspect 6.5  3.4  270 0   0     false(valid-deref) 1 --- inspect 23     14     650   .62 0      unknown 0 --- inspect 7.0  3.9  280 0   .66   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 12   3.6 460 90 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.7 390 .66 0    
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 12   3.5 480 98 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   7.2 380 .66 0    
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   3.3 390 88 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.6 320 .66 0    
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.9 3.0 360 68 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.9 320 .62 0    
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 10   3.2 370 85 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   7.0 330 .66 0    
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   3.6 390 87 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   6.2 350 .66 0    
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   3.6 430 84 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   7.2 350 .62 0    
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.9 3.2 370 65 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6 4.8 310 .62 0    
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.9 3.5 380 87 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.9 5.9 310 .62 0    
ntdrivers-simplified/kbfiltr_simpl2_true-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.4 5.3 310 .62 0    
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.6 2.6 360 57 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0 4.4 300 .66 0    
locks/test_locks_11_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 8.9 4.9 310 .62 0    
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.2 2.6 360 63 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.6 4.3 300 .66 0    
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.9 2.6 370 63 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2 4.7 310 .66 0    
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.5 2.7 340 54 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.1 5.3 310 .66 0    
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.4 2.7 370 62 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.9 4.5 310 .66 0    
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.6 2.6 360 68 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.2 5.0 300 .62 0    
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.1 2.5 320 61 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.8 4.9 310 .66 0    
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.0 2.9 340 52 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.5 4.6 300 .66 0    
locks/test_locks_6_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.8 4.7 300 .66 0    
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 8.1 2.7 360 60 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7 5.2 300 .66 0    
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.1 2.6 340 53 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3 4.6 310 .66 0    
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 7.7 2.6 360 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.3 5.4 300 .66 0    
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect 8.6 3.5 380 69 .66 0      false(valid-deref) 1 wit inspect 4.2  2.3  240 0   0     true -32 --- inspect 7.6   4.4   320   .66 0      false(valid-deref) 1 --- inspect 4.1  2.4  240 0   0      false(valid-deref) 1 --- inspect .59   .59   20    .049 0      - --- inspect
memsafety-ext3/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect 11   4.2 460 91 .66 0      false(valid-deref) 1 wit inspect 3.9  2.1  250 0   0     true -32 --- inspect 8.4   5.1   310   .62 .0041 false(valid-deref) 1 --- inspect 4.2  2.5  240 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.3 2.8 380 71 .66 0      false(valid-deref) 1 wit inspect 3.6  2.0  240 0   0     true -32 --- inspect 12     8.6   330   .62 0      false(valid-deref) 1 --- inspect 3.9  2.3  250 0   0      true -32 --- inspect .59   .58   20    .049 0      - --- inspect
memsafety-ext3/getNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect 14   4.2 540 99 .66 0      false(valid-deref) 1 wit inspect 4.2  2.3  250 0   .45  false(valid-deref) 1 --- inspect 8.6   5.2   320   .62 0      unknown 0 --- inspect 4.6  2.6  250 0   .074  error (2) 0 --- inspect .61   .61   21    .061 0      - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c false(valid-deref) 1 wit inspect 22   8.6 550 190 .66 0      false(valid-deref) 1 wit inspect 4.7  2.5  260 0   0     true -32 --- inspect 8.9   5.0   330   .62 0      false(valid-deref) 1 --- inspect 4.8  2.8  270 0   0      false(valid-deref) 1 --- inspect .61   .61   21    .057 0      - --- inspect
memsafety-ext3/getNumbers4_false-valid-deref.c false(valid-deref) 1 wit inspect 59   34   770 590 .62 0      false(valid-deref) 1 wit inspect 6.1  3.3  260 0   0     true -32 --- inspect 9.3   5.7   380   .62 0      false(valid-deref) 1 --- inspect 5.3  3.0  260 0   3.8    false(valid-deref) 1 --- inspect .62   .63   21    .066 0      - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c true -32 wit inspect 9.8 3.6 390 77 .66 0      error (1) 0 --- inspect .93 .56 45 0   0     true -32 --- inspect 11     6.1   340   .62 0      unknown 0 --- inspect 1.2  .78 50 0   0      error (1) 0 --- inspect .073  .073  12    0     0      - --- inspect
memsafety-ext3/realloc1_false-valid-deref.c false(valid-deref) 1 wit inspect 15   4.7 550 120 .66 0      false(valid-deref) 1 wit inspect 5.3  2.9  270 0   0     true -32 --- inspect 8.0   5.0   310   .62 0      unknown 0 --- inspect 4.8  2.8  270 0   .0041 false(valid-deref) 1 --- inspect .62   .62   20    .066 0      - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c false(valid-deref) 0 wit inspect 7.8 2.6 360 71 .66 0      true -32 wit inspect 4.2  2.3  240 0   0     true -32 --- inspect 7.7   4.8   320   .62 0      unknown 0 --- inspect 3.5  2.1  240 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 7.6 2.7 350 60 .66 0      true -32 wit inspect 4.5  2.5  250 0   0     true -32 --- inspect 8.2   5.1   310   .66 0      unknown 0 --- inspect 4.1  2.3  250 0   0      false(valid-deref) 1 --- inspect .63   .65   20    .061 .0041 - --- inspect
memsafety-ext3/scopes3_false-valid-deref.c false(valid-deref) 1 wit inspect 12   3.9 480 110 .66 0      false(valid-deref) 1 wit inspect 4.9  2.7  250 0   .016 out of memory 0 --- inspect 59     38     7000   1.0  0      false(valid-deref) 1 --- inspect 4.2  2.4  250 0   .20   error (2) 0 --- inspect .60   .60   21    .049 0      - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c false(valid-deref) 1 wit inspect 8.7 3.2 370 66 .66 .0041 false(valid-deref) 1 wit inspect 4.5  2.5  250 0   0     false(valid-deref) 1 --- inspect 7.0   4.4   310   .66 0      false(valid-deref) 1 --- inspect 4.3  2.5  240 0   .0041 false(valid-deref) 1 --- inspect .62   .61   20    .057 0      - --- inspect
memsafety-ext3/scopes5_false-valid-deref.c false(valid-deref) 1 wit inspect 7.7 2.6 350 67 .66 0      false(valid-deref) 1 wit inspect 4.1  2.3  240 0   0     true -32 --- inspect 7.2   4.1   310   .62 0      false(valid-deref) 1 --- inspect 3.5  2.1  240 0   3.6    error (2) 0 --- inspect .61   .61   20    .049 0      - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c true -32 wit inspect 13   6.8 430 140 .66 0      error (1) 0 --- inspect .78 .46 47 0   0     true -32 --- inspect 15     10     400   .62 0      unknown 0 --- inspect 1.3  .80 49 0   0      error (1) 0 --- inspect .079  .079  11    0     0      - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c true 2 wit inspect 12   4.1 530 110 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.8 490 .66 0    
memsafety-ext3/getNumbers3_true-valid-memsafety.c true 2 wit inspect 9.5 3.7 400 73 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.2 400 .62 0    
memsafety-ext3/getNumbers4_true-valid-memsafety.c true 2 wit inspect 45   21   1100 480 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 70   44   810 .62 .012
memsafety-ext3/scopes4_true-valid-memsafety.c true 2 wit inspect 11   3.5 400 79 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.7 340 .66 0    
pthread-memsafety/fillarray1_false-valid-deref.i error (7) 0 --- inspect 17   5.8 360 120 .75 0      error (invalid witness file) 0 --- inspect .69 .42 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0      error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0      error (invalid witness file) 0 --- inspect .0018 .0023 .52 0     0      - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i error (7) 0 --- inspect 17   5.6 370 140 .75 0      error (invalid witness file) 0 --- inspect .77 .47 42 0   0     error (2) 0 --- inspect .020 .021 5.7 0    0      error (invalid witness file) 0 --- inspect 1.2  .78 48 0   0      error (invalid witness file) 0 --- inspect .0016 .0021 .41 0     0      - --- inspect
pthread-memsafety/list1_false-valid-deref.i error (7) 0 --- inspect 17   5.7 390 140 .75 0      error (invalid witness file) 0 --- inspect .70 .41 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .62 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0022 .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 1500 1100   22000 15000 32   .0041 21 -52 81   45   4300 0   .92 21 -380 270 170 13000 11   .0041 21 8 81 48 4400 0   8.3 21 -57 110   110   330 1.6  .0041 27 54 330 190 9400 17 .012
    correct results 40 67 550 210   18000 4700 26   .0041 12 12 64   35   3300 0   .47 4 4 95 57 2300 2.5 0      8 8 34 20 2000 0   7.6 7 7 4.3 4.3 140 .41 .0041 27 54 330 190 9400 17 .012
        correct true 27 54 290 100   11000 2300 18   0      0 0 0 0 27 54 330 190 9400 17 .012
        correct false 13 13 270 110   7400 2300 8.5 .0041 12 12 64   35   3300 0   .47 4 4 95 57 2300 2.5 0      8 8 34 20 2000 0   7.6 7 7 4.3 4.3 140 .41 .0041 0
    correct-unconfimed results 2 0 16 5.5 710 130 1.3 0      0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 2 0 16 5.5 710 130 1.3 0      0 0 0 0 0
    incorrect results 2 -64 23 10   830 220 1.3 0      2 -64 8.7 4.8 490 0   0    12 -384 120 71 4100 7.5 .0041 0 2 -64 1.2 1.2 41 .12 0      0
        incorrect true 2 -64 23 10   830 220 1.3 0      2 -64 8.7 4.8 490 0   0    12 -384 120 71 4100 7.5 .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) 3 -52 -380 8 -57 54
Run set uautomizer.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-Other