-
Andrei Paskevich authored
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.
b4caa997