generate ponter/array access bounds expressions

What did you mean by “array access bounds expressions”?
If you want to do something along the lines of constraint-based bounds check elimination, you can check out SAFECode.
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.

If you can give more details about your project, someone might be able to help out a bit more. : )

H.