debian-boogie - Debian packaging for Boogie

	Commit message (Expand)	Author	Age
...
* \|	Dafny: did a little to extend the support of labeled statements in refinement...	Unknown	2012-09-10
* \|	Dafny: improved checking of inherited postconditions (in refinements)	Unknown	2012-09-10
* \|	Boogie: added /tracePOs option for printing out number of proof obligations w...	Unknown	2012-09-10
\| *	Chalice: implemented automatic trigger-finding for quantifiers in user-suppli...	Unknown	2012-09-11
* \|	Merge	Rustan Leino	2012-09-10
\|\ \
* \| \|	ignore Chalice/bin	Rustan Leino	2012-09-10
* \| \|	Merge	Rustan Leino	2012-09-10
\|\ \ \
\| * \| \|	Find implementations of interface methods for dynamic dispatch, not just	Unknown	2012-09-09
* \| \| \|	DafnyExtension: addressed a class initialization order problem	Rustan Leino	2012-09-09
* \| \| \|	Dafny: allow 'decreases *' (that is, non-terminating recursion) on tail-recur...	Rustan Leino	2012-09-09
\| * \| \|	Avoid creating a dynamic dispatch table for GetHashCode and ToString: it ends	Unknown	2012-09-09
\| * \| \|	Moved the statement traverser's operand stack (used for explicit push/pop/dup	Unknown	2012-09-09
\|/ / /
\| \| *	Chalice: added findFunctionAppsContaining(..) to Expression, which finds all ...	Unknown	2012-09-08
\| \| *	Chalice: implemented the final cases of the "inside" feature for predicates. ...	Unknown	2012-09-08
* \| \|	Merge	Unknown	2012-09-07
\|\ \ \
* \| \| \|	Dafny: Added detection and support for tail recursive calls (and an optional...	Unknown	2012-09-07
* \| \| \|	DafnyExtension: new color (violet) for buffer snapshot sent to the verifier	Unknown	2012-09-07
\| * \| \|	Implement support for alternative SMT solvers -- CVC3 and CVC4	Peter Collingbourne	2012-09-06
\| * \| \|	Dafny: Fixed a test that would fail with Z3 4.1.	wuestholz	2012-09-07
\| \| \| *	Chalice: implemented "inside" information for all cases which translate to st...	Unknown	2012-09-06
\| \| \| *	Chalice: added "inside" knowledge of predicate instance nesting to unfold sta...	Unknown	2012-09-06
\| \| \| *	Chalice: first part of implementation of tracking which predicate instances o...	Unknown	2012-09-06
* \| \| \|	Merge	Unknown	2012-09-05
\|\\| \| \|
* \| \| \|	Dafny: fixed typo in latex mode	Unknown	2012-09-05
\| \| \| *	Chalice: Merge	Unknown	2012-09-05
\| \| \| \|\
\| \| \| * \|	Chalice: support for static functions. Functions declared "static" are axioma...	Unknown	2012-09-05
\| \| \| \| *	Chalice: Remove accidental changes to chalice.bat.	stefanheule	2012-09-05
\| \| \| \|/
\| \| \| *	Chalice: adopted triggering/axioms used for "recursive" functions for all fun...	Unknown	2012-09-04
\| \| \| *	Chalice: reapplied changes from changeset	Unknown	2012-09-03
\| \| \| *	reapplied changes from changeset:	Unknown	2012-09-03
\| \| \| *	Chalice: added list segment example	Unknown	2012-09-03
\| \| \| *	Chalice: reremoved implementation of (unuses) UpdateSecMask, as was previousl...	Unknown	2012-09-03
\| \| \| *	Chalice: reapplied changes from changeset	Unknown	2012-09-03
\| \| \| *	Reapplied changes from previous update	Unknown	2012-09-03
\| \| \| *	Reverted Prelude.scala and Translator.scala to those from version 96adb1c351bd	Unknown	2012-09-03
\| * \| \|	Moved point at which preprocessed output is shown.	Unknown	2012-08-31
\| * \| \|	Shared state is now properly abstracted in requires clauses.	Unknown	2012-08-31
* \| \| \|	DafnyExtension: don't duplicate names of inherited identifiers	Unknown	2012-08-30
* \| \| \|	Dafny: for refinements, don't consider a newly provided predicate body to be ...	Unknown	2012-08-30
* \| \| \|	DafnyExtension: changed how "_" is displayed (now display as a keyword, not a...	Unknown	2012-08-30
* \| \| \|	Dafny: allow "_" as don't-care variable name	Unknown	2012-08-30
\| \| * \|	Dafny: allow more corecursive calls for copredicates	Rustan Leino	2012-08-30
\| \|/ / \|/\| \|
\| * \|	Merge	Unknown	2012-08-30
\| \|\ \ \| \|/ / \|/\| \|
\| * \|	Barriers now handled uniformly via bugle_barrier.	Unknown	2012-08-30
* \| \|	Dafny: fixed bug in checking postconditions of functions that mention the res...	Unknown	2012-08-29
* \| \|	DafnyExtension: fixed bug (omitted case: VarDeclStmt has no Update component)	Unknown	2012-08-29
* \| \|	Dafny: fixed contract violation in parser (for non-parsing Lhs production)	Unknown	2012-08-29
\|/ /
* \|	A small fix in variable definition analysis.	Unknown	2012-08-29
* \|	Added generation of invariants to restrict source location to sensible values.	Egor Kyshtymov	2012-08-28
* \|	DafnyExtension: don't reverify a buffer with no changes	Rustan Leino	2012-08-27