summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Fix issue 132. The formal argument can't be assume to be allocated when aGravatar qunyanm2016-02-12
| | | | function is invoked inside an "Old" expression.
* Fix issue 134. Wrong variable was used in the loop.Gravatar qunyanm2016-02-11
|
* Fix issue 133. The return type for some compare operators was wrongly typedGravatar qunyanm2016-02-11
| | | | as int instead of bool.
* Add /view:<view1, view2> option to filter module exports to be printed.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 120. Need to wrap operations that are "lit lifted" and turned intoGravatar qunyanm2016-02-08
| | | | boogie function calls with "Lit" function.
* Fix issue 124. Consider math operators that later turned into function callsGravatar qunyanm2016-02-08
| | | | as candidates for triggers.
* 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 128. Change the translation of CanCallAssumption for let-such-thatGravatar qunyanm2016-02-04
| | | | | | | | | | | | | expression from // CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] = // (forall b0,b1 :: typeAntecedent ==> // CanCall[[ RHS(b,g) ]] && // (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) && // $let$canCall(b,g)) to // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] = // $let$canCall(g) && // CanCall[[ Body($let$b0(g), $let$b1(g), h) ]]
* 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.
* Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"Gravatar qunyanm2016-02-02
|
* Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
| | | | module.
* Revert Makefile to its prior settingsGravatar Richard L. Ford2016-01-29
| | | | | The prior change did not work for people who had their setup using the previous values.
* Fix build and test failures, cleanup grammar.Gravatar Richard L. Ford2016-01-27
| | | | | | | | | | 1. A build failure caused by a method call before a contract was fixed. 2. An absolute path in an ".expect" file was changed to relative. 3. I eliminated the TopDecls and DeclModifiers non-terminals. They were giving a warning from Coco/R about being deletable. Instead I used repetition of the TopDecl or DeclModifier non-terminals where they had been used. I think this is also cleaner to talk about.
* 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.
* Fix issue 121. Don't split QuantifierExpr that are empty.Gravatar qunyanm2016-01-25
|
* Fix issue 122. Only generate autoTriggers for QuantifierExpr that are notGravatar qunyanm2016-01-25
| | | | empty.
* VS IDE performance - invoke dafny parser when the buffer hasn't changed forGravatar qunyanm2016-01-20
| | | | | | half a second, but delay calling Dafny resolver until the text buffer hasn't been changed for 5 seconds. Also save the parsing result from TokenTagger in ITextBuffer's property instead of in a static field.
* 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 117. Generate an error when the "opened" of an import doesn't matchGravatar qunyanm2016-01-08
| | | | between a module and its refinement base.
* Fix issue 118. When iteratively computing bounds, treat RefBoundedPool typedGravatar qunyanm2016-01-07
| | | | bound as undetermined so that iteration will continue.
* Removed Contract.Requires from method overrides (preconditions of overrides ↵Gravatar Rustan Leino2016-01-06
| | | | | | | | are inherited from the overridden method and Code Contracts will copy those preconditions to make sure the right run-time checking happens; when Code Contracts finds preconditions on overrides, it emits warnings).
* Fix some VS IDE performance issues.Gravatar qunyanm2016-01-06
| | | | | | | | | | | | - cache scan results so it can be shared between different instances of DafnyTokenTagger - Instead of rescanning the whole text buffer upon a text change, only rescan the text span that the text change is in. - set the timer to half a second to match the comment at the beginnig of the file. The event change are only passed along to Dafny when the user stop typing for half a second. - Change framework dependence so the project can work with version 4.5 and higher.
* 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
| | | | collectors.
* Fix printing for ForallStmt. Previously we traverse the resolved forallGravatar qunyanm2015-12-04
| | | | | | | | expressions to get the attributes for the forallstmt, which is flawed since the forallexpr could have been splitted into different subquantifiers each with different triggers. PrintExpression already knows how to print out splitted forall expressions, so we use it to print the resolved forall expressions instead.
* Fix issue 113. Make sure the tempVar name used in ToString() method doesn'tGravatar qunyanm2015-12-03
| | | | collide with the names of its formals.
* 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.
* Made an adjustment in the printing of resolved forall expressions (previous ↵Gravatar leino2015-11-28
| | | | | | | code introduced with bug fix 103 and tripped over with the /rprint and /autoTriggers:1 flags used in the new dafny4/UnionFind.dfy test).
* 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
|/ | | | the auto-triggers can be computed for ForallStmt.
* 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
| | | | occurrence of Set/MapComprehension when translating it to c#.
* Fix issue 107. Instead of writing out StaticReceiverExpr as null valuedGravatar qunyanm2015-11-17
| | | | LiteralExpr, write out its type instead.
* Fix issue 100. Add an axiom for functionHandle to trigger off of the origialGravatar qunyanm2015-11-17
| | | | function and connect with Apply1 of the function.
* Updated version number to 1.9.6.21116. This version is now on rise4fun.Gravatar leino2015-11-16
|
* 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
| | | | | | | | | | swap them when the expr is first created in parser or for calcstmt. This avoids problems of operands being swapped again when the expr is copied.
| * Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, weGravatar qunyanm2015-11-06
| | | | | | | | | | need exclude the private terms (the ones that includes the quantifier expr's bv) from it exported terms.
* | MergeGravatar leino2015-11-06
|\|
* | In the VS IDE, don't generate hover-text information for auto-generated ↵Gravatar leino2015-11-05
| | | | | | | | identifiers
| * Fix issue 104. Use ResolvedExpression to compute subexpressions forGravatar qunyanm2015-11-04
| | | | | | | | DatatypeUpdateExpr if ResovedExpression is not null.
| * Fix issue89. Copy the out param to a local before use it in an anonymousGravatar qunyanm2015-11-04
| | | | | | | | | | | | method that is generated by LetExpr. Change the compiler so that each stmt writes to its own buffer before add it to the program's buffer so that we can insert the above mentioned copy instruction before the stmt.
| * 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.
* MergeGravatar leino2015-10-26
|\