summaryrefslogtreecommitdiff
path: root/Source/Dafny/Resolver.cs
Commit message (Collapse)AuthorAge
* Fix issue 75. Adjust the fuel for existentials to use more fuel in an assumeGravatar qunyanm2016-03-31
| | | | context and less in an assert.
* Update module export error messages. Also for "import Y" if there is at leastGravatar qunyanm2016-03-21
| | | | | one exported view, but no exported view is marked as default, then it is an error.
* Fix issue 139. Allow bound variables in nested case patterns to shadow variablesGravatar qunyanm2016-02-26
| | | | declared outside the enclosing match.
* 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
| | | | a class is referenced.
* Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports.Gravatar qunyanm2016-02-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For the following situation module LibA { // ...things declared here... } module LibB { // ...things declared here... } module R { import opened LibA // ...things declared here... } module S refines R { import opened LibB // ...declared here... } 1. If module R declares a TopLevelDecl “G”, then we should report an error if S attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already. 2. If LibA declares a TopLevelDecl “G” but R does not directly declare any TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G” in S. This behavior is missing in Dafny. 3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S directly declares any TopLevelDecl “G”, then no error should be issued, and any use of “G” in S should resolve to the “G” in LibA. This behavior is missing in Dafny.
* Fix issue 129. When looking for a constructor for which Dafny knows how toGravatar qunyanm2016-02-02
| | | | | | | | instantiate all it arguments, don't stop as soon as one instantiable constructor is found. Instead, figure out all instantiable constructors and then pick the best among these. A simple and reasonable "best" is an instantiable constructor that requires a minimal number of already constructed type arguments, and to break ties among these, pick the first one listed.
* Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
| | | | module.
* Implement 'extern' declaration modifier.Gravatar Richard L. Ford2016-01-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The 'extern' declaration modifier provides a more convenient way of interfacing Dafny code with C# source files and .Net DLLs. We support an 'extern' keyword on a module, class, function method, or method (cannot extern ghost). We check the CompileNames of all modules to make sure there are no duplicate names. Every Dafny-generated C# class is marked partial, so it can potentially be extended. The extern keyword could be accompanied by an optional string naming the corresponding C# method/class to connect to. If not given the name of the method/class is used. An 'extern' keyword implies an {:axiom} attribute for functions and methods, so their ensures clauses are assumed to be true without proof. In addition to the .dfy files, the user may supply C# files (.cs) and dynamic linked libraries (.dll) on command line. These will be passed onto the C# compiler, the .cs files as sources, and the .dll files as references. As part of this change the grammar was refactored some. New productions are - TopDecls - a list of top-level declarations. - TopDecl - a single top-level declaration - DeclModifiers - a list of declaration modifiers which are either 'abstract', 'ghost', 'static', 'protected', or 'extern'. They can be in any order and we diagnose duplicates. In addition, since they are not all allowed in all contexts, we check and give diagnostics if an DeclModifier appears where it is not allowed.
* Mark temps that are generated in the resolver as auto-generated identifiers soGravatar qunyanm2016-01-20
| | | | that they don't show up in the VS IDE
* Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typedGravatar qunyanm2016-01-07
| | | | bound as undetermined so that iteration will continue.
* Fix issue 110. Set useImport to true when trying to registerTopLevelDeclsGravatar qunyanm2015-12-02
| | | | in MakeAbstractSignature.
* Fix issue 111. Create a new BoundVar for each CasePattern of MatchCaseExpr whenGravatar qunyanm2015-11-30
| | | | trying to substitute the nested CasePattern with the BoundVar.
* Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so thatGravatar qunyanm2015-11-25
| | | | the auto-triggers can be computed for ForallStmt.
* 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
| | | | it does not depend on the order they appeared.
* Introduced new datatype update syntax: D.(f := E)Gravatar leino2015-10-23
| | | | | The old syntax, D[f := E], is still supported for a short while, but generates a warning about that syntax being deprecated. The new syntax also supports multiple updates: D.(f := E0, g := E1, h := E2)
* 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 ↵Gravatar Bryan Parno2015-10-19
| | | | | | itself, as well as the signature and body of other functions.
* Implemented resolution, verification, and (poorly performing) compilation of ↵Gravatar leino2015-10-05
| | | | | | | existential if guards. Fixed bugs in ghost checks involving comprehensions and attributes. Added SubstituteBoundedPool method.
* Parsing and pretty printing of the new "existential guards" of the two kinds ↵Gravatar leino2015-10-03
| | | | of "if" statements.
* Hover text includes #[_k-1] suffix for terms rewritten in prefix ↵Gravatar Rustan Leino2015-10-02
| | | | | | | predicates/lemmas (this fixes an item from the wishlist). Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?). Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1].
* Removed some unused code.Gravatar Rustan Leino2015-09-30
|
* MergeGravatar leino2015-09-28
|\
* | Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
| | | | | | | | Moved all bounds discovery to resolution pass 1.
* | Removed the 'inSpecOnlyContext' map that had been part of the resolution ofGravatar leino2015-09-28
| | | | | | | | | | 'break' statements out of ghost structures. This is now done in pass 2 by looking at the .IsGhost field of the target statement.
* | Renamed CheckIsNonGhost to CheckIsCompilable.Gravatar leino2015-09-28
| |
* | Removed more traces of the previous resolution checks that happened during ↵Gravatar leino2015-09-28
| | | | | | | | | | | | pass 0. Fixed resolution of specification components of alternative loops.
* | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
| | | | | | | | | | | | | | Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions.
| * 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 ↵Gravatar Michael Lowell Roberts2015-09-21
| | | | | | | | ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
* | Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
| |
* | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing ↵Gravatar leino2015-08-31
|/ | | | for way to build up and later solve type constraints.
* 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 ↵Gravatar Rustan Leino2015-08-20
|/ | | | reference equality
* 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
| |\ | |/ |/| | | | | Changes that were needed included preventing the InductionRewriter from iterating on a SplitQuantifier and using the new error reporting engine.
| * 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
| | | | | | | | | | | | | | | | | | This requires rewriting the parts of the AST that contain these quantifiers. We unfortunately don't have facilities to do such rewrites at the moment (and there are loops in the AST, so it would be hard to write such a facility). As a workaround, this commit introduces a field in quantifier expressions, SplitQuantifiers. Code that manipulate triggers is expected to look for this field, and ignore the other fields if that one is found.
| * 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
| | | | | | | | | | The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
* | Bug fixes and improvements in pretty printingGravatar leino2015-08-11
| |
* | Moved discovery of induction variables into a Rewriter.Gravatar leino2015-08-11
|/ | | | | Generate warnings for malformed :induction arguments. Removed the functionality that allowed induction on 'this'.
* 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-06-05 00:17:35 +0000