By popular demand, read effects are back. They serve to mark dependence
of a program function on external variables which are otherwise not
mentioned in the function's specification. Such annotation is necessary,
for example, to add the needed type invariants.

The "reads" clauses are comma-separated variables (contrary to write
effects, where one must point out the modified field).

If a user specifies a "reads" clause for a defined function, we check
that every listed variable occurs in the code and that every free
variable in the code occurs in the specification (which includes the
"reads" clause). Notice that this concers function arguments, too:

  val r : ref int
  let f (x : ref int) reads {r} = x := !r

would require x to be added to reads.

One exception to this rule is the the result type in a non-recursive
function may contain regions coming the function's arguments (though
not from the context). It is sometimes useful to write a function
around a constructor or a projection: see function [create] in
verifythis_fm2012_LRS.mlw. For recursive functions we impose
the full non-alias discipline.