debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	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
\|
*	Added lemmas that make verification go through faster and more reliably	leino	2015-01-05
\|
*	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
\| \|
* \|	Finished up refactoring of the new name segment parsing, AST, and resolution.	leino	2014-12-07
\| \| \| \| \| \| \| \|	Removed now defunct IdentifierSequence from the AST.
\| *	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
\|
*	Use arbitrary lookahead to determine if the next expression is a lambda ↵	leino	2014-11-13
\| \| \| \|	expression.
*	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
\| *	Extracted a separate class to generate fresh variable names.	wuestholz	2014-11-06
\| \|
\| *	Updated test.	chmaria	2014-11-06
\| \|
\| *	Added computation of free variables in dirty while statements.	chmaria	2014-11-06
\|/
*	Merge	Rustan Leino	2014-11-05
\|\
* \|	Temporarily disabled one of the methods in NumberRepresentations.dfy -- this ↵	leino	2014-11-05
\| \| \| \| \| \| \| \|	needs to be addressed in some way that will produce stable verification results
* \|	Merge	leino	2014-11-04
\|\ \
* \ \	Merge	leino	2014-11-04
\|\ \ \
* \| \| \|	Refactored SnapshotableTrees a bit and made it verify in a reasonable amount ↵	leino	2014-11-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of time :)
\| \| * \|	Made dirty statements ghost.	chmaria	2014-11-04
\| \| \| \|
\| \| \| *	Merge	Rustan Leino	2014-11-03
\| \| \| \|\ \| \| \| \|/ \| \| \|/\|
\| \| \| *	Updated a test case for new syntax and convensions	Rustan Leino	2014-11-03
\| \| \| \|
\| \| * \|	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
\| \|\\| \|
\| \| * \|	Minor fix in test dafny2/SnapshotableTrees.dfy.	chmaria	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.