[klee-dev] Using KLEE in LLVM Pass

[Khaled Yakdan]

Hi,

I am working on an LLVM analysis pass where I need to reason about whether
two values are equal. I am wondering if KLEE can be used for this purpose.
One idea would be to symbolically execute the given function and then ask
the solver if two expressions of interest are actually equal. Can KLEE be
used as previously described? If yes, I would be grateful if you can
provide some hints how this can be realized.

Also, a more general question. Can KLEE be used as a library in other
projects?

Thanks
-------------- next part --------------
HTML attachment scrubbed and removed