Dafny version

4.11

Code to produce this issue

method ReadUnapplied(c: Cell)
  reads {}
{
  if
  case true =>
    var arr := new int[10](_ reads c => c.data); // error: insufficient reads // BUG: missing check
  case true =>
    var x := c.data; // error: insufficient reads
  case true =>
    var x := ReadAnObject(c); // error: insufficient reads
  case true =>
    var f := ReadAnObject;
    var x := f(c); // error: insufficient reads
  case true =>
    var s := seq(10, _ reads c => c.data); // error: insufficient reads
}

class Cell {
  var data: int
}

function ReadAnObject(c: Cell): int
  reads c
{
  c.data
}

Command to run and resulting output

% dafny verify --type-system-refresh --general-traits=datatype --general-newtypes --reads-clauses-on-methods test.dfy
test.dfy(8,15): Error: insufficient reads clause to read field; Consider adding 'reads c' or 'reads c`data' in the enclosing method specification for resolution
  |
8 |     var x := c.data; // error: insufficient reads
  |                ^^^^

test.dfy(10,25): Error: insufficient reads clause to invoke function
   |
10 |     var x := ReadAnObject(c); // error: insufficient reads
   |                          ^

test.dfy(13,13): Error: insufficient reads clause to invoke function
   |
13 |     var x := f(c); // error: insufficient reads
   |              ^

test.dfy(15,13): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor
   |
15 |     var s := seq(10, _ reads c => c.data); // error: insufficient reads
   |              ^^^


Dafny program verifier finished with 1 verified, 4 errors

What happened?

4 of the 5 read operations above correctly generate an error message, but 1 is missing. The initializer function that's given to the new array allocation should also be checked for read effects.

The missing is essentially a statement-level read operation, whereas all the others are expression-level read operations. This probably explains the bug, because the functionality in the Dafny implementation to inspect read effects is defined on expressions. To produce an error message for this as well, there needs to be a traversal over statements that, when --reads-clauses-on-methods is used, checks the array initializer function (if any) for having allowed read effects. The code for checking this initializer is going to be very similar (or identical) to the expression check that the seq constructor (see the examples above) has allowed read effects in its initializer.

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

Mac