debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Make syntax of "match" expressions and "match" statements the same -- curly ↵	Rustan Leino	2014-06-24
\| \| \| \|	braces around the cases are now supported for both and are optional for both
*	Merge	Rustan Leino	2014-06-24
\|\
* \|	Added some axioms about seq-to-multiset conversions	Rustan Leino	2014-06-24
\| \|
* \|	Invert LHS sub-expressions in forall assignment statements, which gives the ↵	Rustan Leino	2014-06-24
\| \| \| \| \| \| \| \|	opportunity to designate a good trigger.
\| *	DafnyExtension: Made it possible to activate the more advanced verification ↵	wuestholz	2014-06-23
\| \| \| \| \| \| \| \|	result caching in Boogie (experimental for now).
\| *	DafnyExtension: Minor change to deal with a change in the Boogie ↵	wuestholz	2014-06-20
\|/ \| \| \|	command-line options
*	Specialized Lit function for int and real (leaving all other cases ↵	Rustan Leino	2014-06-10
\| \| \| \| \| \|	polymorphic). This reduces the number of int<->U conversions that Boogie adds, which avoids a looping problem in Z3. (Regrettably, the test suite seems to have become rather unstable. Sometimes everything verifies and sometimes there is some looping forever.)
*	Made the snapshotable trees test "unsupported" instead of "unresolved".	wuestholz	2014-06-05
\|
*	Improved axiom that knows that array-to-sequence converstion depends only on ↵	Rustan Leino	2014-06-04
\| \| \| \|	those heap location that hold the array elements
*	Fixed issues with absolute file names in the expected output for the lit tests.	wuestholz	2014-06-04
\|
*	Added support for 'dirty' forall statements.	chmaria	2014-06-03
\| \| \| \| \| \| \| \| \| \| \|	One can now write forall statements without bodies (but with ensures clauses) as follows: forall s \| s in S ensures s < 0; where S is set<int>. The ensures clauses are assumed but not checked.
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Fixed bug in resolution, where type proxies involved in equality tests did ↵	Rustan Leino	2014-05-07
\| \| \| \| \| \|	not get assigned. (Issue #35) Fixed Main detection--a method "Main" with type parameters cannot be a program entry point.
*	Fixed some bugs where various attributes were not properly visited during ↵	Rustan Leino	2014-05-05
\| \| \| \|	type checking.
*	DafnyExtension: Made it display the compilation output in the VS output pane.	wuestholz	2014-04-21
\|
*	Add support for assumption variables.	wuestholz	2014-04-21
\|
*	DafnyExtension: Added some support for logging program snapshots that are ↵	wuestholz	2014-04-21
\| \| \| \|	sent to the verifier.
*	Fixed bug #33.	Rustan Leino	2014-04-19
\|
*	Version 1.8.2.10419, binary release and (except for the "include" update in ↵	Rustan Leino	2014-04-19
\| \| \| \|	the previous check-in) rise4fun
*	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
\|
*	Cleaned up some no longer needed parentheses in test file	Rustan Leino	2014-04-15
\|
*	Run-time real support	Rustan Leino	2014-04-13
\|
*	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.
*	Adjusted merge	Rustan Leino	2014-04-04
\|
*	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
\|/
*	DafnyExtension: Fixed a concurrency issue.	wuestholz	2014-04-03
\|
*	Improvements in sequence axioms to make checking more automatic.	Rustan Leino	2014-04-02
\| \| \| \|	Minor changes in a test file.
*	Bumped version to 1.8.1.10324. To go onto rise4fun and as a binary drop.	Rustan Leino	2014-03-24
\|
*	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 typo in latex style file	Rustan Leino	2014-03-20
\|/
*	Added axiom to transfer array element-type information onto the elements ↵	Rustan Leino	2014-03-20
\| \| \| \| \| \|	themselves. Other serendipitous axiom improvements.
*	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.