debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Merge	Jason Koenig	2011-06-29
\|\
* \|	Added returns with parameters to printer.	Jason Koenig	2011-06-29
\| \|
* \|	Fixed bug in compiler relating to returns with parameters.	Jason Koenig	2011-06-29
\| \|
* \|	Added regression tests for new return statements with parameters.	Jason Koenig	2011-06-29
\| \|
* \|	Stable implementation of return statements with parameters.	Jason Koenig	2011-06-29
\| \|
* \|	Made Receiver mutable, as this cannot be linked properly by the parser.	Jason Koenig	2011-06-29
\| \|
\| *	Merge	Rustan Leino	2011-06-29
\| \|\
\| * \|	Boogie: use (WEIGHT 0) with the select-of-store axioms	Rustan Leino	2011-06-29
\| \| \|
\| * \|	Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions	Rustan Leino	2011-06-29
\| \| \|
* \| \|	Initial implementation of return statments with parameters.	Jason Koenig	2011-06-29
\| \|/ \|/\|
* \|	Removed development comments.	Jason Koenig	2011-06-29
\| \|
* \|	Merge	Jason Koenig	2011-06-29
\|\ \
* \| \|	Added regression test file LoopModifies.dfy.	Jason Koenig	2011-06-29
\| \| \|
\| * \|	Boogie build succeeded, 1 test(s) failed	CodeplexBot	2011-06-29
\|/ /
* \|	Merge	Jason Koenig	2011-06-28
\|\ \
* \| \|	Added regression test for loop modifies clauses.	Jason Koenig	2011-06-28
\| \| \|
* \| \|	Changed regression test answer for dafny0 to reflect new error messages.	Jason Koenig	2011-06-28
\| \| \|
* \| \|	Initial modifies on loops implementation. Still some errors remaining.	Jason Koenig	2011-06-28
\| \| \|
\| * \|	ported all the counterexample code to Michal's new Model class; the goal is ↵	Unknown	2011-06-27
\|/ / \| \| \| \| \| \|	to eliminate the class ErrorModel from the codebase.
* \|	Boogie build succeeded	CodeplexBot	2011-06-27
\| \|
* \|	Fixed non-incremental option of stratified inlining	Unknown	2011-06-27
\| \|
* \|	FindLeastToVerify: accept multiple procedures	Unknown	2011-06-26
\| \|
* \|	Call PostOrderVisitIterative by default	Unknown	2011-06-26
\| \|
* \|	Added an iterative version of PostOrderVisit (but it is not called)	Unknown	2011-06-26
\| \|
* \|	Avoid restarting the theorem prover for stratified inlining because it	Unknown	2011-06-25
\| \| \| \| \| \| \| \| \| \|	can lose context. Added a cache for FindLeastToVerify
* \|	early clearing of live variables and incarnation maps	qadeer	2011-06-24
\| \|
* \|	further refactoring	qadeer	2011-06-24
\| \|
* \|	Merge	qadeer	2011-06-24
\|\ \
* \| \|	extra test files	qadeer	2011-06-24
\| \| \|
* \| \|	fixes to z3api	qadeer	2011-06-24
\| \| \|
\| * \|	Boogie build succeeded	CodeplexBot	2011-06-24
\|/ /
* \|	Merge	qadeer	2011-06-23
\|\ \
* \| \|	implementation of iterative LetVC	qadeer	2011-06-23
\| \| \|
\| * \|	Merge	Jason Koenig	2011-06-23
\| \|\ \
\| * \| \|	Added loop modifies clause syntax.	Jason Koenig	2011-06-23
\| \| \|/ \| \|/\|
* \| \|	Merge	qadeer	2011-06-23
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	bug fix in translation of dispatch continuation	qadeer	2011-06-23
\| \| \|
\| * \|	Didn't intend to include Z3api by default	Unknown	2011-06-23
\| \| \|
\| * \|	Bug fix for trace generation with extractLoop option	Unknown	2011-06-23
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	Bug fix for trace generation with extractLoop option	Unknown	2011-06-23
\| \| \|
* \| \|	clean up in z3api	qadeer	2011-06-22
\|/ /
* \|	Merge	qadeer	2011-06-22
\|\\|
* \|	partial fixes to these regressions	qadeer	2011-06-22
\| \|
* \|	various fixes to port to latest version of Microsoft.Z3.dll	qadeer	2011-06-22
\| \|
\| *	Merge	Rustan Leino	2011-06-21
\| \|\ \| \|/ \|/\|
\| *	Dafny: bug fix in generating IsCanonicalBoolBox predicates	Rustan Leino	2011-06-21
\| \|
* \|	Merge	qadeer	2011-06-20
\|\\|
* \|	Translate IConditional exactly the same way as IConditionalStatement to ↵	qadeer	2011-06-20
\| \| \| \| \| \| \| \|	account for side-effects in expressions
\| *	Merge	Rustan Leino	2011-06-20
\| \|\ \| \|/ \|/\|
\| *	Dafny: better error message when "decreases *" is attempted on a function or ↵	Rustan Leino	2011-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	method Dafny: fixed compilation bug with parallel assignment involving a ghost LHS Dafny: added sequence-to-set conversion if a function's reads clause is used implicitly as the decreases clause