[klee-dev] klee_print_expr in SMTLIB2 format

[Ramanuj Chouksey]

Dear sir,
As suggested, I checked the ExprSMTLIBPrinter.cpp and
SpecialFunctionHandler.cpp.
Now I am able to print the constraints in SMTLIB2 format along with
symbolic expression in the klee_print_expr by adding the following
lines.

ExprSMTLIBPrinter printer;
printer.setOutput(llvm::errs());
Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
printer.setQuery(query);
printer.generateOutput();

However, I am not able to find out a way to print the symbolic
expression of a given variable in SMTLIB2 format.
May I get some more suggestions regarding this?

Thanking You,
Ramanuj Choukey,
Research Scholar,
CSE, IIT Guwahati,
India.

On Fri, Jul 26, 2019 at 3:04 AM Cadar, Cristian <c.cadar at imperial.ac.uk> wrote:
>
> No, but you should be able to accomplish this easily, by changing the
> code in handlePrintExpr() to use the code for printing expressions in
> the SMT-LIBv2 format (ExprSMTLIBPrinter).
>
> Best,
> Cristian
>
> On 25/07/2019 12:43, Ramanuj Chouksey wrote:
> > Hi,
> > How do I convert the symbolic expression printed by klee_print_expr
> > into SMTLIB2 format? Is it possible using kleaver?
> >
> > Thanking you,
> > Ramanuj,
> > Research Scholar,
> > CSE, IIT Guwahati,
> > India.
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev