summaryrefslogtreecommitdiff
path: root/Source/Dafny/Resolver.cs
Commit message (Expand)AuthorAge
* Fix issue 75. Adjust the fuel for existentials to use more fuel in an assumeGravatar qunyanm2016-03-31
* Update module export error messages. Also for "import Y" if there is at leastGravatar qunyanm2016-03-21
* Fix issue 139. Allow bound variables in nested case patterns to shadow variablesGravatar qunyanm2016-02-26
* Fix issue 134. Wrong variable was used in the loop.Gravatar qunyanm2016-02-11
* Fix issue 131. Instead of crashing, report an error when an undefined member ofGravatar qunyanm2016-02-09
* Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.Gravatar qunyanm2016-02-05
* Fix issue 129. When looking for a constructor for which Dafny knows how toGravatar qunyanm2016-02-02
* Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
* Implement 'extern' declaration modifier.Gravatar Richard L. Ford2016-01-27
* Mark temps that are generated in the resolver as auto-generated identifiers soGravatar qunyanm2016-01-20
* Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typedGravatar qunyanm2016-01-07
* 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
* Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
* Fix issue 94. Allow tuple-based assignment in statement contexts.Gravatar qunyanm2015-11-14
* Fix issue 91 - Change how we compute the bounds of quantified variables so thatGravatar qunyanm2015-10-29
* 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
* 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
* 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
* | 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
* | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing f...Gravatar leino2015-08-31
|/
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
* | Cleanup a number of FIXMEs that I had left in the codeGravatar Clément Pit--Claudel2015-08-20
| * Changed equality tests involving traits from using strings to using reference...Gravatar Rustan Leino2015-08-20
|/
* Fixed bug in type unificationGravatar Rustan Leino2015-08-20
* MergeGravatar Rustan Leino2015-08-20
|\
* | Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
| * Merge.Gravatar Clément Pit--Claudel2015-08-19
| |\ | |/ |/|
| * Refactor calls to 'new CallCmd' and clear a few FIXMEsGravatar Clément Pit--Claudel2015-08-18
* | Update the way bounds are discovered to try to choose "better" bounds.Gravatar Bryan Parno2015-08-17
| * Start committing split quantifiersGravatar Clément Pit--Claudel2015-08-14
| * Run the trigger rewriter after the quantifier splitterGravatar Clément Pit--Claudel2015-08-14
| * Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
* | Bug fixes and improvements in pretty printingGravatar leino2015-08-11
* | Moved discovery of induction variables into a Rewriter.Gravatar leino2015-08-11
|/
* Bug fix: check that assign-such-that constraint is of type booleanGravatar Rustan Leino2015-07-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 23:57:42 +0000