Tool ULTIMATE Kojak 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* [apollon037; apollon054; apollon077; apollon078; apollon115] 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:40:15 CET 2017-12-03 05:43:12 CET 2017-12-03 06:07:12 CET 2017-12-03 06:08:25 CET 2017-12-03 05:47:35 CET
Run set ukojak.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-Arrays
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_0440.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/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_0440.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 1 5.7 320 45 0 2.4  250 1 6.5   260   -32 .63   18    -
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 5.0 260 45 0 91    2300 1 5.3   270   -32 .60   18    -
array-memsafety/count_down_unsafe_false-valid-deref.i 1 5.6 300 45 0 3.4  250 1 7.3   280   1 .65   18    -
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 4.6 250 41 -32 2.8  240 1 5.2   260   1 .62   18    -
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 8.9 470 78 0 5.2  250 1 5.5   260   1 .66   18    -
array-memsafety/cstrlen_unsafe_false-valid-deref.i 1 10   530 85 0 3.4  250 1 7.5   290   -32 .63   18    -
array-memsafety/cstrncat_unsafe_false-valid-deref.i 1 4.7 260 38 -32 2.9  250 1 4.1   260   -32 .59   18    -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 1 4.7 260 41 1 2.8  250 1 5.3   260   -32 .59   18    -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 9.9 550 79 0 3.4  250 1 5.8   270   1 .66   19    -
array-memsafety/diff_usafe_false-valid-deref.i 1 4.9 290 43 0 91    2300 1 5.3   260   1 .60   18    -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 6.8 330 54 0 3.6  250 -32 13     490   1 .65   18    -
array-memsafety/lis_unsafe_false-valid-deref.i 0 900   1500 8600 0 .53 42 0 .019 4.8 0 .0012 .26 -
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 6.1 330 46 0 3.8  270 1 5.9   260   1 .66   18    -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 0 11   590 110 0 3.6  250 -32 13     500   -32 .65   18    -
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 5.8 310 49 0 3.5  250 1 6.0   300   -32 .65   18    -
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 5.0 260 45 0 91    2200 1 5.9   270   -32 .60   18    -
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 4.4 250 36 -32 4.3  250 1 4.1   260   -32 .59   18    -
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i 0 900   2300 13000 - - - 0 .019 4.9
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i 2 22   760 220 - - - 0 960     730  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i 2 20   720 180 - - - 0 960     740  
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i 0 900   2000 12000 - - - 0 .019 4.9
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i 2 56   1200 710 - - - 2 11     400  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i 2 64   1400 780 - - - 2 14     520  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i 0 900   1200 11000 - - - 0 .019 4.8
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i 2 43   1200 610 - - - 2 16     490  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i 2 220   1400 2900 - - - 0 960     830  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i 2 100   1300 1400 - - - 0 960     1500  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i 0 900   1700 11000 - - - 0 .020 4.9
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i 2 21   790 230 - - - 2 12     490  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i 0 900   1700 12000 - - - 0 .019 4.8
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i 2 260   1200 3300 - - - 0 960     1100  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i 0 900   1300 7000 - - - 0 .048 5.0
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i 0 900   1600 14000 - - - 0 .018 4.9
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i 0 900   1700 12000 - - - 0 .018 4.9
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i 0 900   1200 6500 - - - 0 .021 4.8
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i 2 76   1300 880 - - - 2 15     520  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i 2 36   970 350 - - - 2 7.6   430  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i 0 900   1800 13000 - - - 0 .021 4.8
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i 0 900   1300 5700 - - - 0 .019 5.0
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i 2 47   650 540 - - - 0 960     790  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i 2 36   820 460 - - - 0 960     720  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i 2 61   700 720 - - - 0 960     760  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i 2 16   650 140 - - - 0 960     780  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i 2 77   1400 1000 - - - 0 960     950  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i 0 900   1500 13000 - - - 0 .019 4.9
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i 0 900   1300 13000 - - - 0 .021 4.8
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i 2 260   1400 3900 - - - 0 960     780  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i 2 77   1400 1100 - - - 0 960     910  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i 0 900   1200 11000 - - - 0 .019 4.9
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i 2 610   1200 7400 - - - 0 960     1500  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i 2 22   800 260 - - - 2 14     500  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i 0 900   1500 11000 - - - 0 .020 4.9
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i 2 270   1500 3600 - - - 0 960     1100  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i 0 900   1200 6200 - - - 0 .019 4.8
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i 2 32   980 380 - - - 0 960     780  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i 0 900   1700 12000 - - - 0 .019 4.8
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i 0 900   1200 7000 - - - 0 .022 5.0
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i 0 900   1100 11000 - - - 0 .029 4.9
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i 2 27   870 280 - - - 2 22     490  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i 0 900   2700 11000 - - - 0 .019 4.9
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i 2 8.7 470 77 - - - 2 11     420  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i 2 30   970 310 - - - 0 960     740  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i 2 54   1300 630 - - - 0 960     780  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i 2 420   1400 6600 - - - 0 960     840  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i 0 900   1300 11000 - - - 0 .019 4.8
array-examples/relax_false-valid-deref.i 1 6.2 310 53 0 3.6  260 1 7.1   280   1 .66   18    -
array-examples/sanfoundry_24_false-valid-deref.i 0 900   5800 12000 0 .55 44 0 .021 5.0 0 .0011 .34 -
array-examples/standard_strcpy_false-valid-deref_ground.i 0 900   5700 15000 0 .54 41 0 .020 4.9 0 .0011 .34 -
array-examples/standard_strcpy_original_false-valid-deref.i 0 900   5200 11000 0 .70 43 0 .019 4.8 0 .0013 .26 -
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 70 26000 85000 310000 21 -95 320   10000 21 -49 110 5100 21 -280 11   310 48 18 17000 21000
    correct results 43 70 3100 34000 40000 1 1 2.8 250 15 15 87 4000 8 8 5.2 150 9 18 120 4300
        correct true 27 54 3000 29000 39000 0 0 0 9 18 120 4300
        correct false 16 16 99 5300 820 1 1 2.8 250 15 15 87 4000 8 8 5.2 150 0
    correct-unconfimed results 1 0 11 590 110 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 1 0 11 590 110 0 0 0 0
    incorrect results 0 3 -96 9.9 740 2 -64 26 990 9 -288 5.5 170 0
        incorrect true 0 3 -96 9.9 740 2 -64 26 990 9 -288 5.5 170 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 70 -95 -49 -280 18
Run set ukojak.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-Arrays