Age | Commit message (Expand) | Author |
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 |
2009-06-07 | Diagnose some more syntax errors instead of crashing. | Daniel Dunbar |
2009-06-07 | Fix typo. | Daniel Dunbar |
2009-06-07 | Make sure to include arrays to be evaluated in the set of used arrays. | Daniel Dunbar |
2009-06-07 | Implement array declarations. | Daniel Dunbar |
2009-06-07 | Don't delete decls before parsing is complete. | Daniel Dunbar |
2009-06-07 | Update test case. | Daniel Dunbar |
2009-06-07 | Make sure to make up a valid VersionResult on failures. | Daniel Dunbar |
2009-06-07 | Eliminate anonymous versions. | Daniel Dunbar |
2009-06-06 | Document the KQuery language. | Daniel Dunbar |
2009-06-05 | Fixed a division by zero triggered by straight-line code in klee-stats. | Cristian Cadar |
2009-06-05 | Moved PrintStats.py to tool/klee-stats/ | Cristian Cadar |
2009-06-05 | Support counter example queries (at least, the restricted set that we | Daniel Dunbar |
2009-06-05 | Support the extended query command syntax. | Daniel Dunbar |
2009-06-05 | Add Expr::is{Zero,True,False} methods. | Daniel Dunbar |
2009-06-05 | Turn an assert into a parse failure. | Daniel Dunbar |
2009-06-05 | Don't evaluate queries if there were parse failures. | Daniel Dunbar |
2009-06-05 | Add evaluation support to kleaver (now the default). | Daniel Dunbar |
2009-06-05 | llvm::Casting support for Kleaver AST nodes. | Daniel Dunbar |
2009-06-05 | Set svn:ignore properties. | Daniel Dunbar |
2009-06-05 | Clean up a number of unused variable warnings when building w/o | Daniel Dunbar |
2009-06-05 | Remove some unnecessary uses of C++ exceptions. | Daniel Dunbar |
2009-06-05 | Expr::print shouldn't introduce line breaks or extra formatting. | Daniel Dunbar |
2009-06-05 | Add test case. | Daniel Dunbar |
2009-06-05 | (llvm up) Update klee for introduction of f{add,sub,mul} instructions. | Daniel Dunbar |
2009-06-04 | Make ConstantExpr's value and constructor private. | Daniel Dunbar |