[klee-dev] Question about interface and constraint solving in klee

[Shiyu Dong]

Hi all,

I am working on klee and trying to integrate it with another solver (CVC4) to do some test. I found that klee communicates with STP by calling the c_interface.h. The good thing is that the solver I am using has the same interface (same name) and some of the inside functions have overlaps. I'm wondering if there is anythings other than the STPBuilder that I need to change in order to make this integration, because Daniel has mentioned that he did something so that klee can be separated from STP(http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00030.html).

Also, I know klee runs based on the .o file generated by llvm. So I want to ask in what language does klee represent the constraints and passing them to the solver? Is it in still in readable language such as SMT or CVC, or some lower level representation?

Last question about the big picture of klee, in order to have a better understanding about how klee deals with constraints, what part of the code should I pay more attention to?

Thanks in advance for helping me with these basic questions.

Best Regards,
Shiyu
--
Shiyu Dong
Graduate Student
Electrical & Computer Engineering
University of Texas at Austin
Tel: (512) 927-7817
E-mail: shiyud at utexas.edu 

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