Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unhelpful error message about reads clause #5262

Closed
MikaelMayer opened this issue Mar 27, 2024 · 0 comments · Fixed by #5265
Closed

Unhelpful error message about reads clause #5262

MikaelMayer opened this issue Mar 27, 2024 · 0 comments · Fixed by #5265
Assignees
@MikaelMayer
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials

Comments

@MikaelMayer
Copy link
Member

Dafny version

latest-nightly

Code to produce this issue

trait Entries<T> {
  var entries: array<T>
  method Copy() returns (x: array<T>)
    ensures fresh(x) && x[..] == entries[..]
  {
    x := new T[entries.Length](
        i requires 0 <= i < entries.Length
        reads entries
        //    ^^^^^^^ Insufficient reads clause to read field
        => entries[i]);
  }
}

Command to run and resulting output

Paste in VSCode and see the error message.

What happened?

I did not get it why it could not read the array "entries" since it's in a method.
It turns out, "entries" is a shortcut for "this.entries", which means that this expression requires "reads this".
I think I would have immediately spotted it if, instead of the error message:

Insufficient reads clause to read field

I would have had the following error message, at least because "this" is implicit.

Insufficient reads clause to read field 'entries', perhaps try adding reads 'this' in the enclosing scope

What type of operating system are you experiencing the problem on?

Windows
@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: documentation Dafny's reference manual, tutorial, and other materials kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny and removed kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label labels Mar 27, 2024
@MikaelMayer MikaelMayer mentioned this issue Mar 28, 2024
Merged
@MikaelMayer MikaelMayer self-assigned this Mar 28, 2024
MikaelMayer added a commit that referenced this issue Mar 29, 2024
@MikaelMayer
Fix: Enhanced "insufficient reads clause to read field" (#5265)
4a3aace 
This PR enhances the error message, giving more context. Fixes #5262

For example, in the context of a method where `x` is a field,

    x := 5;
    f := () => if 5 / x == 1 then 2 else 3;
                      ^ Error here

Instead of saying 

git-issue-405.dfy(19,22): Error: insufficient reads clause to read field

the new message is more helpful:

git-issue-405.dfy(19,22): Error: insufficient reads clause to read
field;
Consider extracting this.x to a local variable, or adding 'reads this'
    in the enclosing lambda specification for resolution

The first part of this message is added only for lambda expressions, the
second part is always present for scope tolerating a reads clause. For
scopes such as functions or methods, where the reads clause can
sometimes be more fine-grained, the hint `or 'reads this`x'` is added
for discoverability.
For scopes without a possible resolution, the following error message is
now emitted:

    Error: insufficient reads clause to read field; Mutable fields
    cannot be accessed within certain scopes, such as default
    values or the right-hand side of constants

For a function by method, the scope is the function and not the method
body.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@MikaelMayer MikaelMayer

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Enhanced "insufficient reads clause to read field" dafny-lang/dafny
1 participant
@MikaelMayer