diff options
| author |  Rustan Leino <unknown> | 2014-01-14 16:32:17 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-14 16:32:17 -0800 |
| commit | f27a3687977016270740f62b35beb2830278af56 (patch) | |
| tree | 5d45a5630399b559f1ebf0d963c780db149bbddc /Test/dafny0/Definedness.dfy | |
| parent | 48d3c16cb2a20e3a0c761c590abe28adaa47fbfd (diff) | |
Improve error information by generating "Related location" information that traces into preconditions of called functions
Diffstat (limited to 'Test/dafny0/Definedness.dfy')
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 58337a26..af078003 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -74,7 +74,7 @@ class StatementTwoShoes { var s: StatementTwoShoes;
function method F(b: int): StatementTwoShoes
requires 0 <= b;
- reads this;
+ reads this;
{
s
}
|