| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
can now assume the precondition (as had also been the case back in the days when
reads clauses had to be self framing).
|
| |
|
|
|
|
| |
Test/dafny0/Reads.dfy for benefits.
(Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.)
|
| | |
|
| | |
|
| |
|
|
| |
precondition has otherwise been checked for well-formedness
|
| | |
|
| |
|
|
| |
allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)
|
|
|
* The reads clause now needs to be self framing.
* The requires clause now needs to be framed by the reads clause.
* There are one-shot lambdas, with a single arrow, but they will probably be
removed.
* There is a {:heapQuantifier} attribute to quantifiers, but they will
probably be removed.
* Add smart handling of type variables
* Add < and > for datatype & type parameter
|
Clément Pit--Claudel
Rustan Leino
Dan Rosén