<span style='font-family:Verdana'><span style='font-size:12px'><div>What did you mean by "array access bounds expressions"?</div><div>If you want to do something along the lines of constraint-based bounds check elimination, you can check out SAFECode.</div><div>I don't think KLEE would be very useful for proving the safety of memory accesses, rather the lack thereof. Also, KLEE doesn't handle symbolic array sizes.</div><div> </div><div>If you can give more details about your project, someone might be able to help out a bit more. : )</div><div> </div><div>H.</div><div><div><p style="margin:0px; padding:0px;" > </p><blockquote style="border-left: 1px solid #CCC; padding-left: 5px; margin-left: 5px; margin-bottom: 0px; margin-top: 0px; margin-right: 0px;" type="cite"><p style="margin:0px; padding:0px;" ><span style="font-family:Verdana"><span style="font-size:12px">----- Original Message -----</span></span></p><p style="margin:0px; padding:0px;" ><span style="font-family:Verdana"><span style="font-size:12px">From: Eric Lu</span></span></p><p style="margin:0px; padding:0px;" ><span style="font-family:Verdana"><span style="font-size:12px">Sent: 06/04/13 10:20 AM</span></span></p><p style="margin:0px; padding:0px;" ><span style="font-family:Verdana"><span style="font-size:12px">To: LLVM Developers Mailing List</span></span></p><p style="margin:0px; padding:0px;" ><span style="font-family:Verdana"><span style="font-size:12px">Subject: [LLVMdev] generate ponter/array access bounds expressions</span></span></p> <div><div>Hello, <div>  </div><div style="">  I want to generate pointer/array access bounds expressions within LLVM. I have read some docs about symbolic and KLEE, but I am not sure if there are some better methods. </div><div style="">  </div><div style="">  I guess it is possible to do it with symbolic execution[1]， but I think it is a little complex to do my project with klee. It seems I need to do some work like in [1] to KLEE to finish my project.</div><div style=""> </div><div style="">   And I wonder if  there are some better methods available in LLVM IR?  I.E. are there exmple code  in SAFECode? </div><div style=""> </div><div style="">Or are there some better ways to do this?</div><div style=""> </div><div style=""> </div><div style="">[1] <span style=""><span style="font-size:7pt;font-family:'Times New Roman'">  </span></span><span style="">Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions</span></div><div style=""> </div><div style=""> </div><div style=""><span style="">Thanks!</span></div><div style=""> </div><div style=""><span style="">Eric</span></div><p style="margin:0px; padding:0px; margin-left:35.45pt"> </p></div></div></blockquote><p style="margin:0px; padding:0px;" > </p></div></div></span></span>