summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
Commit message (Expand)AuthorAge
* New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
* Add support for assumption variables.Gravatar wuestholz2014-04-21
* Members included from different files are now internally marked with an Inclu...Gravatar Rustan Leino2014-04-19
* Allow reals in decreases clausesGravatar Rustan Leino2014-04-08
* MergeGravatar Rustan Leino2014-04-04
|\
* | Also include lower set bounds (bounding a set from below) in witness guesses ...Gravatar Rustan Leino2014-04-04
* | Changed an error from a verification error to a syntactic (resolution) errorGravatar Rustan Leino2014-04-04
* | Added "modify Frame { Body }" statement.Gravatar Rustan Leino2014-04-04
* | Added "modify" statement.Gravatar Rustan Leino2014-04-03
| * Basic support for datatype-update syntatic sugarGravatar Bryan Parno2014-04-03
|/
* Reduced noise in BVD display of temporary variables of the translationGravatar Rustan Leino2014-03-24
* Propagate literals through equality operations.Gravatar Nada Amin2014-03-19
* MergeGravatar Rustan Leino2014-03-17
|\
* | Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss t...Gravatar Rustan Leino2014-03-17
* | AST refactoring:Gravatar Rustan Leino2014-03-17
| * Improve computations, in particular compositionality. Isolated useless litera...Gravatar Nada Amin2014-03-12
| * change computation weight to 3. Tests still pass.Gravatar Nada Amin2014-03-11
|/
* Refactored code for dealing with SCCs in the call graph.Gravatar Rustan Leino2014-02-24
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...Gravatar Rustan Leino2014-02-23
* Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for lite...Gravatar Rustan Leino2014-02-13
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
* Provide more detailed feedback for errors involving if-then-elseGravatar Bryan Parno2014-02-03
* Improve error information by generating "Related location" information that t...Gravatar Rustan Leino2014-01-14
* MergeGravatar Rustan Leino2014-01-08
|\
* | Allow left-hand sides of a let expression to be patterns (like in the case of...Gravatar Rustan Leino2014-01-08
| * Added support for automatic generation of function requirements via the :auto...Gravatar Bryan Parno2014-01-08
|/
* Improved the name-clashing situation when substituting to produce printable A...Gravatar Rustan Leino2014-01-03
* No longer specialize axioms Haskell-style for functions whose bodies contains...Gravatar Rustan Leino2014-01-03
* Print and translate "match" expressions in general positions, not just at the...Gravatar Rustan Leino2014-01-03
* MergeGravatar Rustan Leino2013-12-30
|\
* | Added proper parsing for StmtExpr's in all contexts.Gravatar Rustan Leino2013-12-30
| * Pass on attributes for methods, iterators, and functions to Boogie.Gravatar wuestholz2013-12-26
|/
* Hover text for default decreases clauses of loops.Gravatar Rustan Leino2013-12-20
* MergeGravatar Rustan Leino2013-12-19
|\
* | Added an .EndTok for every statement. (Note, in some places, especially in V...Gravatar Rustan Leino2013-12-19
| * Compute default decreases clauses in Resolver instead of in the Translator.Gravatar Rustan Leino2013-12-19
|/
* MergeGravatar Rustan Leino2013-12-17
|\
* | Don't inline opaque functions.Gravatar Rustan Leino2013-12-17
| * MergeGravatar Rustan Leino2013-12-16
| |\ | |/ |/|
| * Fixed bug where free conditions preceded checked conditions (for inlined pred...Gravatar Rustan Leino2013-12-16
* | Pass assert/assume attributes down to BoogieGravatar Rustan Leino2013-12-16
* | Fix build failure due to changes in Boogie.Gravatar wuestholz2013-12-16
* | Add support for the :axiom attribute for ghost methods.Gravatar Bryan Parno2013-12-13
* | Added support for opaque function definitions, indicated via the {:opaque} at...Gravatar Bryan Parno2013-12-13
* | Fixed a bug in the Boogie generated for refinement checks (now that there is ...Gravatar Rustan Leino2013-12-09
|/
* Added support for attributes on variable declarations.Gravatar wuestholz2013-11-18
* Removed code for an unreachable caseGravatar Rustan Leino2013-08-06
* Merged PredicateExpr and CalcExpr into a single StmtExprGravatar Rustan Leino2013-08-06
* Unified function/method context heightsGravatar Rustan Leino2013-08-04
* Set up call-graph to keep track of edges between functions and methods. (To ...Gravatar Rustan Leino2013-08-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 04:46:03 +0000