debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Added initial support for dirty while statements.	chmaria	2014-11-01
\|
*	Allow assignment LHSs in a forall statement to be the same, so long as the ↵	leino	2014-10-30
\| \| \| \| \| \|	they are assigned the same RHS value. Don't include havoc assignments in LHS-duplicate checks.
*	Resolve attributes of a forall statement only after bound variables have ↵	leino	2014-10-29
\| \| \| \| \| \| \|	been added to the scope. Resolve the attributes of local variables. Don't resolve attributes of PredicateStmt's more than once.
*	Fix bug in translation of 'new' for arrays	Rustan Leino	2014-10-29
\|
*	Merge	leino	2014-10-28
\|\
* \|	Fixed type-inference bug that could create cycles in proxy type graph	leino	2014-10-28
\| \|
* \|	Disallow automatic completion of type arguments to the LHS of datatype ↵	leino	2014-10-28
\| \| \| \| \| \| \| \|	declarations
\| *	Create large stack in DafnyDriver.cs, before calling main,	Bryan Parno	2014-10-28
\|/ \| \| \|	just in case Boogie needs more room
*	Fixed a bug in the Substituter for datatype update expressions.	leino	2014-10-28
\|
*	Add a DafnyCC option that disables some of Dafny's cleverness to better ↵	Bryan Parno	2014-10-27
\| \| \| \|	match DafnyCC's capabilities
*	Fix datatype updates so chained updates don't explode performance	Bryan Parno	2014-10-27
\|
*	Make autoreqs of free requires not free	Bryan Parno	2014-10-27
\|
*	Allow autoReq in methods to generate auto-requirements on requires	Bryan Parno	2014-10-27
\|
*	Fixed range bug that was causing extension to sometimes crash	Bryan Parno	2014-10-27
\|
*	Don't process opaque functions more than once when generating auto-reqs	Bryan Parno	2014-10-27
\|
*	Fix fixup to opaque-function revealer to deal with zero-argument lemmas	Bryan Parno	2014-10-27
\|
*	Fix autoreq handling of quantifiers	Bryan Parno	2014-10-27
\|
*	Ensure that no file is processed twice, even if one command-line file is ↵	Bryan Parno	2014-10-27
\| \| \| \|	included by another command-line file.
*	Added an attribute :timeLimitMultiplier for setting relative time outs.	Bryan Parno	2014-10-27
\|
*	Push the translation of user-supplied triggers deeper	Bryan Parno	2014-10-27
\|
*	Add support for counting spec/impl/proof lines by supressing, e.g., ghost ↵	Bryan Parno	2014-10-27
\| \| \| \|	statements
*	Add an option to allow automatically generated requirements to be printed	Bryan Parno	2014-10-27
\| \| \| \|	to a file, making them easier to inspect and manipulate.
*	Even with noCheating enabled, don't check included files or methods marked ↵	Bryan Parno	2014-10-27
\| \| \| \|	with :decl or :imported
*	Allow non-ghost axioms in order to model trusted external calls,	Bryan Parno	2014-10-27
\| \| \| \| \|	e.g., Ironclad's calls to assembly instructions. Also fixed what appeared to be a bug in the Makefile for invoking Coco
*	Merge	leino	2014-10-25
\|\
* \|	Marked "free" as soon-to-be-deprecated	leino	2014-10-25
\| \|
* \|	Made semi-colons are specification clauses optional. In a future version, ↵	leino	2014-10-25
\| \| \| \| \| \| \| \|	they will no longer be allowed.
\| *	Add an option to use reduce Z3's knowledge of non-linear arithmetic.	Bryan Parno	2014-10-24
\|/ \| \| \|	Results in more manual work, but it also produces more predictable behavior.
*	Allow underscores in numeric literals (and in field/destructor names that ↵	leino	2014-10-23
\| \| \| \| \| \|	are written as numeric strings). The underscores have no semantic meaning, but can help a human parse the numbers.
*	Changed version to 1.9.1.11022	leino	2014-10-21
\|
*	When guessing decreases clauses for loops, convert numeric values to their ↵	leino	2014-10-21
\| \| \| \|	ultimate base type (int or real) before subtracting
*	Fixed crash in inferred descreases clauses involving newtypes.	leino	2014-10-21
\| \| \| \|	Added BinarySearch as a test case.
*	Changed version to 1.9.1.11021	leino	2014-10-21
\| \| \| \|	Also include ModelViewer.dll in binary distribution
*	Comparisons and well-founded order of char	leino	2014-10-21
\|
*	Add char literals.	leino	2014-10-20
\| \| \| \|	Disallow backslash from being part of identifier names.
*	Merge	leino	2014-10-20
\|\
* \|	Added types "char" and "string" (the latter being a synonym for "seq<char>").	leino	2014-10-20
\| \| \| \| \| \| \| \| \| \| \| \|	Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes.
\| *	DafnyExtension: Fixed minor issue in the menu.	wuestholz	2014-10-19
\|/
*	Updated version to 1.9.0.11016. This version is going on rise4fun.com.	leino	2014-10-16
\|
*	Merge	leino	2014-10-14
\|\
\| *	Minor change	wuestholz	2014-10-14
\| \|
* \|	Fixed parsing crash on malformed chaining with == and !!	leino	2014-10-09
\| \|
* \|	Print arrow types with parentheses around the domain type when the domain ↵	leino	2014-10-09
\| \| \| \| \| \| \| \|	consists of one tuple type.
* \|	Stricter rules about that types need to be completely resolved.	leino	2014-10-08
\|/ \| \| \| \| \|	Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it). If the type of literal "null" is unresolved, make the type "object". The need to translate unresolved proxies is now assumed to be gone.
*	Allow any integer-based type, not just 'int', in the following places:	leino	2014-10-06
\| \| \| \| \| \| \| \| \| \|	* array indices (any dimension) * array lengths (with new, any dimension) * sequence indicies * subsequence bounds (like sq[lo..hi]) * the new multiplicity in multiset update (m[t := multiplicity]) * subarray-to-sequence bounds (like a[lo..hi]) Note that for an array 'a', 'a.Length' is always an integer, so a comparison 'i < a.Length' still requires 'i' to be an integer, not any integer-based value. Same for '\|sq\|' for a sequence 'sq'.
*	Merge	leino	2014-09-29
\|\
* \|	Shorter wait-for-idle time in the Dafny IDE	leino	2014-09-29
\| \|
\| *	DafnyExtension: Made it not log the pretty-printed program.	wuestholz	2014-09-28
\| \|
\| *	DafnyExtension: minor change due to change in Boogie	wuestholz	2014-09-28
\| \|
\| *	Did more refactoring.	wuestholz	2014-09-23
\| \|