| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires |  qunyanm | 2016-03-28 |
| | | | | | | it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. | ||
| * | Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that | qunyanm | 2015-11-25 |
| | | | | | the auto-triggers can be computed for ForallStmt. | ||
| * | Suppress many warnings in the test suite. |  Clément Pit--Claudel | 2015-08-28 |
| | | | | | | We already have separate tests for those, and we want the output to be the same with and without /autoTriggers. | ||
| * | Fix: Unify column numbers in Dafny's errors | Clément Pit--Claudel | 2015-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. | ||
| * | Minor fixes in .expect files | Clément Pit--Claudel | 2015-07-16 |
| | | |||
| * | Postpone reads checks of function preconditions until after the entire ↵ | leino | 2015-06-15 |
| | | | | | precondition has otherwise been checked for well-formedness | ||
| * | Combined some common routines into CheckWellformedAndAssume, which also ↵ | leino | 2015-06-12 |
| | | | | | allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change) | ||
| * | Fix lit headers implicitly relying on bash-style constructs | Clément Pit--Claudel | 2015-06-08 |
| | | | | | | Window's batch doesn't recognize ";" as a command separator; lit has a workaround for that, bu it's just as simple to do the right thing on our side. | ||
| * | Beefed up collection axioms (in particular, for maps) to improve the chance ↵ | Rustan Leino | 2015-03-10 |
| | | | | | of proving the existence check of let-such-that and assign-such-that | ||
| * | Snapshot, to be continued | leino | 2014-12-02 |
| | | |||
| * | Resolve attributes of a forall statement only after bound variables have ↵ | leino | 2014-10-29 |
| | | | | | | | | been added to the scope. Resolve the attributes of local variables. Don't resolve attributes of PredicateStmt's more than once. | ||
| * | Marked "free" as soon-to-be-deprecated | leino | 2014-10-25 |
| | | |||
| * | Updated expected test results for previous check-in | Rustan Leino | 2014-07-02 |
| | | |||
| * | Fixed a crash in the translation of fresh(seq<T>). | Rustan Leino | 2014-07-02 |
| | | |||
| * | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |