Hi, I have seen on stackoverflow and on some emails from 2011 on this list that it was somewhat possible to run Klee's symbolic execution without directly modifying the code and to show the path conditions using seed (it was suggested to grep over the --help of klee but unfortunately it was too little information from there for me to grasp). I have also noticed that when Klee generate errors it tracks down the source code line (according to my understanding of the tutorial example on ER). Thus:
(1) Is it possible currently to use Klee without modifying the code directly? Which cases are possible? Anything else that could allow to play with Klee from within another program more directly would also be helpful (so far I didn't see any), for example like Clang offers libclang,python wrappers, etc. (2) How can I use seed (or maybe any other alternative) to track down the path conditions using Klee? I see that the tests cases only gives the input if I follow the tutorials and check the .ktests (3) Is it possible to associate the source line of a given path condition assuming (2) i possible? Thank you, Carlos Andrade http://carlosandrade.co
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
