debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Members included from different files are now internally marked with an ↵	Rustan Leino	2014-04-19
\| \| \| \| \| \| \|	IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features. Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines). Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked.
*	Fixed bug #32 dafny.codeplex.com.	Rustan Leino	2014-04-15
\|
*	Compile reals	Rustan Leino	2014-04-13
\|
*	Allow reals in decreases clauses	Rustan Leino	2014-04-08
\|
*	Merge	Rustan Leino	2014-04-04
\|\
* \|	Fixed refinement of modify statements	Rustan Leino	2014-04-04
\| \|
\| *	Partial support for slicing a sequence using lengths, rather than indices.	Bryan Parno	2014-04-04
\|/ \| \| \|	Will get cleaner once we have tuple support.
*	Merge	Rustan Leino	2014-04-04
\|\
* \|	Also include lower set bounds (bounding a set from below) in witness guesses ↵	Rustan Leino	2014-04-04
\| \| \| \| \| \| \| \|	for assign/let such-that.
* \|	Support the transition from "modify Frame;" to "modify Frame { Body }" by ↵	Rustan Leino	2014-04-04
\| \| \| \| \| \| \| \|	refinement.
* \|	Changed an error from a verification error to a syntactic (resolution) error	Rustan Leino	2014-04-04
\| \|
* \|	Added "modify Frame { Body }" statement.	Rustan Leino	2014-04-04
\| \|
* \|	Added "modify" statement.	Rustan Leino	2014-04-03
\| \| \| \| \| \| \| \|	In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
\| *	Basic support for datatype-update syntatic sugar	Bryan Parno	2014-04-03
\|/
*	Merge	Rustan Leino	2014-03-24
\|\
* \|	Reduced noise in BVD display of temporary variables of the translation	Rustan Leino	2014-03-24
\| \|
\| *	Auto-set type arguments of built-in collection types, just like for ↵	Rustan Leino	2014-03-21
\|/ \| \| \|	user-defined types.
*	Fixed problem with propagating allocation information about array elements.	Rustan Leino	2014-03-20
\| \| \| \|	Improved situation with (reducing bogosity of) type checking of "object".
*	Propagate literals through equality operations.	Nada Amin	2014-03-19
\|
*	Merge	Rustan Leino	2014-03-17
\|\
* \|	Fixed resolution bug where "var x := x" was allowed.	Rustan Leino	2014-03-17
\| \|
* \|	Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵	Rustan Leino	2014-03-17
\| \| \| \| \| \| \| \|	to VarDeclStmt.Locals
* \|	AST refactoring:	Rustan Leino	2014-03-17
\| \| \| \| \| \| \| \| \| \|	Changed VarDecl to no longer inherit from Statement. Removed ConcreteSyntaxStatement and changed VarDeclStmt's superclass be Statement.
\| *	Improve computations, in particular compositionality. Isolated useless ↵	Nada Amin	2014-03-12
\| \| \| \| \| \| \| \|	literals around if-then-else as a surprising source of practical hanging.
\| *	change computation weight to 3. Tests still pass.	Nada Amin	2014-03-11
\|/
*	Added further assistance in coming up with decreases clauses in SCCs with ↵	Rustan Leino	2014-02-24
\| \| \| \|	co-recursive calls.
*	Unfinished code -- please forgive (I'm switching machines and will fix shortly)	Rustan Leino	2014-02-24
\|
*	Refactored code for dealing with SCCs in the call graph.	Rustan Leino	2014-02-24
\| \| \| \|	Fixed bug.
*	Fixed bugs in co-call checks	Rustan Leino	2014-02-23
\|
*	Fixed some checking of recursive method/copredicate calls	Rustan Leino	2014-02-23
\|
*	Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵	Rustan Leino	2014-02-23
\| \| \| \|	-> "prefix lemma")
*	Allow unary minus on reals	Rustan Leino	2014-02-13
\|
*	Fixed crash in parser	Rustan Leino	2014-02-13
\|
*	Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for ↵	Rustan Leino	2014-02-13
\| \| \| \| \| \|	literals. Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations).
*	Preliminary support for reals in Dafny specs. No compiler suport yet.	Bryan Parno	2014-02-10
\|
*	Fixed bug in DafnyExtension (hover text computation would crash if ↵	Rustan Leino	2014-02-06
\| \| \| \| \| \|	Translator had not been run). Fixed duplicate hover text information for Lines of calc statements.
*	Removed some blank lines at the end of hover texts.	Rustan Leino	2014-02-06
\|
*	Merge	Rustan Leino	2014-02-04
\|\
* \|	Mark auto-generated expressions (in "decreases" clauses) and don't use these ↵	Rustan Leino	2014-02-04
\| \| \| \| \| \| \| \|	when figuring out hover text.
\| *	Provide more detailed feedback for errors involving if-then-else	Bryan Parno	2014-02-03
\|/
*	Fixed bug that misclassified a ghost statement	Rustan Leino	2014-01-31
\|
*	Compile to .exe only if the Main method has no user-defined preconditions.	Rustan Leino	2014-01-31
\| \| \| \|	If Main is already declared as static, don't produce a second static Main.
*	Produce hover text for many of the refinement omissions (i.e., "..." and the ↵	Rustan Leino	2014-01-31
\| \| \| \|	like).
*	Fix a bug in the interaction between opaque and generics	Bryan Parno	2014-01-23
\|
*	Fix minor issue in compilation of main methods.	wuestholz	2014-01-17
\|
*	Merge	Rustan Leino	2014-01-14
\|\
* \|	Improve error information by generating "Related location" information that ↵	Rustan Leino	2014-01-14
\| \| \| \| \| \| \| \|	traces into preconditions of called functions
\| *	Added a missing autoReq resolution step	Bryan Parno	2014-01-14
\| \|
\| *	Merge	Bryan Parno	2014-01-13
\| \|\ \| \|/ \|/\|
\| *	Improve autoReq's interactions with opaque	Bryan Parno	2014-01-13
\| \|