Abstract Interpretation in LLVM

Question

I need to use abstract interpretation to do some analysis using LLVM. Is this possible? or I need to use analysis tools easier. If I could do that by LLVM , which classes would help me to formulate the statements from the original source code to get the relations between the variables (and the possible ranges of values for each variable)

Answer 1

You can have a look at KLEE which is a symbolic interpreter for LLVM bitcode: https://github.com/klee