summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Version 1.8.0.10115 release candidateGravatar Rustan Leino2014-01-15
|
* MergeGravatar Rustan Leino2014-01-14
|\
* | Improve error information by generating "Related location" information that ↵Gravatar Rustan Leino2014-01-14
| | | | | | | | traces into preconditions of called functions
| * Added a missing autoReq resolution stepGravatar Bryan Parno2014-01-14
| |
| * MergeGravatar Bryan Parno2014-01-13
| |\ | |/ |/|
| * Improve autoReq's interactions with opaqueGravatar Bryan Parno2014-01-13
| |
* | Supply C# compiler switch /nowarn:0219, which suppresses any warning CS0219 ↵Gravatar Rustan Leino2014-01-13
| | | | | | | | about variables not being used.
* | MergeGravatar Rustan Leino2014-01-13
|\|
* | Added /compile:3, which compiles in memory and then executes the program (if ↵Gravatar Rustan Leino2014-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.Gravatar Bryan Parno2014-01-13
|/
* Proof that there is no bound on the size of prime numbersGravatar Rustan Leino2014-01-11
|
* Fixed spurious complaint about assignment to non-ghost variableGravatar Rustan Leino2014-01-11
|
* MergeGravatar Rustan Leino2014-01-11
|\
| * A better fix to deal with StaticReceiverTypes affected by autoReq.Gravatar Bryan Parno2014-01-10
| |
* | MergeGravatar Rustan Leino2014-01-10
|\|
* | GHC-MergeSort: removed lemmas and proof steps rendered unnecessary now that ↵Gravatar Rustan Leino2014-01-09
| | | | | | | | axioms for functions with match'es are no longer specialized
| * MergeGravatar Bryan Parno2014-01-09
| |\ | |/ |/|
| * Fixed a resolve bug for UserDefinedTypesGravatar Bryan Parno2014-01-09
| |
* | Dafny renditions of sorting algorithms proved in other provers (Coq, ↵Gravatar Rustan Leino2014-01-08
|/ | | | Isabelle, F*)
* Manually adjusted mergeGravatar Rustan Leino2014-01-08
|
* MergeGravatar Rustan Leino2014-01-08
|\
* | Allow left-hand sides of a let expression to be patterns (like in the case ↵Gravatar Rustan Leino2014-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 problemsGravatar Rustan Leino2014-01-08
| |
| * :autoReq now works with static functions.Gravatar Bryan Parno2014-01-08
| | | | | | | | This required fixing a small bug in how StaticReceiverExpr's were being handled
| * Add autoReq support for matches.Gravatar Bryan Parno2014-01-08
| | | | | | | | Add better handling of resolved data types in autoReq.
| * Added support for automatic generation of function requirements via the ↵Gravatar Bryan Parno2014-01-08
| | | | | | | | :autoReq attribute.
| * Don't produce default decreases clause for co-predicates, since ↵Gravatar Rustan Leino2014-01-07
| | | | | | | | co-predicates don't have decreases clauses
| * One more file to go with the previous check-in (DafnyRuntime.cs apparently ↵Gravatar Rustan Leino2014-01-06
| | | | | | | | gets copied)
| * Compile assign-such-that for all integers, not just ones where a bound is foundGravatar Rustan Leino2014-01-06
|/
* More thoroughly check for nested assume statements during compilationGravatar Rustan Leino2014-01-05
|
* Added ghost let expressions.Gravatar Rustan Leino2014-01-05
|
* Renamed a constructor in a test fileGravatar Rustan Leino2014-01-03
|
* Improved the name-clashing situation when substituting to produce printable ↵Gravatar Rustan Leino2014-01-03
| | | | AdditionalInformation for forall-statement ensures clauses.
* Removed unused declarationGravatar Rustan Leino2014-01-03
|
* MergeGravatar Rustan Leino2014-01-03
|\
* | Changed BreadthFirstSearch example to no longer use "inductive naturals", ↵Gravatar Rustan Leino2014-01-03
| | | | | | | | | | | | sequences, or roll-it-yourself maps. Instead, use "nat", List, and "map". Use VC splitting to combat performance issues.
| * Make ModuleDefinition inherit from TopLevelDecl instead of just DeclarationGravatar Bryan Parno2014-01-03
| |
* | Allow "match" expressions anywhereGravatar Rustan Leino2014-01-03
| |
* | No longer specialize axioms Haskell-style for functions whose bodies ↵Gravatar Rustan Leino2014-01-03
| | | | | | | | contains "match" expressions.
* | Print and translate "match" expressions in general positions, not just at ↵Gravatar Rustan Leino2014-01-03
| | | | | | | | the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.)
* | Embellished axioms about GenericAlloc and DtAlloc.Gravatar Rustan Leino2014-01-03
|/
* Hover text for inferred postconditions of 'forall' statements (the one for ↵Gravatar Rustan Leino2013-12-30
| | | | calls leaves something to be desired)
* MergeGravatar Rustan Leino2013-12-30
|\
* | Added proper parsing for StmtExpr's in all contexts.Gravatar Rustan Leino2013-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.Gravatar wuestholz2013-12-26
| |
| * DafnyExtension: Reduce the default number of Z3 instances by one.Gravatar wuestholz2013-12-26
| |
| * Changed the iterator class hover text back to the iterator name (which is ↵Gravatar Rustan Leino2013-12-20
|/ | | | consistent with everything else), not the "iterator" keyword
* Hover text for default decreases clauses of loops.Gravatar Rustan Leino2013-12-20
| | | | Collected various routines used to create resolved Dafny expressions into the Expression class.
* Moved the hover text of iterator classes to the "iterator" keyword itself ↵Gravatar Rustan Leino2013-12-19
| | | | (since it is long and there may be other things hanging off the iterator name)
* MergeGravatar Rustan Leino2013-12-19
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 15:01:19 +0000