Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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; apollon081; apollon164] [apollon052; apollon077; apollon078; apollon160] [apollon077; apollon078] [apollon040; apollon066; apollon077; apollon078; apollon139; apollon161]
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: [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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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-02 11:31:00 CET 2017-12-02 13:19:03 CET 2017-12-02 13:40:51 CET 2017-12-02 13:42:37 CET 2017-12-02 13:21:13 CET
Run set esbmc-kind.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-Arrays
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_1131.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/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1131.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 .17 29 2.4 1 2.5  250 -32 4.9   230   0 .64   18    -
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 .20 28 1.9 0 91    490 -32 4.7   230   1 .59   18    -
array-memsafety/count_down_unsafe_false-valid-deref.i 1 .26 29 2.4 1 2.6  270 -32 4.8   240   -32 4.1    18    -
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 .30 28 3.7 -32 1.9  240 -32 3.3   230   1 .58   18    -
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 .23 29 2.2 1 3.6  250 -32 4.9   240   1 .64   18    -
array-memsafety/cstrlen_unsafe_false-valid-deref.i 1 .20 29 2.5 1 4.0  250 -32 3.3   230   0 .64   18    -
array-memsafety/cstrncat_unsafe_false-valid-deref.i 0 .28 28 3.2 -32 2.0  240 -32 3.4   230   -32 .59   18    -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 0 .41 28 4.1 -32 3.0  250 -32 5.1   240   0 .63   18    -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 .37 29 3.6 -32 2.4  250 -32 3.5   230   1 .66   150    -
array-memsafety/diff_usafe_false-valid-deref.i 0 .27 28 2.6 -32 2.2  250 -32 3.5   230   -32 .58   19    -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 .36 31 4.1 1 2.5  250 -32 5.3   240   1 .64   18    -
array-memsafety/lis_unsafe_false-valid-deref.i 0 .40 29 3.9 -32 3.5  250 -32 5.6   250   0 .64   18    -
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 .63 36 7.7 1 2.4  250 -32 3.5   230   1 .64   18    -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 0 .40 29 3.7 -32 3.8  240 -32 5.0   240   0 .65   18    -
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 .23 29 2.4 1 2.4  250 -32 3.5   240   -32 .64   18    -
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 .15 28 1.4 -32 2.9  240 -32 4.7   220   1 .59   18    -
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 .23 28 1.9 1 2.1  250 -32 3.3   240   0 .59   18    -
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i 0 900    440 11000   - - - 0 .019 4.9
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i 0 900    520 12000   - - - 0 .018 4.8
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i 0 900    510 13000   - - - 0 .019 4.9
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i 0 900    1500 12000   - - - 0 .023 5.0
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i 0 900    1200 8800   - - - 0 .019 4.8
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i 0 900    510 13000   - - - 0 .020 5.0
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i 0 900    730 11000   - - - 0 .018 5.0
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i 0 900    830 12000   - - - 0 .019 5.0
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i 0 900    660 12000   - - - 0 .021 5.0
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i 0 900    1400 9400   - - - 0 .018 4.9
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i 0 900    620 11000   - - - 0 .019 4.9
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i 0 900    850 10000   - - - 0 .022 4.9
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i 0 900    570 11000   - - - 0 .035 4.9
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i 0 900    790 9600   - - - 0 .024 4.8
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i 0 900    3500 11000   - - - 0 .024 4.9
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i 0 900    650 12000   - - - 0 .018 4.9
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i 0 900    640 9700   - - - 0 .020 4.8
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i 0 900    310 13000   - - - 0 .019 4.9
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i 0 900    520 11000   - - - 0 .020 5.0
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i 0 900    1100 8600   - - - 0 .023 4.9
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i 0 900    990 9000   - - - 0 .019 4.9
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i 0 900    1800 11000   - - - 0 .018 5.0
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i 0 900    1900 10000   - - - 0 .020 4.9
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i 0 900    1300 9300   - - - 0 .018 4.8
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i 0 900    360 9600   - - - 0 .024 5.0
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i 2 .17 27 1.3 - - - 0 960     810  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i 0 900    1300 11000   - - - 0 .019 4.9
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i 0 900    3500 9900   - - - 0 .019 4.8
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i 0 900    660 11000   - - - 0 .018 4.8
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i 0 900    860 11000   - - - 0 .025 4.8
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i 0 900    1300 12000   - - - 0 .019 4.9
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i 0 900    1000 11000   - - - 0 .018 4.9
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i 0 900    350 11000   - - - 0 .018 4.9
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i 0 900    790 10000   - - - 0 .018 5.0
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i 0 900    640 10000   - - - 0 .019 4.8
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i 0 900    1200 10000   - - - 0 .019 4.8
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i 0 900    3500 10000   - - - 0 .019 4.8
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i 0 900    830 11000   - - - 0 .020 4.9
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i 0 900    660 11000   - - - 0 .019 4.9
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i 0 900    250 12000   - - - 0 .018 4.8
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i 0 900    390 11000   - - - 0 .025 4.8
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i 0 900    960 11000   - - - 0 .019 4.9
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i 0 900    310 9900   - - - 0 .021 4.9
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i 0 900    2000 12000   - - - 0 .024 4.9
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i 0 900    780 14000   - - - 0 .025 4.8
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i 0 900    250 9800   - - - 0 .019 5.0
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i 0 900    310 13000   - - - 0 .019 4.9
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i 0 900    720 11000   - - - 0 .019 4.8
array-examples/relax_false-valid-deref.i 1 .28 30 3.2 1 2.4  250 -32 3.7   250   0 .65   19    -
array-examples/sanfoundry_24_false-valid-deref.i 0 900    910 10000   0 .54 44 0 .019 4.9 0 .0010 .26 -
array-examples/standard_strcpy_false-valid-deref_ground.i 0 900    210 12000   0 .43 44 0 .019 4.9 0 .0010 .27 -
array-examples/standard_strcpy_original_false-valid-deref.i 0 900    1200 12000   0 .66 43 0 .018 4.8 0 .0011 .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 15 45000    50000 550000   21 -247 140 4900 21 -576 76 4300 21 -121 15   460 48 0 960 1000
    correct results 14 15 3.8  410 41   9 9 24 2300 0 7 7 4.3 260 0
        correct true 1 2 .17 27 1.3 0 0 0 0
        correct false 13 13 3.6  380 39   9 9 24 2300 0 7 7 4.3 260 0
    correct-unconfimed results 5 0 1.7  140 17   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 5 0 1.7  140 17   0 0 0 0
    incorrect results 0 8 -256 22 2000 18 -576 76 4200 4 -128 6.0 74 0
        incorrect true 0 8 -256 22 2000 18 -576 76 4200 4 -128 6.0 74 0
        incorrect false 0 0 0 0 0
score (69 tasks, max score: 117) 15 -247 -576 -121 0
Run set esbmc-kind.sv-comp18.MemSafety-Arrays cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Arrays uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-Arrays