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
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev