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 false(valid-deref) 1 wit inspect .54  13 5.9  false(valid-deref) 1 wit inspect 4.6  250 false(valid-deref) 1 wit inspect 7.1   260   false(valid-deref) 1 wit inspect .67   18    - wit inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.2   13 15    timeout (exception) 0 wit inspect 91    490 false(valid-deref) 1 wit inspect 5.2   260   false(valid-deref) 1 wit inspect .71   18    - wit inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .60  13 7.7  false(valid-deref) 1 wit inspect 3.6  250 false(valid-deref) 1 wit inspect 5.7   260   true -32 wit inspect .83   18    - wit inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .57  11 5.7  true -32 wit inspect 3.1  240 false(valid-deref) 1 wit inspect 5.4   250   error (2) 0 wit inspect .61   18    - wit inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .99  14 12    false(valid-deref) 1 wit inspect 4.8  250 true -32 wit inspect 16     480   false(valid-deref) 1 wit inspect .66   18    - wit inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.8   13 25    false(valid-deref) 1 wit inspect 8.5  400 true -32 wit inspect 7.5   260   error (2) 0 wit inspect .69   18    - wit inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .67  12 7.3  false(valid-deref) 1 wit inspect 3.4  250 false(valid-deref) 1 wit inspect 5.1   260   true -32 wit inspect .62   18    - wit inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.1   13 16    false(valid-deref) 1 wit inspect 3.8  260 false(valid-deref) 1 wit inspect 5.7   260   error (2) 0 wit inspect .63   18    - wit inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.1   14 14    false(valid-deref) 1 wit inspect 4.3  250 true -32 wit inspect 6.7   260   false(valid-deref) 1 wit inspect .84   19    - wit inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.8   14 23    timeout 0 wit inspect 98    4300 false(valid-deref) 1 wit inspect 6.8   260   false(valid-deref) 1 wit inspect .61   18    - wit inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.1   14 12    timeout (exception) 0 wit inspect 91    1900 true -32 wit inspect 6.0   240   false(valid-deref) 1 wit inspect .66   18    - wit inspect
array-memsafety/lis_unsafe_false-valid-deref.i unknown 0 wit inspect 1.3   14 18    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.2   18 16    false(valid-deref) 1 wit inspect 3.9  250 false(valid-deref) 1 wit inspect 7.0   280   true -32 wit inspect .81   18    - wit inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .64  79 9.1  false(valid-deref) 1 wit inspect 4.8  250 true -32 wit inspect 7.6   270   true -32 wit inspect .75   18    - wit inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .61  29 7.5  false(valid-deref) 1 wit inspect 3.7  250 false(valid-deref) 1 wit inspect 8.0   260   true -32 wit inspect .66   18    - wit inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.3   14 15    timeout 0 wit inspect 96    3600 false(valid-deref) 1 wit inspect 6.9   260   false(valid-deref) 1 wit inspect .61   18    - wit inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .83  13 11    false(valid-deref) 1 wit inspect 3.1  240 false(valid-deref) 1 wit inspect 5.7   250   error (2) 0 wit inspect .66   18    - wit inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect .83  13 9.5  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2400  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 1.2   13 16    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     750  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890     13 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 1.5   13 17    - 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 2.2   13 30    - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     400  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i unknown 0 wit inspect 900     410 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 370     25 4500    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1500  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 6.4   14 78    - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     490  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i out of memory 0 wit inspect 36     15000 480    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.7   14 30    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1500  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 3.9   15 45    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1000  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.4   13 30    - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     490  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 320     41 3900    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     840  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 240     20 2800    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     850  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 7.4   14 100    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1500  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 4.9   14 55    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     810  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 5.0   13 52    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     810  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 5.6   14 76    - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 37     490  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 1.4   13 19    - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     500  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.2   13 25    - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     450  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.5   14 33    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     760  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 4.1   18 49    - wit inspect - wit inspect - wit inspect true 2 wit inspect 21     510  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 120     15 1800    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     790  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 6.2   14 77    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     750  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 6.6   14 80    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     700  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 4.6   13 61    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     800  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.3   14 28    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     910  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 7.3   14 78    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     810  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 370     25 4400    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 5.4   13 64    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     800  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.5   13 37    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     950  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 9.0   13 100    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     820  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 7.3   14 90    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.4   12 31    - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     490  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 330     34 4200    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     760  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 230     18 3100    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     920  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 7.1   13 86    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1500  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 120     14 1600    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     780  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 7.3   13 110    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     770  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 12     13 160    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     840  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 11     17 140    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     880  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 3.4   13 39    - wit inspect - wit inspect - wit inspect true 2 wit inspect 27     500  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 1.8   13 20    - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     510  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.0   14 27    - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     420  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 2.1   13 25    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     730  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 6.6   14 91    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     830  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 5.9   15 66    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     830  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect 5.9   15 67    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
array-examples/relax_false-valid-deref.i unknown 0 wit inspect .042 11 .39 error (invalid witness file) 0 wit inspect .71 45 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
array-examples/sanfoundry_24_false-valid-deref.i unknown 0 wit inspect 900     470 10000    error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect
array-examples/standard_strcpy_false-valid-deref_ground.i false(valid-deref) 0 wit inspect 18     12 230    timeout 0 wit inspect 91    3700 true -32 wit inspect 9.4   320   true -32 wit inspect .59   18    - wit inspect
array-examples/standard_strcpy_original_false-valid-deref.i false(valid-deref) 0 wit inspect 15     12 220    timeout 0 wit inspect 91    3600 true -32 wit inspect 9.6   300   true -32 wit inspect .60   18    - 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 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