Tool 2LS 0.5.0 CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux Predator-HP SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a ULTIMATE Automizer f7c3ed31 ULTIMATE Kojak f7c3ed31 ULTIMATE Taipan f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 09:48:02 CET [[ 2017-01-14 21:34:09 CET ]] [[ 2017-01-14 21:49:16 CET ]] [[ 2017-01-14 21:34:25 CET ]] [[ 2017-01-14 21:52:20 CET ]] 2017-01-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]] 2017-01-11 09:49:51 CET [[ 2017-01-14 20:52:01 CET ]] [[ 2017-01-14 21:02:28 CET ]] [[ 2017-01-14 20:57:34 CET ]] [[ 2017-01-14 21:06:31 CET ]] 2017-01-11 10:34:02 CET [[ 2017-01-14 21:41:36 CET ]] [[ 2017-01-14 21:45:05 CET ]] [[ 2017-01-14 21:43:06 CET ]] [[ 2017-01-14 21:46:49 CET ]] 2017-01-11 10:43:32 CET [[ 2017-01-14 21:41:35 CET ]] [[ 2017-01-14 21:45:05 CET ]] [[ 2017-01-14 21:43:06 CET ]] [[ 2017-01-14 21:46:49 CET ]] 2017-01-13 04:38:11 CET [[ 2017-01-14 23:48:17 CET ]] [[ 2017-01-14 23:57:43 CET ]] [[ 2017-01-14 23:52:59 CET ]] [[ 2017-01-15 00:03:21 CET ]] 2017-01-13 04:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]] 2017-01-13 04:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]] 2017-01-13 05:20:12 CET [[ 2017-01-15 00:51:08 CET ]] [[ 2017-01-15 01:00:54 CET ]] [[ 2017-01-15 00:55:05 CET ]] [[ 2017-01-15 01:06:26 CET ]] 2017-01-13 05:51:33 CET [[ 2017-01-15 01:19:13 CET ]] [[ 2017-01-15 01:22:10 CET ]] [[ 2017-01-15 01:20:47 CET ]] [[ 2017-01-15 01:23:25 CET ]] 2017-01-13 06:35:22 CET [[ 2017-01-15 01:30:25 CET ]] [[ 2017-01-15 01:30:43 CET ]] [[ 2017-01-15 01:30:33 CET ]] [[ 2017-01-15 01:30:54 CET ]] 2017-01-13 12:06:28 CET [[ 2017-01-15 02:02:31 CET ]] [[ 2017-01-15 02:04:15 CET ]] [[ 2017-01-15 02:04:05 CET ]] [[ 2017-01-15 02:06:30 CET ]] 2017-01-14 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]] 2017-01-14 11:37:51 CET [[ 2017-01-15 04:18:56 CET ]] [[ 2017-01-15 04:38:06 CET ]] [[ 2017-01-15 04:27:27 CET ]] [[ 2017-01-15 04:45:45 CET ]] 2017-01-14 06:16:04 CET [[ 2017-01-15 05:34:44 CET ]] [[ 2017-01-15 05:49:53 CET ]] [[ 2017-01-15 05:35:06 CET ]] [[ 2017-01-15 05:51:11 CET ]] 2017-01-14 06:29:29 CET [[ 2017-01-15 05:44:30 CET ]] [[ 2017-01-15 05:59:35 CET ]] [[ 2017-01-15 05:44:48 CET ]] [[ 2017-01-15 06:00:32 CET ]] 2017-01-14 16:15:06 CET [[ 2017-01-15 05:45:52 CET ]] [[ 2017-01-15 06:00:59 CET ]] [[ 2017-01-15 05:46:10 CET ]] [[ 2017-01-15 06:02:27 CET ]]
Run set 2ls.sv-comp17.MemSafety-Arrays cbmc.sv-comp17.MemSafety-Arrays ceagle.sv-comp17.MemSafety-Arrays cpa-bam-bnb.sv-comp17.MemSafety-Arrays cpa-kind.sv-comp17.MemSafety-Arrays cpa-seq.sv-comp17.MemSafety-Arrays depthk.sv-comp17.MemSafety-Arrays esbmc.sv-comp17.MemSafety-Arrays esbmc-falsi.sv-comp17.MemSafety-Arrays esbmc-incr.sv-comp17.MemSafety-Arrays esbmc-kind.sv-comp17.MemSafety-Arrays predatorhp.sv-comp17.MemSafety-Arrays smack.sv-comp17.MemSafety-Arrays symbiotic4.sv-comp17.MemSafety-Arrays uautomizer.sv-comp17.MemSafety-Arrays ukojak.sv-comp17.MemSafety-Arrays utaipan.sv-comp17.MemSafety-Arrays
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-11_1034.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1043.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]] [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
array-memsafety/add_last_unsafe_false-valid-deref.i error (8) .19 26 1.4  0 false(valid-deref) .19 20 1.8  1 false(valid-deref) .028 8.0 .17 1 error (1) .43 37 3.4 0 error (1) .42 40 3.4 0 error 2.4 210 22 0 false(valid-deref) .50 29 6.9 1 false(valid-deref) 130   3300 1500 1 false(valid-deref) .21  24 2.2  1 false(valid-deref) .20  24 2.1  1 false(valid-deref) .21  24 2.2  1 unknown .11 23 1.7 0 false(valid-deref) 1.8 79 22 1 false(valid-deref) .22 10 2.8 1 false(valid-deref) 6.2 340 47 1 false(valid-deref) 6.6 320 53 1 false(valid-deref) 6.1 320 49 1
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) .13 25 .87 1 false(valid-deref) .11 17 .98 1 false(valid-deref) .022 7.9 .15 1 error (1) .45 40 3.8 0 error (1) .42 40 4.1 0 timeout 920   11000 7300 0 false(valid-deref) .36 28 3.8 1 timeout 900   12000 5500 0 false(valid-deref) .10  23 1.1  1 false(valid-deref) .096 23 .91 1 false(valid-deref) .093 23 1.0  1 false(valid-deref) .16 22 1.9 1 false(valid-deref) 1.9 73 24 1 false(valid-deref) .24 11 2.7 1 false(valid-deref) 6.5 360 50 1 false(valid-deref) 5.9 330 49 1 false(valid-deref) 6.2 320 45 1
array-memsafety/count_down_unsafe_false-valid-deref.i error (8) .17 26 1.4  0 false(valid-deref) .25 24 2.3  1 false(valid-deref) .029 7.8 .18 1 error (1) .44 37 3.8 0 error (1) .44 40 3.9 0 error 2.5 220 21 0 false(valid-deref) .55 29 6.3 1 out of memory 230   15000 2900 0 false(valid-deref) .21  24 1.9  1 false(valid-deref) .20  24 2.1  1 false(valid-deref) .20  24 2.0  1 unknown .11 23 1.8 0 false(valid-deref) 1.9 79 25 1 false(valid-deref) .23 11 2.8 1 false(valid-deref) 7.2 370 55 1 false(valid-deref) 6.8 320 52 1 false(valid-deref) 6.4 350 49 1
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) .13 23 .86 1 false(valid-deref) .11 20 1.1  1 false(valid-deref) .027 7.5 .11 1 error (1) .45 40 4.0 0 error (1) .41 38 4.3 0 false(valid-deref) 2.2 230 19 1 false(valid-deref) .33 28 4.1 1 false(valid-deref) 15   850 170 1 false(valid-deref) .12  23 .96 1 false(valid-deref) .089 23 .99 1 false(valid-deref) .094 23 .91 1 false(valid-deref) .12 21 1.9 1 false(valid-deref) 1.8 86 23 1 false(valid-deref) .63 12 6.1 1 false(valid-deref) 5.7 340 44 1 false(valid-deref) 5.7 320 47 1 false(valid-deref) 5.9 330 43 1
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) .12 25 1.2  1 false(valid-deref) .12 19 1.1  1 false(valid-deref) .064 33   .48 1 error (1) .45 40 3.9 0 error (1) .42 37 3.6 0 error 2.6 220 25 0 false(valid-deref) .36 29 4.2 1 false(valid-deref) 3.4 280 44 1 false(valid-deref) .13  24 1.2  1 false(valid-deref) .11  24 1.2  1 false(valid-deref) .10  24 1.2  1 unknown .14 23 1.7 0 false(valid-deref) 2.0 84 22 1 error .41 10 5.2 0 false(valid-deref) 12   490 95 1 false(valid-deref) 9.9 490 83 1 false(valid-deref) 14   490 120 1
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) .19 26 1.4  1 false(valid-deref) .21 20 1.7  1 false(valid-deref) .027 8.0 .16 1 error (1) .39 37 4.0 0 error (1) .39 37 3.5 0 error 2.5 220 25 0 false(valid-deref) .37 29 4.3 1 false(valid-deref) 1.9 180 26 1 false(valid-deref) .10  24 1.2  1 false(valid-deref) .097 24 1.1  1 false(valid-deref) .14  24 1.1  1 unknown .14 23 1.8 0 false(valid-deref) 1.9 84 26 1 error .60 11 7.3 0 false(valid-deref) 7.6 400 61 1 false(valid-deref) 11   480 85 1 false(valid-deref) 7.9 380 61 1
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) .11 23 1.2  1 false(valid-deref) .12 21 1.1  1 false(valid-deref) .035 8.0 .13 1 error (1) .43 37 3.8 0 error (1) .39 37 3.5 0 false(valid-deref) 2.2 230 18 1 false(valid-deref) .36 28 3.8 1 false(valid-deref) 20   1600 260 1 false(valid-deref) .13  23 1.0  1 false(valid-deref) .11  23 1.1  1 false(valid-deref) .11  23 1.1  1 false(valid-deref) .13 22 1.8 1 false(valid-deref) 1.9 81 22 1 false(valid-deref) 1.2  12 11   1 false(valid-deref) 5.5 320 48 1 false(valid-deref) 5.7 320 42 1 false(valid-deref) 5.8 320 43 1
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) .10 23 .91 1 false(valid-deref) .12 21 1.3  1 false(valid-deref) .026 7.7 .12 1 error (1) .45 39 4.1 0 error (1) .40 38 4.0 0 false(valid-deref) 2.3 230 20 1 false(valid-deref) .36 28 3.8 1 false(valid-deref) 890   9100 7000 1 false(valid-deref) .12  23 .98 1 false(valid-deref) .095 23 1.1  1 false(valid-deref) .094 23 1.2  1 false(valid-deref) .12 21 1.9 1 false(valid-deref) 1.9 85 26 1 false(valid-deref) 1.3  12 13   1 false(valid-deref) 5.7 320 45 1 false(valid-deref) 6.6 350 50 1 false(valid-deref) 6.0 340 50 1
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) .12 26 1.3  1 false(valid-deref) .13 20 1.3  1 false(valid-deref) .043 8.0 .21 1 error (1) .43 37 3.4 0 error (1) .43 37 3.9 0 error 2.6 220 21 0 false(valid-deref) .35 29 4.5 1 timeout 900   5700 7700 0 false(valid-deref) .12  24 1.3  1 false(valid-deref) .099 24 1.4  1 false(valid-deref) .11  24 1.3  1 unknown .11 24 1.6 0 false(valid-deref) 2.2 85 25 1 error .36 11 3.8 0 false(valid-deref) 9.7 400 73 1 false(valid-deref) 11   480 83 1 false(valid-deref) 180   690 2000 1
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) .12 23 1.1  1 false(valid-deref) .11 20 1.1  1 false(valid-deref) .035 7.9 .13 1 error (1) .42 40 3.8 0 error (1) .42 38 3.7 0 false(valid-deref) 2.4 240 21 1 false(valid-deref) .35 28 3.7 1 timeout 900   7200 9100 0 false(valid-deref) .12  23 .95 1 false(valid-deref) .094 23 1.1  1 false(valid-deref) .098 23 1.0  1 false(valid-deref) .15 23 2.4 1 false(valid-deref) 1.8 80 25 1 false(valid-deref) .25 12 2.6 1 false(valid-deref) 6.1 320 45 1 false(valid-deref) 6.2 320 49 1 false(valid-deref) 6.1 330 46 1
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) .22 30 2.6  1 false(valid-deref) .39 39 3.7  1 false(valid-deref) .029 8.0 .15 1 error (1) .39 37 3.3 0 error (1) .43 40 4.0 0 error 10   220 14 0 false(valid-deref) .88 29 12   1 out of memory 540   15000 3400 0 false(valid-deref) .29  24 3.5  1 false(valid-deref) .30  25 3.5  1 false(valid-deref) .30  24 3.8  1 unknown .21 34 1.7 0 false(valid-deref) 2.0 86 24 1 false(valid-deref) .30 13 2.9 1 false(valid-deref) 9.5 380 71 1 false(valid-deref) 8.1 380 58 1 false(valid-deref) 11   380 90 1
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) .29 34 2.8  1 false(valid-deref) .24 20 1.8  1 false(valid-deref) .034 7.8 .21 1 error (1) .40 37 3.5 0 error (1) .42 38 3.6 0 error 2.5 220 23 0 false(valid-deref) .73 29 7.9 1 out of memory 32   15000 380 0 false(valid-deref) .27  24 3.3  1 false(valid-deref) .26  24 3.4  1 false(valid-deref) .29  25 3.5  1 unknown .12 23 1.7 0 false(valid-deref) 2.2 95 27 1 unknown .29 14 3.6 0 false(valid-deref) 10   410 75 1 false(valid-deref) 41   700 440 1 false(valid-deref) 18   460 150 1
array-memsafety/mult_array_unsafe_false-valid-deref.i error (8) .19 28 1.4  0 false(valid-deref) .25 27 2.8  1 false(valid-deref) .039 8.1 .19 1 error (1) .45 39 3.9 0 error (1) .41 40 4.3 0 error 2.6 220 21 0 false(valid-deref) .64 29 8.8 1 false(valid-deref) 20   1300 240 1 false(valid-deref) .28  27 3.9  1 false(valid-deref) .28  26 3.3  1 false(valid-deref) .31  26 3.4  1 unknown .13 23 1.7 0 false(valid-deref) 1.9 82 24 1 false(valid-deref) .36 17 4.5 1 false(valid-deref) 6.6 330 50 1 false(valid-deref) 7.1 320 59 1 false(valid-deref) 7.2 330 63 1
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) .27 33 2.7  1 false(valid-deref) .32 33 3.0  1 false(valid-deref) .052 43   .74 1 error (1) .45 40 3.9 0 error (1) .39 38 3.4 0 error 2.4 210 20 0 false(valid-deref) 1.8  29 25   1 timeout 900   4200 11000 0 false(valid-deref) .51  25 7.3  1 false(valid-deref) .51  27 6.7  1 false(valid-deref) .51  27 6.7  1 unknown .12 23 1.9 0 false(valid-deref) 2.0 84 22 1 false(valid-deref) .40 11 4.3 1 false(valid-deref) 8.0 360 62 1 false(valid-deref) 11   510 89 1 false(valid-deref) 7.0 360 55 1
array-memsafety/reverse_array_unsafe_false-valid-deref.i error (8) .21 38 1.9  0 false(valid-deref) .70 83 9.5  1 false(valid-deref) .027 7.9 .20 1 error (1) .40 39 3.8 0 error (1) .42 39 4.0 0 error 2.6 220 21 0 false(valid-deref) .59 29 8.1 1 timeout 900   2000 11000 0 false(valid-deref) .20  24 2.5  1 false(valid-deref) .19  24 2.8  1 false(valid-deref) .21  24 2.5  1 unknown .11 25 2.0 0 false(valid-deref) 1.9 81 28 1 false(valid-deref) .23 11 2.5 1 false(valid-deref) 7.0 370 50 1 false(valid-deref) 7.5 350 64 1 false(valid-deref) 7.1 350 53 1
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) .15 26 .95 1 false(valid-deref) .11 18 1.0  1 false(valid-deref) .021 7.8 .10 1 error (1) .44 40 3.9 0 error (1) .44 37 3.3 0 false(valid-deref) 2.4 230 22 1 false(valid-deref) .36 28 4.1 1 timeout 900   7200 8000 0 false(valid-deref) .13  23 .85 1 false(valid-deref) .13  23 1.0  1 false(valid-deref) .11  23 1.2  1 false(valid-deref) .12 24 1.8 1 false(valid-deref) 1.9 73 23 1 false(valid-deref) .22 11 2.9 1 false(valid-deref) 6.7 340 49 1 false(valid-deref) 6.7 330 47 1 false(valid-deref) 6.1 330 55 1
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) .12 22 .79 1 false(valid-deref) .12 17 .88 1 false(valid-deref) .067 43   .45 1 error (1) .41 38 3.7 0 error (1) .40 37 3.8 0 false(valid-deref) 2.3 230 20 1 false(valid-deref) .35 27 3.9 1 false(valid-deref) 2.9 310 33 1 false(valid-deref) .093 23 1.0  1 false(valid-deref) .090 23 1.1  1 false(valid-deref) .10  23 1.1  1 false(valid-deref) .17 21 1.8 1 false(valid-deref) 1.8 82 21 1 false(valid-deref) .58 11 6.7 1 false(valid-deref) 5.7 320 48 1 false(valid-deref) 5.6 320 41 1 false(valid-deref) 6.6 350 54 1
array-memsafety/add_last-alloca_true-valid-memsafety.i false(valid-deref) .27 31 2.6  -16 error (134) 120    13000 1200    0 true .030 8.2 .17 2 error (1) .45 40 4.0 0 error (1) .40 38 3.7 0 error 2.5 210 21 0 unknown 900    69 2100   0 true 890   4100 11000 2 timeout 900     2700 9500    0 timeout 900     4600 11000    0 timeout 900     5800 11000    0 unknown .11 22 1.8 0 true 750   330 8200 2 true .26 10 3.2 2 timeout 900   1600 11000 0 timeout 900   860 14000 0 timeout 900   4700 9600 0
array-memsafety/array01-alloca_true-valid-memsafety.i true .37 28 3.7  2 error (42) 850    8900 6300    0 true .028 8.1 .19 2 error (1) .43 37 3.4 0 error (1) .39 37 3.5 0 error 2.5 220 21 0 unknown 890    280 10000   0 out of memory 230   15000 2500 0 out of memory 850     15000 9200    0 timeout 900     380 10000    0 timeout 900     430 9000    0 unknown .15 23 1.6 0 true 750   500 7800 2 timeout (timeout) 900    790 12000   0 true 10   430 82 2 true 15   540 150 2 true 10   450 86 2
array-memsafety/array02-alloca_true-valid-memsafety.i true .47 30 5.3  2 error (1) 470    14000 3700    0 true .026 7.9 .23 2 error (1) .42 40 3.9 0 error (1) .40 38 3.7 0 error 2.6 220 25 0 unknown 890    280 9300   0 out of memory 300   15000 2300 0 timeout 900     10000 8400    0 timeout 900     390 8800    0 timeout 900     410 12000    0 unknown .15 23 1.7 0 true 760   580 7200 2 timeout (timeout) 900    950 11000   0 true 9.2 420 71 2 true 19   530 180 2 true 11   480 90 2
array-memsafety/array03-alloca_true-valid-memsafety.i true .38 29 3.7  2 error (134) 510    14000 3700    0 true .041 44   .94 2 error (1) .42 37 3.3 0 error (1) .39 38 3.7 0 error 2.5 210 23 0 unknown 890    280 1700   0 out of memory 50   15000 570 0 timeout 900     13000 9000    0 timeout 900     800 7200    0 timeout 900     880 7700    0 unknown .12 23 1.6 0 true 750   390 7000 2 timeout (timeout) 900    760 9700   0 true 9.1 430 77 2 timeout 900   1000 12000 0 true 11   500 99 2
array-memsafety/bubblesort-alloca_true-valid-memsafety.i timeout 900    13000 5300    0 error (42) 850    2700 6600    0 true .066 44   .40 2 error (1) .42 38 4.2 0 error (1) .41 37 3.8 0 error 2.5 210 23 0 unknown 890    310 8600   0 out of memory 330   15000 3000 0 timeout 900     4200 2200    0 timeout 900     460 11000    0 timeout 900     530 8100    0 unknown .11 24 1.9 0 true 750   510 6600 2 true .24 11 2.9 2 true 10   400 76 2 true 38   880 380 2 true 11   440 85 2
array-memsafety/count_down-alloca_true-valid-memsafety.i true .55 30 5.7  2 error (42) 850    9000 5400    0 true .029 7.9 .21 2 error (1) .41 37 3.8 0 error (1) .42 38 4.2 0 error 2.6 230 25 0 unknown 890    300 11000   0 out of memory 250   15000 2300 0 out of memory 380     15000 4500    0 timeout 900     380 8200    0 timeout 900     390 9200    0 unknown .11 23 1.7 0 true 750   210 8500 2 timeout (timeout) 900    570 11000   0 true 12   490 95 2 true 46   700 550 2 true 13   500 100 2
array-memsafety/cstrcat-alloca_true-valid-memsafety.i false(valid-deref) .26 29 2.4  -16 error (134) 110    14000 1100    0 true .030 8.1 .18 2 error (1) .43 37 3.8 0 error (1) .41 42 3.9 0 error 2.6 220 24 0 unknown 900    84 12000   0 true 390   1600 4700 2 timeout 900     1300 12000    0 timeout 900     2800 13000    0 unknown .23  24 2.6  0 unknown .14 23 1.8 0 true 750   280 8800 2 true 1.2  13 13   2 timeout 900   3000 13000 0 timeout 900   1300 15000 0 timeout 900   2900 11000 0
array-memsafety/cstrchr-alloca_true-valid-memsafety.i false(valid-deref) .22 26 1.8  -16 error (42) 850    4600 6700    0 true .028 7.9 .18 2 error (1) .44 40 3.9 0 error (1) .44 40 3.6 0 error 2.4 210 23 0 unknown 170    46 2400   0 true 20   490 210 2 timeout 900     4000 13000    0 timeout 900     8900 12000    0 timeout 900     12000 12000    0 unknown .11 22 1.9 0 true 750   170 10000 2 true .23 11 2.3 2 true 13   490 100 2 true 27   580 300 2 true 15   520 130 2
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i false(valid-deref) .26 27 2.2  -16 error (42) 850    1800 9700    0 true .028 7.8 .20 2 error (1) .44 39 3.8 0 error (1) .42 40 3.6 0 error 2.5 220 20 0 unknown 39    35 520   0 true 320   850 1100 2 timeout 900     1200 2100    0 timeout 900     6200 12000    0 timeout 900     8600 13000    0 unknown .16 33 1.8 0 true 750   210 8300 2 true 3.3  20 36   2 true 27   680 260 2 true 230   1000 3400 2 true 44   830 420 2
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i false(valid-deref) .24 28 2.5  -16 error (134) 83    13000 940    0 true .059 8.0 .15 2 error (1) .45 40 4.0 0 error (1) .43 40 4.0 0 error 2.6 220 23 0 unknown 140    48 1600   0 true 21   860 260 2 timeout 900     7800 11000    0 out of memory 640     15000 7600    0 unknown .16  24 1.9  0 unknown .21 33 1.6 0 true 750   220 9100 2 true .37 11 4.0 2 timeout 900   1200 13000 0 timeout 900   1800 12000 0 timeout 900   1200 13000 0
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i false(valid-deref) .37 33 3.3  -16 error (42) 850    9000 7300    0 true .028 8.3 .20 2 error (1) .43 40 4.0 0 error (1) .42 40 4.0 0 error 2.4 210 22 0 unknown 900    170 12000   0 timeout 900   10000 8800 0 timeout 900     500 11000    0 timeout 900     990 11000    0 timeout 900     1600 12000    0 unknown .11 24 1.8 0 true 750   610 7600 2 timeout (timeout) 900    550 9900   0 true 24   550 250 2 timeout 900   1500 13000 0 true 36   610 340 2
array-memsafety/cstrlen-alloca_true-valid-memsafety.i false(valid-deref) .21 26 1.7  -16 error (42) 850    3900 4500    0 true .030 7.9 .16 2 error (1) .44 40 3.8 0 error (1) .42 38 3.5 0 error 2.7 220 21 0 unknown 100    30 1300   0 true 11   290 140 2 out of memory 690     15000 8400    0 out of memory 480     15000 6700    0 out of memory 520     15000 7600    0 unknown .13 24 1.7 0 true 750   150 9300 2 true .23 10 2.6 2 true 13   500 91 2 true 17   520 160 2 true 14   500 110 2
array-memsafety/cstrncat-alloca_true-valid-memsafety.i false(valid-deref) .45 32 4.7  -16 error (134) 380    14000 3600    0 true .039 8.0 .17 2 error (1) .43 40 3.9 0 error (1) .43 40 3.7 0 error 2.6 220 22 0 unknown 900    150 10000   0 true 890   3100 12000 2 timeout 900     650 12000    0 timeout 900     790 11000    0 timeout 900     1000 12000    0 unknown .11 24 1.8 0 true 750   260 8700 2 true 2.7  17 31   2 timeout 900   1000 11000 0 timeout 900   1400 11000 0 timeout 900   1600 11000 0
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i false(valid-deref) .32 29 3.1  -16 error (42) 850    2000 8500    0 true .079 43   .55 2 error (1) .43 40 3.9 0 error (1) .40 40 3.3 0 error 2.6 220 24 0 unknown 62    79 870   0 true 210   3700 2700 2 timeout 900     3200 12000    0 timeout 900     7800 13000    0 unknown .23  24 2.7  0 unknown .15 22 1.6 0 true 750   240 8000 2 true 5.4  22 65   2 true 29   540 300 2 true 410   1300 5000 2 true 37   770 420 2
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i false(valid-deref) 1.9  120 22    -16 error (134) 220    14000 3000    0 true .027 7.8 .19 2 error (1) .43 39 3.9 0 error (1) .39 38 3.4 0 error 2.5 210 20 0 timeout 900    960 11000   0 out of memory 170   15000 1900 0 out of memory 720     15000 7400    0 out of memory 590     15000 4100    0 unknown .20  24 1.9  0 unknown .11 24 1.8 0 true 750   240 7100 2 true 4.3  28 56   2 timeout 900   1600 14000 0 timeout 900   2600 14000 0 timeout 900   1500 12000 0
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i false(valid-deref) .34 46 3.7  -16 error (42) 850    9200 8600    0 true .029 7.9 .17 2 error (1) .44 39 4.0 0 error (1) .40 37 3.9 0 error 2.6 220 22 0 unknown 900    140 11000   0 timeout 900   10000 7900 0 timeout 900     360 11000    0 timeout 900     680 13000    0 timeout 900     1100 12000    0 unknown .14 24 1.7 0 true 750   550 6500 2 timeout (timeout) 900    500 7000   0 true 43   730 450 2 timeout 900   1600 12000 0 true 61   880 650 2
array-memsafety/cstrspn-alloca_true-valid-memsafety.i false(valid-deref) .33 33 3.7  -16 error (42) 850    9100 7400    0 true .082 43   .47 2 error (1) .39 37 3.9 0 error (1) .42 38 3.4 0 error 10   220 14 0 unknown 900    150 12000   0 timeout 900   10000 11000 0 timeout 900     390 11000    0 timeout 900     760 12000    0 timeout 900     1200 11000    0 unknown .11 23 1.7 0 true 750   510 6100 2 timeout (timeout) 900    510 8300   0 true 45   690 510 2 timeout 900   1600 13000 0 true 62   700 740 2
array-memsafety/diff-alloca_true-valid-memsafety.i timeout 900    6200 5200    0 error (42) 850    6500 3400    0 true .038 8.0 .19 2 error (1) .42 40 3.9 0 error (1) .45 40 4.0 0 error 2.6 220 20 0 unknown 890    180 7800   0 timeout 900   12000 11000 0 timeout 900     340 9500    0 timeout 900     500 10000    0 timeout 900     700 10000    0 unknown .12 24 1.6 0 true 750   150 11000 2 true .28 13 3.0 2 true 16   530 130 2 timeout 900   1000 12000 0 true 33   690 340 2
array-memsafety/insertionsort-alloca_true-valid-memsafety.i out of memory 750    15000 5200    0 error (42) 850    9000 3700    0 true .026 8.0 .15 2 error (1) .44 37 3.3 0 error (1) .45 38 4.2 0 error 2.6 220 22 0 unknown 890    180 9000   0 timeout 900   8300 8100 0 timeout 900     710 6800    0 timeout 900     360 9100    0 timeout 900     400 10000    0 unknown .11 24 1.7 0 true 750   440 6100 2 true .22 11 2.6 2 true 12   480 90 2 true 30   610 270 2 true 15   500 110 2
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i true .52 30 5.9  2 error (42) 850    2800 6500    0 true .023 8.2 .17 2 error (1) .45 40 3.9 0 error (1) .45 38 3.8 0 error 2.5 220 21 0 unknown 890    300 8900   0 out of memory 550   15000 2600 0 timeout 900     8900 10000    0 timeout 900     480 9400    0 timeout 900     510 8800    0 unknown .12 23 1.7 0 true 750   460 8100 2 true .23 11 2.5 2 true 9.7 400 76 2 true 32   670 380 2 true 11   440 78 2
array-memsafety/lis-alloca_true-valid-memsafety.i timeout 900    340 10000    0 error (42) 850    2500 5700    0 true .030 8.1 .18 2 error (1) .44 37 3.5 0 error (1) .41 37 3.2 0 error 2.6 220 20 0 unknown 890    190 10000   0 out of memory 150   15000 400 0 out of memory 440     15000 5500    0 timeout 900     360 8600    0 timeout 900     490 8500    0 unknown .11 24 1.8 0 true 750   350 6500 2 true .24 12 3.0 2 true 15   500 130 2 timeout 900   1400 11000 0 timeout 900   790 9200 0
array-memsafety/mult_array-alloca_true-valid-memsafety.i timeout 900    190 10000    0 error (134) 110    14000 1300    0 true .040 8.1 .16 2 error (1) .45 40 4.0 0 error (1) .42 38 3.9 0 error 2.6 220 21 0 unknown 320    89 3600   0 true 25   1300 260 2 timeout 900     6100 10000    0 timeout 900     13000 9600    0 timeout 900     13000 9600    0 unknown .15 23 2.0 0 true 750   370 7700 2 true .52 15 6.8 2 true 18   510 180 2 timeout 900   740 13000 0 true 65   530 800 2
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i timeout 900    11000 8800    0 error (1) 83    13000 1100    0 true .081 44   .65 2 error (1) .43 40 4.3 0 error (1) .40 37 3.9 0 error 2.5 220 22 0 unknown 100    33 1300   0 true 5.2 450 57 2 timeout 900     9100 13000    0 out of memory 490     15000 6500    0 unknown .13  24 1.6  0 unknown .10 24 2.2 0 true 750   320 11000 2 true .79 12 9.7 2 true 12   480 94 2 true 18   540 180 2 true 15   570 110 2
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i timeout 900    3400 9700    0 error (42) 850    1300 5900    0 true .026 8.2 .23 2 error (1) .41 40 4.0 0 error (1) .39 37 3.3 0 error 2.5 220 21 0 unknown 110    43 1300   0 true 42   1000 130 2 out of memory 710     15000 9400    0 out of memory 280     15000 4000    0 unknown .13  24 1.7  0 unknown .14 23 1.6 0 true 750   410 11000 2 true 1.2  15 14   2 true 12   540 90 2 true 12   480 100 2 true 14   510 110 2
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i false(valid-deref) .18 26 1.5  -16 error (42) 850    1000 3900    0 true .030 7.8 .15 2 error (1) .41 40 4.1 0 error (1) .42 38 3.6 0 error 2.6 210 21 0 unknown 32    34 410   0 unknown 5.9 840 83 0 unknown .14  24 1.3  0 unknown .14  24 1.3  0 unknown .13  24 1.4  0 unknown .14 24 1.6 0 true 750   450 8900 2 true 1.6  15 18   2 true 16   530 140 2 true 12   480 120 2 true 27   530 260 2
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i error (8) .19 26 1.5  0 error (1) 84    13000 870    0 true .030 7.8 .16 2 error (1) .44 40 3.8 0 error (1) .40 37 3.4 0 error 2.5 220 20 0 unknown 93    32 1200   0 true 4.9 410 64 2 out of memory 800     15000 10000    0 out of memory 310     15000 4300    0 unknown .13  24 1.5  0 unknown .11 24 1.8 0 true 750   410 8400 2 true .30 11 3.9 2 true 11   470 100 2 true 12   490 110 2 true 14   500 120 2
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i false(valid-deref) .27 28 2.4  -16 error (1) 93    13000 1000    0 true .027 8.2 .23 2 error (1) .42 37 3.3 0 error (1) .41 37 3.5 0 error 2.7 220 22 0 unknown 130    45 2000   0 true 20   760 210 2 timeout 900     7900 9700    0 out of memory 660     15000 8700    0 unknown .16  24 1.7  0 unknown .15 22 1.6 0 true 750   270 8500 2 true .37 11 4.3 2 timeout 900   1100 12000 0 timeout 900   1600 12000 0 timeout 900   1500 12000 0
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i false(valid-deref) 2.5  120 24    -16 error (134) 220    14000 2600    0 true .042 8.3 .18 2 error (1) .45 40 4.0 0 error (1) .39 37 3.5 0 error 2.6 230 22 0 timeout 900    940 13000   0 out of memory 170   15000 2200 0 out of memory 640     15000 7900    0 out of memory 260     15000 3700    0 unknown .18  24 2.3  0 unknown .12 25 2.0 0 true 750   230 7100 2 true 4.2  28 53   2 timeout 900   900 12000 0 timeout 900   1100 14000 0 timeout 910   9900 7700 0
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i false(valid-deref) .23 28 3.0  -16 error (134) 110    14000 1300    0 true .029 7.9 .18 2 error (1) .44 39 3.9 0 error (1) .42 40 4.0 0 error 2.4 210 23 0 unknown 900    85 13000   0 true 380   1600 4000 2 timeout 900     1200 11000    0 timeout 900     2700 10000    0 unknown .21  24 2.9  0 unknown .11 24 2.0 0 true 750   290 8100 2 true 1.5  13 15   2 timeout 900   2600 11000 0 timeout 900   1400 11000 0 timeout 900   3100 11000 0
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i false(valid-deref) .29 31 2.5  -16 error (42) 850    2200 8900    0 true .031 7.9 .15 2 error (1) .42 40 4.0 0 error (1) .39 37 3.3 0 error 2.6 210 22 0 unknown 270    81 3800   0 true 84   2300 1000 2 timeout 900     5200 11000    0 timeout 900     12000 11000    0 unknown .22  24 2.3  0 unknown .11 23 1.7 0 true 750   230 8500 2 true 3.2  20 38   2 true 34   560 320 2 true 350   1200 4800 2 true 67   620 770 2
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i false(valid-deref) .23 28 2.4  -16 error (134) 96    13000 1100    0 true .080 44   .49 2 error (1) .44 40 4.1 0 error (1) .41 37 4.2 0 error 2.5 220 22 0 unknown 130    45 1600   0 true 20   760 240 2 timeout 900     7900 11000    0 out of memory 680     15000 9400    0 unknown .16  25 1.8  0 unknown .10 24 1.9 0 true 750   230 9000 2 true .36 11 3.5 2 timeout 900   1000 12000 0 timeout 900   1800 12000 0 timeout 900   1700 12000 0
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i false(valid-deref) .31 30 3.0  -16 error (42) 850    380 2600    0 true .065 44   .49 2 error (1) .41 40 3.9 0 error (1) .40 37 3.7 0 error 2.7 220 23 0 unknown 900    1100 12000   0 timeout 900   14000 6600 0 timeout 900     1600 2100    0 timeout 900     9500 12000    0 unknown .20  25 1.9  0 unknown .11 23 1.7 0 true 750   230 8100 2 timeout (timeout) 900    620 12000   0 timeout 900   1600 14000 0 timeout 900   1600 12000 0 timeout 900   1500 11000 0
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i false(valid-deref) .36 30 3.6  -16 error (42) 850    13000 4600    0 true .032 8.0 .16 2 error (1) .43 40 3.8 0 error (1) .42 38 3.5 0 error 2.6 220 21 0 unknown 900    95 9500   0 true 890   4400 8600 2 timeout 900     790 13000    0 timeout 900     1700 11000    0 unknown .22  25 2.8  0 unknown .14 24 1.8 0 true 750   250 10000 2 true 1.3  13 12   2 timeout 900   1200 15000 0 timeout 900   1200 11000 0 timeout 900   930 12000 0
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i false(valid-deref) .21 26 1.8  -16 error (42) 850    4700 5100    0 true .027 8.0 .19 2 error (1) .44 39 3.8 0 error (1) .40 37 3.7 0 error 11   220 12 0 unknown 390    30 760   0 true 46   290 91 2 out of memory 510     15000 7300    0 out of memory 260     15000 3100    0 out of memory 300     15000 3700    0 unknown .14 24 1.6 0 true 750   150 9100 2 true .21 10 2.4 2 true 12   470 92 2 true 16   590 140 2 true 14   550 120 2
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i false(valid-deref) .43 32 4.2  -16 error (134) 430    14000 2500    0 true .040 8.3 .20 2 error (1) .45 40 4.1 0 error (1) .43 40 3.7 0 error 2.5 220 20 0 unknown 900    64 11000   0 true 680   2700 9400 2 timeout 900     500 11000    0 timeout 900     1000 12000    0 unknown .37  25 5.2  0 unknown .15 23 1.6 0 true 750   260 11000 2 true 2.8  16 25   2 timeout 900   1400 10000 0 timeout 900   1300 11000 0 timeout 900   11000 5900 0
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i false(valid-deref) .32 31 3.4  -16 error (42) 850    2100 8800    0 true .041 7.9 .16 2 error (1) .42 39 3.9 0 error (1) .42 38 3.7 0 error 2.8 220 20 0 unknown 220    120 2600   0 true 100   4700 1400 2 timeout 900     13000 14000    0 out of memory 340     15000 4100    0 unknown .19  24 2.2  0 unknown .11 24 1.7 0 true 750   210 8400 2 true 4.1  20 58   2 true 32   570 300 2 true 310   1300 4400 2 true 94   800 1100 2
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i false(valid-deref) 2.1  120 25    -16 error (134) 200    14000 2400    0 true .032 8.0 .17 2 error (1) .42 37 3.8 0 error (1) .43 40 3.9 0 error 2.6 220 20 0 timeout 900    970 10000   0 out of memory 170   15000 2200 0 out of memory 570     15000 7500    0 out of memory 260     15000 3000    0 unknown .18  24 2.1  0 unknown .13 23 1.7 0 true 750   230 8800 2 true 3.4  24 44   2 timeout 900   1100 12000 0 timeout 900   1600 11000 0 timeout 900   910 12000 0
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i false(valid-deref) .32 28 2.9  -16 error (42) 850    2100 4700    0 true .030 8.2 .21 2 error (1) .42 37 4.1 0 error (1) .43 40 3.4 0 error 2.6 220 24 0 unknown 110    32 1500   0 true 13   340 180 2 timeout 900     12000 8000    0 out of memory 490     15000 6700    0 out of memory 490     15000 6600    0 unknown .13 24 1.6 0 true 750   180 9300 2 true 1.6  15 21   2 true 13   530 110 2 true 27   580 280 2 true 16   640 130 2
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i false(valid-deref) .42 37 6.0  -16 error (42) 850    300 3900    0 true .039 8.0 .18 2 error (1) .42 40 4.0 0 error (1) .40 37 3.7 0 error 2.5 220 23 0 unknown 900    370 10000   0 timeout 900   9700 7200 0 timeout 900     3100 13000    0 timeout 900     7000 11000    0 unknown .17  25 2.0  0 unknown .11 23 1.8 0 true 750   600 6900 2 timeout (timeout) 900    580 12000   0 true 31   530 320 2 timeout 900   1400 13000 0 true 49   720 540 2
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i timeout 900    27 11000    0 error (42) 850    920 4900    0 true .078 44   .44 2 error (1) .43 40 3.8 0 error (1) .43 37 3.8 0 error 2.7 220 22 0 unknown 890    120 9900   0 out of memory 38   15000 460 0 timeout 900     170 11000    0 timeout 900     230 10000    0 unknown .18  24 2.2  0 unknown .11 23 1.8 0 true 750   320 7500 2 timeout (timeout) 900    800 9900   0 true 39   720 420 2 timeout 900   1700 12000 0 true 85   660 1100 2
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i timeout 900    27 13000    0 error (42) 850    7600 3100    0 true .029 8.2 .19 2 error (1) .43 37 3.6 0 error (1) .43 40 3.6 0 error 2.7 220 24 0 unknown 900    590 14000   0 out of memory 45   15000 530 0 unknown .18  25 1.3  0 unknown .15  24 1.7  0 unknown .16  25 1.9  0 unknown .13 25 1.8 0 timeout 750   290 7400 0 timeout (timeout) 900    800 7600   0 timeout 900   900 14000 0 timeout 900   1500 12000 0 timeout 900   1200 10000 0
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i error (5) .20 38 1.8  0 error (42) 850    8300 5000    0 true .033 8.1 .14 2 error (1) .43 37 3.5 0 error (1) .39 40 3.6 0 error 10   220 14 0 true 1.1  29 13   2 true 15   510 180 2 timeout 900     14000 12000    0 out of memory 550     15000 7000    0 out of memory 480     15000 5700    0 unknown .14 23 1.6 0 true 750   240 9200 2 true .23 10 2.4 2 true 23   510 200 2 true 17   510 150 2 true 19   510 170 2
array-memsafety/selectionsort-alloca_true-valid-memsafety.i out of memory 510    15000 3600    0 error (134) 63    14000 640    0 true .023 8.1 .16 2 error (1) .43 37 3.8 0 error (1) .43 38 3.7 0 error 2.5 220 21 0 unknown 890    310 6500   0 timeout 900   12000 6400 0 timeout 900     680 6500    0 timeout 900     570 11000    0 timeout 900     610 8200    0 unknown .11 23 1.8 0 true 750   470 6600 2 true .24 11 2.4 2 true 13   490 99 2 timeout 900   2100 12000 0 true 14   570 110 2
array-memsafety/stroeder1-alloca_true-valid-memsafety.i timeout 900    5700 8100    0 error (134) 76    14000 1000    0 true .029 7.9 .16 2 error (1) .40 37 3.9 0 error (1) .41 37 4.0 0 error 2.5 220 21 0 unknown 100    53 1400   0 true 4.3 400 50 2 out of memory 320     15000 3800    0 out of memory 190     15000 2400    0 out of memory 190     15000 2400    0 unknown .13 22 1.7 0 true 750   180 8200 2 true .23 10 2.8 2 true 9.4 470 73 2 true 9.9 480 88 2 true 10   470 80 2
array-memsafety/stroeder2-alloca_true-valid-memsafety.i error (8) .17 26 1.6  0 error (134) 61    14000 560    0 true .040 8.2 .18 2 error (1) .46 37 3.8 0 error (1) .44 40 3.9 0 error 2.5 220 22 0 unknown 890    270 8800   0 timeout 900   14000 1800 0 timeout 900     3500 9200    0 timeout 900     360 12000    0 timeout 900     440 10000    0 unknown .15 25 2.0 0 true 760   660 6000 2 true 1.2  13 15   2 true 10   490 79 2 true 21   710 200 2 true 12   480 83 2
array-memsafety/strreplace-alloca_true-valid-memsafety.i false(valid-deref) .32 29 3.1  -16 error (134) 220    14000 1300    0 true .052 43   .44 2 error (1) .44 40 4.0 0 error (1) .41 40 3.8 0 error 2.5 220 22 0 unknown 890    59 10000   0 timeout 900   1000 11000 0 timeout 900     150 14000    0 timeout 900     370 11000    0 timeout 900     460 14000    0 unknown .14 24 1.7 0 true 750   130 9100 2 true .22 11 2.6 2 true 20   500 180 2 true 26   590 240 2 true 19   590 140 2
array-memsafety/subseq-alloca_true-valid-memsafety.i false(valid-deref) .24 27 2.6  -16 error (42) 850    1900 4700    0 true .031 8.0 .15 2 error (1) .41 37 4.1 0 error (1) .39 37 3.7 0 error 2.5 220 23 0 unknown 890    59 13000   0 true 890   2200 9400 2 timeout 900     340 12000    0 timeout 900     620 13000    0 timeout 900     820 11000    0 unknown .10 24 1.8 0 true 750   210 8600 2 timeout (timeout) 900    570 6900   0 true 60   590 730 2 true 470   1600 5900 2 true 91   730 1000 2
array-memsafety/substring-alloca_true-valid-memsafety.i false(valid-deref) .25 29 2.5  -16 error (42) 850    10000 6500    0 true .030 8.2 .17 2 error (1) .42 39 4.1 0 error (1) .40 37 3.5 0 error 2.5 220 22 0 unknown 900    220 12000   0 out of memory 41   15000 560 0 timeout 900     650 13000    0 timeout 900     1400 12000    0 timeout 900     2000 11000    0 unknown .11 27 1.8 0 true 750   510 6600 2 timeout (timeout) 900    760 9700   0 true 61   620 770 2 timeout 900   1500 11000 0 true 50   820 520 2
array-examples/relax_false-valid-deref.i false(valid-deref) .23 27 2.2  1 false(valid-deref) .20 20 1.9  1 unknown .028 8.0 .16 0 error (1) .45 40 3.9 0 error (1) .41 40 4.0 0 error 2.7 220 22 0 false(valid-deref) .63 29 7.4 1 false(valid-deref) 900   5400 1900 1 false(valid-deref) .26  25 2.9  1 false(valid-deref) .25  25 3.0  1 false(valid-deref) .28  25 3.3  1 unknown .15 24 1.7 0 true 750   220 8800 -32 timeout (timeout) 900    2300 7400   0 false(valid-deref) 6.1 330 44 1 false(valid-deref) 23   340 200 1 false(valid-deref) 6.4 320 53 1
array-examples/sanfoundry_24_false-valid-deref.i out of memory 320    15000 2800    0 error (42) 850    6200 5200    0 false(valid-deref) .027 7.9 .15 1 error (1) .44 37 4.0 0 error (1) .41 38 3.4 0 timeout 900   2900 1700 0 unknown 440    100 830   0 true 61   590 120 -32 timeout 900     680 10000    0 out of memory 630     15000 9200    0 out of memory 370     15000 4800    0 timeout 900    2600 5300   0 false(valid-deref) 6.2 92 79 1 timeout (timeout) 900    3500 6500   0 timeout 900   1500 15000 0 timeout 900   1300 14000 0 timeout 900   1700 14000 0
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 900    14000 10000    0 out of memory 74    15000 930    0 false(valid-deref) .024 7.9 .13 1 error (1) .45 40 3.9 0 error (1) .41 37 3.8 0 timeout 900   3700 12000 0 unknown 67    31 920   0 true 5.4 620 63 -32 timeout 900     1100 9400    0 out of memory 870     15000 5400    0 unknown .11  23 .66 0 timeout 900    6000 9100   0 false(valid-deref) 8.4 95 100 1 timeout (timeout) 900    1600 9100   0 timeout 900   2000 12000 0 timeout 900   1400 13000 0 timeout 900   1900 14000 0
array-examples/standard_strcpy_original_false-valid-deref.i timeout 900    14000 9800    0 out of memory 74    15000 960    0 false(valid-deref) .023 7.8 .11 1 error (1) .42 38 3.4 0 error (1) .39 38 3.7 0 timeout 900   3700 11000 0 unknown 67    31 710   0 true 5.4 620 65 -32 timeout 900     1100 11000    0 out of memory 470     15000 4900    0 unknown .11  23 .69 0 timeout 900    5300 10000   0 false(valid-deref) 11   100 160 1 timeout (timeout) 900    1800 11000   0 timeout 900   1400 14000 0 timeout 900   1500 13000 0 timeout 900   1700 14000 0
../../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 69 12000   110000 110000 -440 69 29000   440000 200000 18 69 2.6  970 16   116 69 30 2700 260 0 69 29 2600 260 0 69 3800 36000 34000 6 69 30000   11000 330000 20 69 26000 440000 240000 -39 69 41000   320000 470000 18 69 36000   360000 440000 18 69 22000   140000 260000 18 69 2700    15000 25000 7 69 37000 18000 400000 82 69 15000   19000 160000 83 69 16000 50000 220000 86 69 28000 65000 370000 64 69 18000 76000 220000 84
    correct results 19 4.6 510 45 24 18 3.8 460 39 18 68 2.5  960 16   116 0 0 6 14 1400 120 6 19 11   540 130 20 33 8000 61000 78000 57 18 3.4 430 38 18 18 3.2 440 38 18 18 3.3 430 39 18 7 .97 150 13 7 67 35000 17000 390000 114 48 55   650 640 83 52 860 24000 8100 86 41 2400 24000 29000 64 51 1400 26000 14000 84
        correct true 5 2.3 150 24 10 0 48 1.9  710 12   96 0 0 0 1 1.1 29 13 2 24 6000 39000 67000 48 0 0 0 0 47 35000 15000 390000 94 35 49   500 580 70 34 720 18000 7100 68 23 2200 17000 27000 46 33 1100 20000 11000 66
        correct false 14 2.3 360 21 14 18 3.8 460 39 18 20 .68 250 4.3 20 0 0 6 14 1400 120 6 18 9.9 510 120 18 9 2000 22000 11000 9 18 3.4 430 38 18 18 3.2 440 38 18 18 3.3 430 39 18 7 .97 150 13 7 20 58 1700 750 20 13 6.2 150 64 13 18 130 6500 1000 18 18 190 7000 1600 18 18 310 6800 3100 18
    correct-unconfimed results 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
    incorrect results 29 14   1100 150 -464 0 0 0 0 0 0 3 72 1800 250 -96 0 0 0 0 1 750 220 8800 -32 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 3 72 1800 250 -96 0 0 0 0 1 750 220 8800 -32 0 0 0 0
        incorrect false 29 14   1100 150 -464 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (69 tasks, max score: 117) -440 18 116 0 0 6 20 -39 18 18 18 7 82 83 86 64 84
Run set 2ls.sv-comp17.MemSafety-Arrays cbmc.sv-comp17.MemSafety-Arrays ceagle.sv-comp17.MemSafety-Arrays cpa-bam-bnb.sv-comp17.MemSafety-Arrays cpa-kind.sv-comp17.MemSafety-Arrays cpa-seq.sv-comp17.MemSafety-Arrays depthk.sv-comp17.MemSafety-Arrays esbmc.sv-comp17.MemSafety-Arrays esbmc-falsi.sv-comp17.MemSafety-Arrays esbmc-incr.sv-comp17.MemSafety-Arrays esbmc-kind.sv-comp17.MemSafety-Arrays predatorhp.sv-comp17.MemSafety-Arrays smack.sv-comp17.MemSafety-Arrays symbiotic4.sv-comp17.MemSafety-Arrays uautomizer.sv-comp17.MemSafety-Arrays ukojak.sv-comp17.MemSafety-Arrays utaipan.sv-comp17.MemSafety-Arrays