Tool ULTIMATE Taipan 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 07:53:44 CET 2017-12-03 08:20:31 CET 2017-12-03 08:37:50 CET 2017-12-03 08:38:58 CET 2017-12-03 08:21:58 CET
Run set utaipan.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.MemSafety-Arrays
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-03_0753.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/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2017-12-03_0753.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 290 45 0 3.2  250 1 6.6   270   -32 .67   18    -
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 4.4 260 36 0 91    2200 1 5.5   260   -32 .59   18    -
array-memsafety/count_down_unsafe_false-valid-deref.i 1 5.8 290 45 0 3.3  250 1 6.2   260   1 .68   18    -
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 4.3 260 35 -32 2.6  240 1 5.6   250   1 .61   18    -
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 16   700 130 0 3.1  250 1 5.2   270   1 .65   18    -
array-memsafety/cstrlen_unsafe_false-valid-deref.i 1 7.4 380 63 0 3.4  250 1 7.9   290   -32 .65   18    -
array-memsafety/cstrncat_unsafe_false-valid-deref.i 1 4.2 260 35 -32 1.9  250 1 5.6   270   -32 .61   18    -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 1 4.5 260 36 1 3.0  250 1 5.1   260   -32 .63   18    -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 14   580 130 0 3.3  250 1 6.3   270   1 .67   18    -
array-memsafety/diff_usafe_false-valid-deref.i 1 4.9 280 44 0 91    2200 1 3.6   280   1 .62   18    -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 6.7 290 52 0 3.2  250 -32 12     500   1 .68   18    -
array-memsafety/lis_unsafe_false-valid-deref.i 1 15   820 130 0 3.5  260 1 6.3   280   -32 .69   18    -
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 6.1 300 44 0 3.3  250 1 6.1   270   1 .67   18    -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 0 11   570 89 0 3.3  250 -32 11     500   -32 .68   18    -
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 6.1 280 49 0 3.5  260 1 8.1   300   -32 .67   18    -
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 4.4 260 39 0 91    2300 1 5.5   260   -32 .62   19    -
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 4.5 250 34 -32 2.9  240 1 5.3   260   -32 .59   18    -
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i 2 41   1200 400 - - - 0 960     2500  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i 2 11   550 83 - - - 0 960     770  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i 0 900   770 12000 - - - 0 .037 4.9
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i 0 900   820 10000 - - - 0 .024 4.9
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i 2 15   690 130 - - - 2 9.8   400  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i 2 17   810 150 - - - 2 14     490  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i 0 900   14000 5600 - - - 0 .044 4.9
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i 2 17   830 150 - - - 2 13     490  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i 0 900   890 12000 - - - 0 .048 4.8
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i 0 900   1100 13000 - - - 0 .048 4.8
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i 0 900   880 11000 - - - 0 .040 4.8
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i 0 900   980 12000 - - - 0 .044 4.8
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i 0 900   2600 13000 - - - 0 .050 4.8
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i 0 900   900 12000 - - - 0 .032 4.9
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i 2 28   1200 260 - - - 0 960     1500  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i 0 900   850 11000 - - - 0 .047 4.8
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i 0 900   890 11000 - - - 0 .049 4.8
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i 0 900   1000 11000 - - - 0 .044 4.8
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i 2 37   1400 360 - - - 2 14     500  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i 2 15   740 120 - - - 2 11     440  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i 0 900   1200 11000 - - - 0 .038 4.8
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i 2 54   1400 600 - - - 2 15     510  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i 2 19   780 140 - - - 0 960     770  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i 2 14   830 130 - - - 0 960     760  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i 0 900   740 10000 - - - 0 .018 4.8
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i 2 13   700 110 - - - 0 960     780  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i 0 900   960 12000 - - - 0 .050 4.8
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i 0 900   2200 11000 - - - 0 .041 4.8
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i 0 900   2000 9200 - - - 0 .033 4.9
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i 0 900   880 11000 - - - 0 .041 4.8
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i 0 900   920 12000 - - - 0 .049 4.8
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i 0 900   860 12000 - - - 0 .044 4.9
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i 2 74   2200 790 - - - 0 960     1100  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i 2 16   670 160 - - - 2 11     490  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i 0 900   800 11000 - - - 0 .033 4.9
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i 0 900   1100 11000 - - - 0 .032 4.8
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i 2 46   1900 450 - - - 0 960     1500  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i 2 17   710 140 - - - 0 960     940  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i 0 900   1100 12000 - - - 0 .018 4.8
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i 0 900   890 11000 - - - 0 .018 5.0
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i 0 900   4600 12000 - - - 0 .018 4.9
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i 0 900   740 11000 - - - 0 .019 4.9
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i 2 34   1600 310 - - - 2 12     510  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i 0 900   750 11000 - - - 0 .020 4.9
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i 2 12   630 110 - - - 0 960     740  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i 0 900   1000 12000 - - - 0 .018 4.8
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i 0 900   1500 13000 - - - 0 .020 4.8
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i 0 900   1000 12000 - - - 0 .060 4.8
array-examples/relax_false-valid-deref.i 1 6.5 310 58 0 3.6  270 1 6.8   270   1 .66   18    -
array-examples/sanfoundry_24_false-valid-deref.i 0 900   2000 14000 0 .53 41 0 .018 4.8 0 .0044 .26 -
array-examples/standard_strcpy_false-valid-deref_ground.i 0 900   1300 12000 0 .57 41 0 .042 4.8 0 .0036 .30 -
array-examples/standard_strcpy_original_false-valid-deref.i 0 900   1200 11000 0 .57 43 0 .046 5.0 0 .0045 .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 53 30000 79000 380000 21 -95 320   11000 21 -48 120 5300 21 -312 12   330 48 16 9700 15000
    correct results 35 53 600 25000 5600 1 1 3.0 250 16 16 96 4300 8 8 5.2 150 8 16 99 3800
        correct true 18 36 480 19000 4600 0 0 0 8 16 99 3800
        correct false 17 17 120 6100 1000 1 1 3.0 250 16 16 96 4300 8 8 5.2 150 0
    correct-unconfimed results 1 0 11 570 89 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 1 0 11 570 89 0 0 0 0
    incorrect results 0 3 -96 7.3 740 2 -64 24 1000 10 -320 6.4 180 0
        incorrect true 0 3 -96 7.3 740 2 -64 24 1000 10 -320 6.4 180 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 53 -95 -48 -312 16
Run set utaipan.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.MemSafety-Arrays