debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	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
\| \|
* \|	Merge	Rustan Leino	2014-01-13
\|\\|
* \|	Added /compile:3, which compiles in memory and then executes the program (if ↵	Rustan Leino	2014-01-13
\| \| \| \| \| \| \| \|	there is a Main and there are no errors). Primarily intended for use with rise4fun.
\| *	Small fix to the order in which AutoReq adds its requirements.	Bryan Parno	2014-01-13
\|/
*	Fixed spurious complaint about assignment to non-ghost variable	Rustan Leino	2014-01-11
\|
*	A better fix to deal with StaticReceiverTypes affected by autoReq.	Bryan Parno	2014-01-10
\|
*	Fixed a resolve bug for UserDefinedTypes	Bryan Parno	2014-01-09
\|
*	Manually adjusted merge	Rustan Leino	2014-01-08
\|
*	Merge	Rustan Leino	2014-01-08
\|\
* \|	Allow left-hand sides of a let expression to be patterns (like in the case ↵	Rustan Leino	2014-01-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	of a match expression). Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator. Fixed compilation of match expressions, to allow them anywhere.
\| *	Fixed build break: two contract problems	Rustan Leino	2014-01-08
\| \|
\| *	:autoReq now works with static functions.	Bryan Parno	2014-01-08
\| \| \| \| \| \| \| \|	This required fixing a small bug in how StaticReceiverExpr's were being handled
\| *	Add autoReq support for matches.	Bryan Parno	2014-01-08
\| \| \| \| \| \| \| \|	Add better handling of resolved data types in autoReq.
\| *	Added support for automatic generation of function requirements via the ↵	Bryan Parno	2014-01-08
\| \| \| \| \| \| \| \|	:autoReq attribute.
\| *	Don't produce default decreases clause for co-predicates, since ↵	Rustan Leino	2014-01-07
\| \| \| \| \| \| \| \|	co-predicates don't have decreases clauses
\| *	Compile assign-such-that for all integers, not just ones where a bound is found	Rustan Leino	2014-01-06
\|/
*	More thoroughly check for nested assume statements during compilation	Rustan Leino	2014-01-05
\|
*	Added ghost let expressions.	Rustan Leino	2014-01-05
\|
*	Improved the name-clashing situation when substituting to produce printable ↵	Rustan Leino	2014-01-03
\| \| \| \|	AdditionalInformation for forall-statement ensures clauses.
*	Merge	Rustan Leino	2014-01-03
\|\
\| *	Make ModuleDefinition inherit from TopLevelDecl instead of just Declaration	Bryan Parno	2014-01-03
\| \|
* \|	Allow "match" expressions anywhere	Rustan Leino	2014-01-03
\| \|
* \|	No longer specialize axioms Haskell-style for functions whose bodies ↵	Rustan Leino	2014-01-03
\| \| \| \| \| \| \| \|	contains "match" expressions.
* \|	Print and translate "match" expressions in general positions, not just at ↵	Rustan Leino	2014-01-03
\|/ \| \| \|	the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.)
*	Hover text for inferred postconditions of 'forall' statements (the one for ↵	Rustan Leino	2013-12-30
\| \| \| \|	calls leaves something to be desired)
*	Merge	Rustan Leino	2013-12-30
\|\
* \|	Added proper parsing for StmtExpr's in all contexts.	Rustan Leino	2013-12-30
\| \| \| \| \| \| \| \| \| \| \| \|	Adjusted printer accordingly. Fixed bug in Substituter for CalcStmt in StmtExpr's. Always show terminating semi-colon in hover-text for default decreases clauses.
\| *	Pass on attributes for methods, iterators, and functions to Boogie.	wuestholz	2013-12-26
\| \|