~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2014-12-02	Fix typo	Dan Liew

2014-12-02	Add a comment explaining why the query expr is being negated.	Dan Liew

2014-12-02	The printing of constraints and the QueryExpr have been merged into a	Dan Liew
	single method with two different implementations. There is one version of this method for human readability (printHumanReadableQuery()) and a version for machine consumption (printMachineReadableQuery()). The reason for having two versions is because different behaviour is needed in different scenarios * In machine readable mode the entire query is printed inside a single ``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate as much as possible. * In human readable mode each constraint and query expression is printed inside its own ``(assert ...)`` unless the abbreviation mode is ABBR_LET in which case all constraints and query expr are printed inside a single ``(assert ...)`` much like in the machine readable mode Whilst I was here I also fixed a bug handling identation when printing ``(let ...)`` expressions in printAssert()
2014-12-02	Implement :named and let abbreviation modes in ExprSMTLIBPrinter	Raimondas Sasnauskas
	* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
2014-05-29	Fix header	Martin Nowack

2014-05-29	Avoid non-explicit use of functions from std namespace in KLEE	Martin Nowack

2014-05-29	Remove #include <iostream> to avoid static constructors	Martin Nowack
	iostream injects static constructor function into every compilation unit. Remove this to avoid it.
2014-05-29	Refactoring from std::ostream to llvm::raw_ostream	Martin Nowack
	According to LLVM: lightweight and simpler implementation of streams.
2014-05-11	Fix the logic in ExprSMTLIBPrinter::getSort	Peter Collingbourne
	This now corresponds to the sorts of the operations we emit, as far as I can tell. Read is one example of an operation that now works correctly (with 1-bit array ranges). It's also possible (but not very useful, and I don't think KLEE can produce it) for other operations such as Add to operate on 1-bit values, and this patch also fixes those.
2014-04-02	Modify the SMT-LIB printer to declare arrays in a deterministic ↵	Peter Collingbourne
	(alphabetical) order.
2014-03-09	Use clang-format to reformat SMT-LIB printer in LLVM style.	Peter Collingbourne

2013-05-08	Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to ↵	Cristian Cadar
	negateQueryExpression() to make it clear what it does." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@181445 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24	Nice patch by Dan Liew that adds support for printing queries in the	Cristian Cadar
	SMTLIB format (part of his MSc project work). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8