[klee-dev] klee_print_expr in SMTLIB2 format

[Nowack, Martin]

Hi,

Currently, only queries can be printed.
Extend your code to create an empty constraint set and use the expression (arguments[0]) as an argument:

```

std::vector<ref<Expr>> emptyCS;

ConstraintManager emptyCM(emptyCS);

Query query(emptyCM, arguments[0]);

```

Hope that helps.

Cheers,
Martin

On 27. Jul 2019, at 13:19, Ramanuj Chouksey <ramanuj17291729 at gmail.com<mailto:ramanuj17291729 at gmail.com>> wrote:

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<mailto: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<mailto: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<mailto: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<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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