summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Release for unstableHEADmasterGravatar Benjamin Barenblat2016-06-05
|
* Patch Dafny to use the system Z3Gravatar Benjamin Barenblat2016-06-05
| | | | | | | | In previous versions, it was sufficient to just pass /z3exe:/usr/bin/z3 in the dafny launcher script, but now, Dafny looks for its vendored Z3 (which we don’t install) at runtime and prints a warning if it’s gone. Patch that behaviour away, hardcoding /usr/bin/z3 as the Z3 binary location.
* Update debian/gbp.confGravatar Benjamin Barenblat2016-06-05
|
* Update debian/copyrightGravatar Benjamin Barenblat2016-06-05
|
* Update debian/copyrightGravatar Benjamin Barenblat2016-06-05
|
* Update debian/controlGravatar Benjamin Barenblat2016-06-05
|
* Bump debian/changelogGravatar Benjamin Barenblat2016-06-05
|
* Merge commit 'df5c5f5'Gravatar Benjamin Barenblat2016-05-30
|\
* | Update dependencies and Standards-VersionGravatar Benjamin Barenblat2016-04-06
| |
| * New version number 1.9.7.30401, for binary release on Codeplex and Rise4fun.Gravatar leino2016-04-01
| | | | | | | | Changed copyright date to include 2016.
| * MergeGravatar leino2016-04-01
| |\
| * | New test file, for recursive and iterative versions of McCarthy's 91 functionGravatar leino2016-04-01
| | |
| * | New test case, proving monad laws for listsGravatar leino2016-04-01
| | |
| | * Fix issue 148. The results for sign comparison for BigRational.CompareTo wasGravatar qunyanm2016-04-01
| |/ | | | | | | wrong.
| * Allow modifies clauses for a "Main" method annotated with {:main} attribute.Gravatar qunyanm2016-03-31
| |
| * Fix issue 143. The list that stores the function fuel constants was declared asGravatar qunyanm2016-03-31
| | | | | | | | static field and not initialized correctly. Make it an instance field instead.
| * MergeGravatar qunyanm2016-03-31
| |\
| * | Fix issue 75. Adjust the fuel for existentials to use more fuel in an assumeGravatar qunyanm2016-03-31
| | | | | | | | | | | | context and less in an assert.
| | * Add a wrapper for DafnyServer.exeGravatar Clément Pit--Claudel2016-03-30
| |/
| * Allow users to annontate a method as main with {:main} attribute. It’s an ↵Gravatar qunyanm2016-03-28
| | | | | | | | | | | | | | | | | | error if more than one method is so annotated. For that method, the usual restrictions for "main" apply, but it is allowed to take ghost arguments, and it is allowed to have preconditions. This lets the programmer add some explicit assumptions about the outside world, modeled, for example, via ghost parameters.
| * Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresGravatar qunyanm2016-03-28
| | | | | | | | | | it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run.
| * 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 93. Add per-function fuel setting that can be adjusted locally basedGravatar qunyanm2016-03-18
| | | | | | | | on context.
| * Added test case to go with the recent fix of Issue #49 (changeset f354709009a5).Gravatar Rustan Leino2016-03-01
| |
| * MergeGravatar Rustan Leino2016-03-01
| |\
| * | Revised the $Is and $IsAlloc axioms for arrow terms. It is now possible toGravatar Rustan Leino2016-03-01
| | | | | | | | | | | | | | | derived these predicates. More things can now be verified (including the problem reported in Issue #49).
| * | Added a return-value contractGravatar Rustan Leino2016-02-29
| | |
| | * Revert change 1997 (bfe7c149bef1). IDE performance. Don't delay the resolverGravatar qunyanm2016-02-29
| | | | | | | | | | | | until the editor is idle for 5 second.
| | * Fix issue 139. Allow bound variables in nested case patterns to shadow variablesGravatar qunyanm2016-02-26
| |/ | | | | | | declared outside the enclosing match.
| * MergeGravatar Rustan Leino2016-02-26
| |\
| * | Changes to CanCall assumptions:Gravatar Rustan Leino2016-02-26
| | | | | | | | | | | | | | | | | | - various peephole optimizations of formulas, to generate fewer tautologies - removed unused bound variables in CanCall quantifications (this addresses Issue #135) - added type- and precondition-antecedent in quantified CanCall assumption for lambda expressions, thus fixing an unsoundness
| | * Fix issue 138. Allow parenthese with the nullary constructor inGravatar qunyanm2016-02-26
| | | | | | | | | | | | "case" of a match statement and match expression.
| | * Fix test failure. Print the resulting boogie code to a file insteadGravatar qunyanm2016-02-26
| | | | | | | | | | | | of console.
| | * Fix issue 140. Move the initializion of _this before the TAIL_CALL_START label.Gravatar qunyanm2016-02-26
| | |
| | * Fix issue 136. Less aggressive Lit wrap for assert/assume.Gravatar qunyanm2016-02-26
| |/
| * Update the test's .expect file since the fix is merged into boogie.Gravatar qunyanm2016-02-12
| |
| * 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
| |
| * MergeGravatar qunyanm2016-02-09
| |\
| * | Fix issue 131. Instead of crashing, report an error when an undefined member ofGravatar qunyanm2016-02-09
| | | | | | | | | | | | a class is referenced.
| | * Renamed identifiers for increased geopolitical appealGravatar Rustan Leino2016-02-08
| |/
| * 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.
| * Last checkin checked in the wrong version of bug125.dfy. The failure part ofGravatar qunyanm2016-02-05
| | | | | | | | | | the test was moved into test\dafny0\modules0.dfy so that bug125.dfy can be verified that it was resolved to the correct types.
| * 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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-20 02:44:33 +0000