summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| * Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
| * Revert Makefile to its prior settingsGravatar Richard L. Ford2016-01-29
| * Add Dafny reference manualGravatar Richard L. Ford2016-01-27
| * Fix build and test failures, cleanup grammar.Gravatar Richard L. Ford2016-01-27
| * Add ExternNegative2.dfy.expect.Gravatar Richard L. Ford2016-01-27
| * Implement 'extern' declaration modifier.Gravatar Richard L. Ford2016-01-27
| * 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
| * VS IDE performance - invoke dafny parser when the buffer hasn't changed forGravatar qunyanm2016-01-20
| * 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
| * Added flying robots example to test suiteGravatar Rustan Leino2016-01-06
| * Fix some VS IDE performance issues.Gravatar qunyanm2016-01-06
| * Fix issue 116. Add the missing @ for the generated c# code.Gravatar qunyanm2016-01-05
| * Add /autoTriggers:1 to remove the undeterminateness of proof search.Gravatar qunyanm2015-12-15
| * 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
| * Add the test for Bug88.Gravatar qunyanm2015-12-02
| * Fix issue 110. Set useImport to true when trying to registerTopLevelDeclsGravatar qunyanm2015-12-02
| * Update the test .expect files since the line number info is fixed with boogieGravatar 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
| |\
| * | Added Union-Find program to test suite (could be cleaned up, but verifies)Gravatar 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
| * Changed checked-in version of Z3 to 4.4.1 (from 4.4.0)Gravatar leino2015-11-17
| * 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
| * 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
| | * Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, weGravatar qunyanm2015-11-06
| * | MergeGravatar leino2015-11-06
| |\|
| * | Updated syntax of test case to remove unnecessary semicolons and parenthesesGravatar leino2015-11-05
| * | In the VS IDE, don't generate hover-text information for auto-generated ident...Gravatar leino2015-11-05
| | * 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
| | * Add some files to .hgignore.Gravatar wuestholz2015-11-02
| | * update the test.Gravatar qunyanm2015-10-30
| | * Fix issue 91 - Change how we compute the bounds of quantified variables so thatGravatar qunyanm2015-10-29
| | * Check version info before delete white space so that it will work with pythonGravatar qunyanm2015-10-28
| |/
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-20 11:45:53 +0000