generate ponter/array access bounds expressions

Hello,

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[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.

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?

[1] Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions

Thanks!

Eric