Tool ULTIMATE Automizer 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
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.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-03 04:39:25 CET 2017-12-03 05:43:13 CET 2017-12-03 06:05:52 CET 2017-12-03 06:06:56 CET 2017-12-03 05:47:48 CET
Run set uautomizer.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-Arrays
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.2 280 42 false(valid-deref) 1 wit inspect 3.6  250 false(valid-deref) 1 wit inspect 7.1   270   true -32 wit inspect .67   18    - wit inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 4.7 270 40 timeout 0 wit inspect 92    2200 false(valid-deref) 1 wit inspect 6.0   280   true -32 wit inspect .63   18    - wit inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.5 290 45 false(valid-deref) 1 wit inspect 2.3  250 false(valid-deref) 1 wit inspect 7.3   270   false(valid-deref) 1 wit inspect .66   18    - wit inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 4.2 240 35 false(valid-deref) 1 wit inspect 2.8  240 false(valid-deref) 1 wit inspect 5.1   260   false(valid-deref) 1 wit inspect .67   18    - wit inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 11   540 95 false(valid-deref) 1 wit inspect 3.7  250 false(valid-deref) 1 wit inspect 6.4   270   false(valid-deref) 1 wit inspect .66   18    - wit inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 7.3 360 53 error 0 wit inspect 3.8  250 false(valid-deref) 1 wit inspect 8.0   290   true -32 wit inspect .65   18    - wit inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 4.4 250 36 false(valid-deref) 1 wit inspect 3.5  240 false(valid-deref) 1 wit inspect 6.4   270   true -32 wit inspect .59   18    - wit inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 4.3 260 35 false(valid-deref) 1 wit inspect 2.8  250 false(valid-deref) 1 wit inspect 5.0   260   true -32 wit inspect .61   18    - wit inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 10   530 94 false(valid-deref) 1 wit inspect 4.7  250 false(valid-deref) 1 wit inspect 6.3   270   false(valid-deref) 1 wit inspect .67   18    - wit inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect 4.7 280 43 timeout 0 wit inspect 91    2200 false(valid-deref) 1 wit inspect 5.4   270   false(valid-deref) 1 wit inspect .67   18    - wit inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.2 310 48 error 0 wit inspect 4.9  250 false(valid-deref) 1 wit inspect 9.1   280   false(valid-deref) 1 wit inspect .67   18    - wit inspect
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 11   540 89 error 0 wit inspect 3.4  240 false(valid-deref) 1 wit inspect 7.2   280   true -32 wit inspect .65   18    - wit inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.4 290 44 error 0 wit inspect 3.3  250 false(valid-deref) 1 wit inspect 6.7   270   false(valid-deref) 1 wit inspect .66   18    - wit inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.3 280 46 false(valid-deref) 1 wit inspect 3.5  250 true -32 wit inspect 12     510   true -32 wit inspect .68   18    - wit inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.9 280 51 false(valid-deref) 1 wit inspect 3.4  250 false(valid-deref) 1 wit inspect 8.5   300   true -32 wit inspect .73   18    - wit inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.1 290 40 timeout (exception) 0 wit inspect 91    2100 false(valid-deref) 1 wit inspect 5.8   260   true -32 wit inspect .62   18    - wit inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 4.2 250 40 false(valid-deref) 1 wit inspect 3.1  270 false(valid-deref) 1 wit inspect 4.1   270   true -32 wit inspect .63   18    - wit inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   2500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   770 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   760 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 8.3 420 77 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     420  
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 8.7 400 63 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     400  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 11   530 96 - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     520  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 10   520 100 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     490  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   870 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 9.5 540 83 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     490  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   870 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1000 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1200 9900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   930 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   890 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .029 4.8
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 12   540 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 22     520  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 8.8 450 68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     450  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   870 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 12   530 130 - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     520  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   840 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   740 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   780 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   870 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   980 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   960 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   860 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 9.2 520 80 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     450  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   870 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   2300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   790 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   840 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   900 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   900 9100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 19   550 200 - wit inspect - wit inspect - wit inspect true 2 wit inspect 23     510  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 10   540 88 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     500  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 8.7 430 75 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     420  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   770 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   950 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1100 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect 5.4 290 44 error 0 wit inspect 3.3  250 false(valid-deref) 1 wit inspect 6.7   280   false(valid-deref) 1 wit inspect .67   18    - wit inspect
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900   2400 13000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900   2700 13000 error (invalid witness file) 0 wit inspect .82 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900   2600 14000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 69 42 35000 59000 460000 21 10 330 10000 21 -15 120 5200 21 -312 12   330 48 24 180 5900
    correct results 30 42 240 12000 2100 10 10 33 2500 17 17 110 4600 8 8 5.3 150 12 24 180 5700
        correct true 12 24 130 6000 1200 0 0 0 12 24 180 5700
        correct false 18 18 110 5800 920 10 10 33 2500 17 17 110 4600 8 8 5.3 150 0
    incorrect results 0 0 1 -32 12 510 10 -320 6.5 180 0
        incorrect true 0 0 1 -32 12 510 10 -320 6.5 180 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 42 10 -15 -312 24
Run set uautomizer.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-Arrays