Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 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-01 23:12:01 CET 2017-12-02 00:17:27 CET 2017-12-02 00:48:14 CET 2017-12-02 00:49:56 CET 2017-12-02 00:23:19 CET
Run set map2check.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.MemSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_2312.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/map2check.2017-12-01_2312.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/map2check.2017-12-01_2312.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2017-12-01_2312.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 .54  13 5.9  1 4.6  250 1 7.1   260   1 .67   18    -
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 1.2   13 15    0 91    490 1 5.2   260   1 .71   18    -
array-memsafety/count_down_unsafe_false-valid-deref.i 1 .60  13 7.7  1 3.6  250 1 5.7   260   -32 .83   18    -
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 .57  11 5.7  -32 3.1  240 1 5.4   250   0 .61   18    -
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 .99  14 12    1 4.8  250 -32 16     480   1 .66   18    -
array-memsafety/cstrlen_unsafe_false-valid-deref.i 1 1.8   13 25    1 8.5  400 -32 7.5   260   0 .69   18    -
array-memsafety/cstrncat_unsafe_false-valid-deref.i 1 .67  12 7.3  1 3.4  250 1 5.1   260   -32 .62   18    -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 1 1.1   13 16    1 3.8  260 1 5.7   260   0 .63   18    -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 1.1   14 14    1 4.3  250 -32 6.7   260   1 .84   19    -
array-memsafety/diff_usafe_false-valid-deref.i 1 1.8   14 23    0 98    4300 1 6.8   260   1 .61   18    -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 1.1   14 12    0 91    1900 -32 6.0   240   1 .66   18    -
array-memsafety/lis_unsafe_false-valid-deref.i 0 1.3   14 18    0 .54 43 0 .019 4.9 0 .0015 .27 -
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 1.2   18 16    1 3.9  250 1 7.0   280   -32 .81   18    -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 1 .64  79 9.1  1 4.8  250 -32 7.6   270   -32 .75   18    -
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 .61  29 7.5  1 3.7  250 1 8.0   260   -32 .66   18    -
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 1.3   14 15    0 96    3600 1 6.9   260   1 .61   18    -
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 .83  13 11    1 3.1  240 1 5.7   250   0 .66   18    -
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i 2 .83  13 9.5  - - - 0 960     2400  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i 2 1.2   13 16    - - - 0 960     750  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i 0 890     13 13000    - - - 0 .019 5.0
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i 2 1.5   13 17    - - - 2 11     420  
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i 2 2.2   13 30    - - - 2 11     400  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i 0 900     410 11000    - - - 0 .019 4.9
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i 2 370     25 4500    - - - 0 960     1500  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i 2 6.4   14 78    - - - 2 14     490  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i 0 36     15000 480    - - - 0 .020 4.8
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i 2 2.7   14 30    - - - 0 960     1500  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i 2 3.9   15 45    - - - 0 960     1000  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i 2 2.4   13 30    - - - 2 14     490  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i 2 320     41 3900    - - - 0 960     840  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i 2 240     20 2800    - - - 0 960     850  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i 2 7.4   14 100    - - - 0 960     1500  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i 2 4.9   14 55    - - - 0 960     810  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i 2 5.0   13 52    - - - 0 960     810  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i 2 5.6   14 76    - - - 0 37     490  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i 2 1.4   13 19    - - - 2 15     500  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i 2 2.2   13 25    - - - 2 15     450  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i 2 2.5   14 33    - - - 0 960     760  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i 2 4.1   18 49    - - - 2 21     510  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i 2 120     15 1800    - - - 0 960     790  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i 2 6.2   14 77    - - - 0 960     750  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i 2 6.6   14 80    - - - 0 960     700  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i 2 4.6   13 61    - - - 0 960     800  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i 2 2.3   14 28    - - - 0 960     910  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i 2 7.3   14 78    - - - 0 960     810  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i 2 370     25 4400    - - - 0 960     1100  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i 2 5.4   13 64    - - - 0 960     800  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i 2 2.5   13 37    - - - 0 960     950  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i 2 9.0   13 100    - - - 0 960     820  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i 2 7.3   14 90    - - - 0 960     1100  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i 2 2.4   12 31    - - - 2 13     490  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i 2 330     34 4200    - - - 0 960     760  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i 2 230     18 3100    - - - 0 960     920  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i 2 7.1   13 86    - - - 0 960     1500  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i 2 120     14 1600    - - - 0 960     780  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i 2 7.3   13 110    - - - 0 960     770  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i 2 12     13 160    - - - 0 960     840  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i 2 11     17 140    - - - 0 960     880  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i 2 3.4   13 39    - - - 2 27     500  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i 2 1.8   13 20    - - - 2 15     510  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i 2 2.0   14 27    - - - 2 11     420  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i 2 2.1   13 25    - - - 0 960     730  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i 2 6.6   14 91    - - - 0 960     830  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i 2 5.9   15 66    - - - 0 960     830  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i 2 5.9   15 67    - - - 0 960     1100  
array-examples/relax_false-valid-deref.i 0 .042 11 .39 0 .71 45 0 .022 4.9 0 .0013 .26 -
array-examples/sanfoundry_24_false-valid-deref.i 0 900     470 10000    0 .71 44 0 .019 5.0 0 .0013 .27 -
array-examples/standard_strcpy_false-valid-deref_ground.i 0 18     12 230    0 91    3700 -32 9.4   320   -32 .59   18    -
array-examples/standard_strcpy_original_false-valid-deref.i 0 15     12 220    0 91    3600 -32 9.6   300   -32 .60   18    -
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 106 5100 17000 64000 21 -21 610   21000 21 -213 130 5000 21 -217 12   330 48 22 32000 38000
    correct results 61 106 2300 1000 29000 11 11 48   2900 11 11 69 2900 7 7 4.7 130 11 22 170 5200
        correct true 45 90 2300 700 29000 0 0 0 11 22 170 5200
        correct false 16 16 16 290 200 11 11 48   2900 11 11 69 2900 7 7 4.7 130 0
    correct-unconfimed results 2 0 32 25 450 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 2 0 32 25 450 0 0 0 0
    incorrect results 0 1 -32 3.1 240 7 -224 63 2100 7 -224 4.9 130 0
        incorrect true 0 1 -32 3.1 240 7 -224 63 2100 7 -224 4.9 130 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 106 -21 -213 -217 22
Run set map2check.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.MemSafety-Arrays