Hi, On 4 April 2016 at 16:22, Sumit Kumar <sumit686...@gmail.com> wrote: > Hi, > > I was reading Expr.h file when I came across this comment: > > <b>Steps required for adding an expr</b>: > -# Add case to printKind > -# Add to ExprVisitor > -# Add to IVC (implied value concretization) if possible > > Can anyone please explain the above in anyway possible (brief / detail) ?
I have been adding a lot of new expressions to my fork of KLEE recently so I can tell you what I've found to be the bare minimum. 1. Add class declaration and a corresponding ``Expr::Kind`` to ``Expr.h`` and implementation to ``Expr.cpp``. You might need to provide an implementation of ``computeHash()``, ``create()`` and ``compareContents()`` depending on which existing class your derive form. You will need to add your new Expr class to ``Expr::printKind()``. 2. Add support for your new Expr class to ExprVisitor. 3. Add support for your new Expr class to STPBuilder.cpp and/or Z3Builder.cpp depending on which solver you care about it. If you want to be able to print your constraints as SMT-LIBv2 you'll need to add support for your new Expr class in ``ExprSMTLIBPrinter``. Similarly you will need to put some extra work in to add support for your new Expr class to the KQuery printer/parser. Hope that helps, Dan. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
