debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Allow let-such-that expression to be compiled, provided that they provably ↵	leino	2015-03-13
\| \| \| \|	have a unique value
*	Fixed bug in resolution of illegal programs.	leino	2015-03-10
\| \| \| \|	Fixed comments in some test cases.
*	This changeset changes the default visibility of a function/predicate body ↵	leino	2015-03-09
\| \| \| \| \| \| \| \| \| \|	outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'. Semantics of 'protected': * The definition (i.e., body) of a 'protected' function is not visible outside the defining module * The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions. * In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected' * The 'protected' status of a function must be preserved in refinement modules
*	Added 'protected' keyword (syntax)	leino	2015-03-07
\|
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	Add imap display/update expressions	chrishaw	2015-02-27
\|
*	Add imap type, which is like map but may have have infinite size	chrishaw	2015-02-26
\|
*	Generate unique IDs hierarchically, to reduce changes to IDs when the ↵	leino	2015-01-28
\| \| \| \|	program is modified (to help with fine-grained caching)
*	Did some refactoring to improve the name generation.	wuestholz	2015-01-27
\|
*	Did some refactoring to improve the name generation.	wuestholz	2015-01-27
\|
*	Assume type properties of values that are created by a havoc assignment. ↵	Rustan Leino	2015-01-27
\| \| \| \| \| \|	Such assignments are part of assign-such-that statements, and thus this also fixes Issue 52.
*	Fixed an encoding bug for newtypes (this fixes Issue #50)	Rustan Leino	2015-01-27
\|
*	Minor change to a test case	wuestholz	2015-01-27
\|
*	Updated test output after change in Boogie.	wuestholz	2015-01-24
\|
*	Make sure to check that subrange types are not used as type parameters	leino	2015-01-23
\|
*	Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, ↵	leino	2015-01-23
\| \| \| \| \| \| \|	so use the new name resolution machinery that handles modules and type parameters Included some inadvertently left-out test cases in dafny0/Modules0.dfy Fixed comparable-types tests
*	When ambiguous references all resolve to the same declaration, don't complain	leino	2015-01-09
\|
*	Fixed bug in opaque functions with type parameters	leino	2015-01-07
\|
*	Merge	leino	2015-01-03
\|\
* \|	Fixed resolution of method calls with explicit type parameters.	leino	2015-01-02
\| \| \| \| \| \| \| \|	Finished refactoring of the recent name segments changes.
\| *	Updated test output after change in Boogie.	wuestholz	2014-12-28
\| \|
* \|	Language change: All functions and methods declared lexically outside any ↵	leino	2014-12-12
\|/ \| \| \| \| \| \| \| \| \|	class are now automatically static, and fields are no longer allowed to be declared there. Stated differently, all heap state must now be declared inside an explicitly declared class, and functions and methods declared outside any class can be viewed as belonging to the module. The motivating benefit of this change is to no longer need the 'static' keyword when declaring a module of functions and methods.
*	Fixed two crashes in resolver	leino	2014-12-10
\| \| \| \|	Corrected merge
*	Merge	leino	2014-12-09
\|\
* \|	Allow user-specified type parameters	leino	2014-12-09
\| \|
\| *	minor change on a test.	Reza Ahmadi	2014-12-03
\| \|
\| *	added multiple trait inheritance.	Reza Ahmadi	2014-12-03
\| \| \| \| \| \| \| \|	- a class can now extend more than one traits
* \|	Fixed some issues with assignments in refinements, both soundness bugs in ↵	leino	2014-12-02
\| \| \| \| \| \| \| \|	previous version and changes necessitated by recent parsing refactoring
* \|	Snapshot, to be continued	leino	2014-12-02
\| \|
\| *	removing one unnessessary check in the cloner	Reza Ahmadi	2014-12-02
\| \|
\| *	- fixed a bug in merging fields that come from a parent trait	Reza Ahmadi	2014-12-02
\| \| \| \| \| \| \| \|	- added one more test
\| *	Updated test output after change in Boogie.	wuestholz	2014-11-25
\|/
*	Merge	leino	2014-11-19
\|\
* \|	Fixed bug where resolution was overly restrictive with ghost variables ↵	leino	2014-11-19
\| \| \| \| \| \| \| \| \| \| \| \|	appearing in reads clauses. Fixed bug in the checking of reads subset for field frame targets ("back ticks")
\| *	Updated test output after change in Boogie.	wuestholz	2014-11-16
\|/
*	Bug fixes in the compilation of forall statements.	leino	2014-11-13
\|
*	Merge	leino	2014-11-06
\|\
* \|	Started fixing a number of LL(1) warnings	leino	2014-11-06
\| \| \| \| \| \| \| \| \| \|	Disallow empty modifies/reads clauses (this eliminates some LL(1) warnings) Require modify statement to take a nonempty list of frame expressions
\| *	Updated test.	chmaria	2014-11-06
\| \|
\| *	Added computation of free variables in dirty while statements.	chmaria	2014-11-06
\|/
*	Merge	leino	2014-11-04
\|\
\| *	Made dirty statements ghost.	chmaria	2014-11-04
\| \|
\| *	Fixed test output after refactoring in Boogie.	wuestholz	2014-11-03
\| \|
\| *	Fixed test output after refactoring in Boogie.	wuestholz	2014-11-02
\| \|
* \|	Merge	leino	2014-11-01
\|\\|
\| *	Added initial support for dirty while statements.	chmaria	2014-11-01
\| \|
* \|	Improved power of axioms Seq#FromArray	leino	2014-10-31
\|/
*	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
\|