Tool CBMC 5.8 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* [apollon077; apollon078; apollon091] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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 08:19:34 CET 2017-12-01 08:48:13 CET 2017-12-01 09:05:59 CET 2017-12-01 09:09:10 CET 2017-12-01 08:49:56 CET
Run set cbmc.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-Arrays
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_0819.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/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2017-12-01_0819.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 .48 37 4.2 false(valid-deref) 1 wit inspect 3.7  250 false(valid-deref) 1 wit inspect 5.9   260   true -32 wit inspect .63   18    - wit inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .25 33 2.0 true -32 wit inspect 3.4  250 false(valid-deref) 1 wit inspect 4.2   260   false(valid-deref) 1 wit inspect .61   18    - wit inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .49 36 4.4 false(valid-deref) 1 wit inspect 3.8  250 false(valid-deref) 1 wit inspect 6.8   260   true -32 wit inspect 4.2    18    - wit inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .26 33 2.3 false(valid-deref) 1 wit inspect 2.7  240 false(valid-deref) 1 wit inspect 5.2   260   error (2) 0 wit inspect .57   18    - wit inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .45 36 4.3 exception 0 wit inspect 3.4  250 false(valid-deref) 1 wit inspect 11     430   false(valid-deref) 1 wit inspect .65   18    - wit inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .46 36 4.4 true -32 wit inspect 3.6  250 false(valid-deref) 1 wit inspect 7.7   300   error (2) 0 wit inspect .65   18    - wit inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .24 33 2.0 false(valid-deref) 1 wit inspect 2.8  250 false(valid-deref) 1 wit inspect 6.4   260   error (2) 0 wit inspect .59   18    - wit inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .25 35 2.3 false(valid-deref) 1 wit inspect 3.0  260 false(valid-deref) 1 wit inspect 3.7   270   false(valid-deref) 1 wit inspect .62   18    - wit inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .47 36 4.2 error 0 wit inspect 3.7  250 false(valid-deref) 1 wit inspect 8.8   500   false(valid-deref) 1 wit inspect .64   18    - wit inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .27 33 2.4 timeout 0 wit inspect 92    2100 true -32 wit inspect 4.8   230   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  93 10   timeout 0 wit inspect 91    2100 false(valid-deref) 1 wit inspect 9.3   320   error (2) 0 wit inspect .67   18    - wit inspect
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .48 36 4.4 true -32 wit inspect 4.2  250 false(valid-deref) 1 wit inspect 9.1   490   error (2) 0 wit inspect .66   18    - wit inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .54 38 5.1 true -32 wit inspect 3.7  250 true -32 wit inspect 17     470   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 .65 47 6.8 true -32 wit inspect 3.5  250 false(valid-deref) 1 wit inspect 4.6   280   true -32 wit inspect .66   18    - wit inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .69 47 5.9 true -32 wit inspect 4.6  250 false(valid-deref) 1 wit inspect 8.1   300   true -32 wit inspect .66   18    - wit inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .24 33 2.1 timeout 0 wit inspect 96    3600 false(valid-deref) 1 wit inspect 6.1   270   false(valid-deref) 1 wit inspect .61   19    - wit inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .24 33 2.5 false(valid-deref) 1 wit inspect 3.0  240 false(valid-deref) 1 wit inspect 5.7   260   error (2) 0 wit inspect .63   18    - wit inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 880    13000 3400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 130    13000 1200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 480    13000 3200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 160    13000 1500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    5200 4300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 160    13000 1300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 91    14000 950   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    3800 7300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    1900 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 96    13000 980   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    7000 7600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    4100 4700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 260    14000 1700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    2000 8900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 260    14000 2600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    7300 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    7500 6000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 880    11000 4700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 880    12000 4200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    5200 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    2500 5600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 73    13000 830   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 83    13000 990   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    1300 5400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i false(valid-deref) -16 wit inspect .47 36 3.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 88     690  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 82    13000 850   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 91    13000 1000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 240    14000 2600   - 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 error (134) 0 wit inspect 89    14000 910   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    2200 8400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 94    13000 1200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    430 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 880    8200 4500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    4300 6100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 250    14000 2100   - 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 error (42) 0 wit inspect 870    1700 7200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 230    14000 2300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    2000 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    280 5100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    2600 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    4000 6200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    9400 5000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 72    14000 750   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    2400 3600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 220    13000 2100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 880    12000 4200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    1200 5300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i error (42) 0 wit inspect 870    7800 6500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect .49 37 4.4 error 0 wit inspect 3.7  250 false(valid-deref) 1 wit inspect 7.2   280   false(valid-deref) 1 wit inspect .70   18    - wit inspect
array-examples/sanfoundry_24_false-valid-deref.i error (42) 0 wit inspect 870    6100 5300   error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
array-examples/standard_strcpy_false-valid-deref_ground.i out of memory 0 wit inspect 67    15000 980   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0038 .29 - wit inspect
array-examples/standard_strcpy_original_false-valid-deref.i out of memory 0 wit inspect 67    15000 980   error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .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 2 29000    430000 200000   21 -186 330 12000 21 -48 130 5700 21 -120 15   330 48 2 89 920
    correct results 18 18 8.0  710 74   6 6 19 1500 16 16 110 5000 8 8 5.1 150 1 2 88 690
        correct true 0 0 0 0 1 2 88 690
        correct false 18 18 8.0  710 74   6 6 19 1500 16 16 110 5000 8 8 5.1 150 0
    incorrect results 1 -16 .47 36 3.4 6 -192 23 1500 2 -64 22 700 4 -128 6.1 74 0
        incorrect true 0 6 -192 23 1500 2 -64 22 700 4 -128 6.1 74 0
        incorrect false 1 -16 .47 36 3.4 0 0 0 0
score (69 tasks, max score: 117) 2 -186 -48 -120 2
Run set cbmc.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-Arrays