On Thu, Jul 21, 2011 at 03:36:13PM +0200, Vitaly Chipounov wrote: > Hi, > > Is there a tool to encode a constraint solver query (e.g., from > queries.pc) into C code that, when compiled to LLVM and run in KLEE, > would generate the exact same query as in the log? This may help me > speed up debugging the attached query that is reported as invalid by > KLEE but valid by kleaver.
I have been working on a C expression printer in my KLEE-FP branch, and I hope to make this work open source very soon. It only handles expressions, not queries, but I imagine that queries would be a relatively trivial extension. Thanks, -- Peter _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
