summaryrefslogtreecommitdiff
path: root/Test/dafny4
Commit message (Collapse)AuthorAge
* Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"Gravatar qunyanm2016-02-02
|
* 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.
* 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.
* Added flying robots example to test suiteGravatar 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
| | | | collectors.
* Fix issue 113. Make sure the tempVar name used in ToString() method doesn'tGravatar qunyanm2015-12-03
| | | | collide with the names of its formals.
* Add the test for Bug88.Gravatar qunyanm2015-12-02
|
* 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.
* MergeGravatar leino2015-11-27
|\
* | Added Union-Find program to test suite (could be cleaned up, but verifies)Gravatar 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.
* 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.
* Fix issue 94. Allow tuple-based assignment in statement contexts.Gravatar qunyanm2015-11-14
|
* 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.
* 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.
* update the test.Gravatar qunyanm2015-10-30
|
* 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.
* Fixed bug introduced in changeset 7ebdf9cd4154Gravatar leino2015-10-22
|
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
|
* Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
| | | | Moved all bounds discovery to resolution pass 1.
* Improvements in proofsGravatar leino2015-09-28
|
* 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.
* A test file with an example of least vs greatest fixpoints.Gravatar leino2015-09-22
|
* Proof that Ackermann can be curried and that it is monotonic in both arguments.Gravatar Rustan Leino2015-09-08
|
* Fix some tests by locally disabling auto triggersGravatar Clément Pit--Claudel2015-08-28
|
* Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
| | | | | We already have separate tests for those, and we want the output to be the same with and without /autoTriggers.
* Make use of new syntax in a test fileGravatar Rustan Leino2015-08-21
|
* Fixed bug in type unificationGravatar Rustan Leino2015-08-20
|
* Change the induction heuristic for lemmas to also look in precondition for ↵Gravatar leino2015-08-12
| | | | | | clues about which parameters to include. As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.
* Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ↵Gravatar Rustan Leino2015-07-28
| | | | | | time) in the test suite. Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do.
* Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
| | | | | | | | | Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests.
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\ | | | | | | | | This contains trigger related things under the autoTriggers flag (disabled by default), and some bug-fixes and cleanups that are already enabled.
* | Enable autoTriggers in LitTriggers and SeqFromArrayGravatar Clément Pit--Claudel2015-07-17
| |
* | Fix multiple tests that relied on z3 triggering on $BoxGravatar Clément Pit--Claudel2015-07-13
| | | | | | | | Found by enabling auto-generated triggers and looking for failing tests
| * Added another lemma to a test fileGravatar Rustan Leino2015-07-02
| |
| * MergeGravatar leino2015-07-01
| |\
| * | Fixed bug in BplImp!Gravatar leino2015-07-01
|/ / | | | | | | Improvements in encoding of reads of function values.
| * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
|/ | | | | | | | | | | | | | | | | | | i.e., how many times Z3 is permitted to unfold it's definition. The new {:fuel} annotation can be added to the function itself, it which case it will apply to all uses of that function, or it can overridden within the scope of a module, function, method, iterator, calc, forall, while, assert, or assume. The general format is: {:fuel functionName,lowFuel,highFuel} When applied as an annotation to the function itself, omit functionName. If highFuel is omitted, it defaults to lowFuel + 1. The default fuel setting for recursive functions is 1,2. Setting the fuel higher, say, to 3,4, will give more unfoldings, which may make some proofs go through with less programmer assistance (e.g., with fewer assert statements), but it may also increase verification time, so use it with care. Setting the fuel to 0,0 is similar to making the definition opaque, except when used with all literal arguments.
* MergeGravatar leino2015-06-12
|\
* | Added /vcs... cop-out to test case to make it go throughGravatar leino2015-06-12
| |
| * Fix a bug spotted by Chris in my BigInteger patch; thanks!Gravatar Clément Pit--Claudel2015-06-12
|/ | | | | | | | | | | The problem was this: Console.WriteLine(Int64.Parse("08000000000000000", NumberStyles.HexNumber)); // => -9223372036854775808 Console.WriteLine(Int64.Parse("9223372036854775808")); // => Value was either too large or too small for an Int64. In other words, large hex numbers are interpreted as a sequence of bits, not as an actual number.
* Generate #requires function for OpaqueFunction.Gravatar qunyanm2015-06-04
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 22:01:12 +0000