Age | Commit message (Expand) | Author |
2009-06-12 | Removed unused file. | Cristian Cadar |
2009-06-10 | Move declaration of vc_DeleteExpr outside of function. | Daniel Dunbar |
2009-06-10 | Updated the SMT test driver. Other small changes to parser_temp.h and | Cristian Cadar |
2009-06-10 | Removed CVC3's Parser class. | Cristian Cadar |
2009-06-10 | Wrote a new SMTParser that inherits from klee::expr::Parser. | Cristian Cadar |
2009-06-10 | (Missed save) Move Array construction out of MemoryObject into ObjectState. | Daniel Dunbar |
2009-06-10 | Move Array construction out of MemoryObject into ObjectState. | Daniel Dunbar |
2009-06-10 | Change ExecutionState::symbolics to include both the MemoryObject and the | Daniel Dunbar |
2009-06-10 | Use Arrays instead of MemoryObject where possible. | Daniel Dunbar |
2009-06-10 | Fix a bug in the logging solver which was printing the expression in a | Daniel Dunbar |
2009-06-10 | Added a temporary driver to test the parser. | Cristian Cadar |
2009-06-10 | Changed expression nodes to be ExprHandle (instead of ExprHandle*), and | Cristian Cadar |
2009-06-09 | Use env instead of hard coding python path. | Daniel Dunbar |
2009-06-09 | More constant Array support. | Daniel Dunbar |
2009-06-09 | Do not compile SMT parser by default. Removed automatically generated | Cristian Cadar |
2009-06-09 | Made expression nodes int the SMT parser be pointers to ExprHandle. | Cristian Cadar |
2009-06-09 | Add initial support for constant Arrays. | Daniel Dunbar |
2009-06-09 | Remove Array::object. | Daniel Dunbar |
2009-06-09 | Remove Array::id. | Daniel Dunbar |
2009-06-09 | Switch Array* print-outs to use name instead of ID, and update a few | Daniel Dunbar |
2009-06-09 | Use Array* to map objects instead of id. | Daniel Dunbar |
2009-06-09 | Add Array::name field, initialized but not used for anything yet. | Daniel Dunbar |
2009-06-09 | Kill off UpdateList::isRooted flag. | Daniel Dunbar |
2009-06-09 | Remove unnecessary include. | Daniel Dunbar |
2009-06-09 | Set svn:ignore on lib/SMT/{Debug,Release} | Daniel Dunbar |
2009-06-09 | Quick hack to build SMT LLVM style. | Daniel Dunbar |
2009-06-09 | Remove exception.h and parser_exception.h | Daniel Dunbar |
2009-06-09 | Kill off uses of C++ exceptions. | Daniel Dunbar |
2009-06-09 | Remove lang.h again. | Daniel Dunbar |
2009-06-09 | Get rid of Parser language member, we only use SMTLIB. | Daniel Dunbar |
2009-06-09 | Revert r73105, I think I was too hasty in killing this. | Daniel Dunbar |
2009-06-09 | Fix a compiler warning | Daniel Dunbar |
2009-06-09 | Remove lang.h, it is unused. | Daniel Dunbar |
2009-06-08 | Made the SMTLIB parser compile. Commented out most of the grammar in | Cristian Cadar |
2009-06-08 | More changes needed to make the SMTLIB parser compile. | Cristian Cadar |
2009-06-08 | Removed ValidityChecker field from ParserTemp. Temporarily replaced | Cristian Cadar |
2009-06-08 | Removed support for the PL and Lisp languages. | Cristian Cadar |
2009-06-08 | Added CVC3's parser for the SMT-LIB grammar. | Cristian Cadar |
2009-06-08 | FastCexSolver: Start implementing exact value propogation. | Daniel Dunbar |
2009-06-08 | Add some query logs in utils/data/Queries (for 3 and 4 byte pcregrep) | Daniel Dunbar |
2009-06-08 | FastCexSolver: Stub out infrastructure for propogating exact values & proving | Daniel Dunbar |
2009-06-08 | FastCexSolver: Add exact value contents to CexObjectData. | Daniel Dunbar |
2009-06-08 | FastCexSolver: Rename forceExprTo* to propogatePossible* | Daniel Dunbar |
2009-06-08 | FastCexSolver: Lazily initialize object values and kill off ObjectFinder class. | Daniel Dunbar |
2009-06-08 | Kill off Concat::is[248]ByteConcat, and fix FastCexSolver for this case. | Daniel Dunbar |
2009-06-08 | Add klee::createDummySolver, the dummy solver always fails. | Daniel Dunbar |
2009-06-08 | Cleanup FastCexSolver: | Daniel Dunbar |
2009-06-08 | Fix a mistake in previous commit to turn asserts -> parse errors. | Daniel Dunbar |
2009-06-08 | kleaver: Use raw_ostream, and print some stats. | Daniel Dunbar |
2009-06-07 | Make sure that ExprEvaluator will fold constant expressions (klee never creates | Daniel Dunbar |