summaryrefslogtreecommitdiff
path: root/Source/Dafny
Commit message (Expand)AuthorAge
* Mark temps that are generated in the resolver as auto-generated identifiers soGravatar qunyanm2016-01-20
* Fix issue 117. Generate an error when the "opened" of an import doesn't matchGravatar qunyanm2016-01-08
* Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typedGravatar qunyanm2016-01-07
* Removed Contract.Requires from method overrides (preconditions of overrides a...Gravatar Rustan Leino2016-01-06
* Fix issue 116. Add the missing @ for the generated c# code.Gravatar qunyanm2016-01-05
* Fix issue 114. Do not export private terms for ComprehensionExpr in triggerGravatar qunyanm2015-12-08
* Fix printing for ForallStmt. Previously we traverse the resolved forallGravatar qunyanm2015-12-04
* Fix issue 113. Make sure the tempVar name used in ToString() method doesn'tGravatar qunyanm2015-12-03
* Fix issue 110. Set useImport to true when trying to registerTopLevelDeclsGravatar qunyanm2015-12-02
* Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr whenGravatar qunyanm2015-11-30
* Made an adjustment in the printing of resolved forall expressions (previous c...Gravatar leino2015-11-28
* MergeGravatar leino2015-11-27
|\
* | Make cached results dependent on if a function is ghost or notGravatar leino2015-11-27
* | autocontracts: Don't add modifies clause to ghost methodsGravatar leino2015-11-27
| * Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
|/
* Add code that uses Z3's optimization features (currently disabled by default).Gravatar wuestholz2015-11-19
* Fix issue 108. Use idGenerator to create a new collection name for eachGravatar qunyanm2015-11-18
* Fix issue 107. Instead of writing out StaticReceiverExpr as null valuedGravatar qunyanm2015-11-17
* Fix issue 100. Add an axiom for functionHandle to trigger off of the origialGravatar qunyanm2015-11-17
* Fix issue 94. Allow tuple-based assignment in statement contexts.Gravatar qunyanm2015-11-14
* MergeGravatar leino2015-11-11
|\
* | Fixed compilation of equality between reference typesGravatar leino2015-11-11
| * Fix issue 101. Instead of swapping operands for Exp opcode in BinaryExpr,Gravatar qunyanm2015-11-10
| * Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, weGravatar qunyanm2015-11-06
|/
* Fix issue 104. Use ResolvedExpression to compute subexpressions forGravatar qunyanm2015-11-04
* Fix issue89. Copy the out param to a local before use it in an anonymousGravatar qunyanm2015-11-04
* Fix issue 91 - Change how we compute the bounds of quantified variables so thatGravatar qunyanm2015-10-29
* Fixed location of blue dots to appear after semi-colons, not just before them.Gravatar leino2015-10-26
* In method and iterator specifications, inline top-level predicates (exceptGravatar leino2015-10-24
* Introduced new datatype update syntax: D.(f := E)Gravatar leino2015-10-23
* Refactored resolution of datatype updates, preparing for a change of syntaxGravatar leino2015-10-23
* Fixed bug introduced in changeset 7ebdf9cd4154Gravatar leino2015-10-22
* Improve Dafny's ability to find fueled functions by checking the function its...Gravatar Bryan Parno2015-10-19
* Implemented resolution, verification, and (poorly performing) compilation of ...Gravatar leino2015-10-05
* Parsing and pretty printing of the new "existential guards" of the two kinds ...Gravatar leino2015-10-03
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l...Gravatar Rustan Leino2015-10-02
* Removed some unused code.Gravatar Rustan Leino2015-09-30
* MergeGravatar leino2015-09-28
|\
* | Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
* | Removed the 'inSpecOnlyContext' map that had been part of the resolution ofGravatar leino2015-09-28
* | Renamed CheckIsNonGhost to CheckIsCompilable.Gravatar leino2015-09-28
* | Removed more traces of the previous resolution checks that happened during pa...Gravatar leino2015-09-28
* | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
| * fixed bugs related to identifying newtypes as types of integers and reals.Gravatar Michael Lowell Roberts2015-09-23
| * fix for warnings related to deprecated z3 options (please update to the lates...Gravatar Michael Lowell Roberts2015-09-22
* | Removed unused code (old code from previous ghost-statement handling)Gravatar leino2015-09-21
* | Moved premature uses of .IsGhost for Statement'sGravatar leino2015-09-21
| * merged IronDafny updates. two unit tests related to traits do not pass if ENA...Gravatar Michael Lowell Roberts2015-09-21
* | Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 23:59:44 +0000