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.
I guess it is possible to do it with symbolic execution， but I think it is a little complex to do my project with klee. It seems I need to do some work like in  to KLEE to finish my project.
And I wonder if there are some better methods available in LLVM IR? I.E. are there exmple code in SAFECode?
Or are there some better ways to do this?
 Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions