Description:
- Choice was made to not add unused variables when there is no contract
and no body (no pre/(x)post, and no body).
- For postcondition variable result, we only check variables that are not
of unit type. And, we report a warning only if the variable is not present
in all the ensures.
- For result variable, with several imbricated raise, it seems possible to
have false positive with no location. Removing the no location case which
seems unhelpful anyway
- "diverges" states that the computation may not terminate (which
does not mean that is always diverges: just as any other effect
annotation, this clause states a possibility of a side effect).
- "reads {}" states that the computation does not access any variable
except those that are listed elsewhere in the specification (or the
proper function arguments, if "reads" is in a function spec).
- "writes {}" states that the computation does not modify any mutable
value.
- If a function definition or an abstract computation may diverge,
but there is no "diverges" clause in the specification, a warning
is produced. If a function definition or an abstract computation
always terminates, but there is a "diverges" clause in the spec,
an error is produced.
- If there is a "reads" or a "writes" clause in a function definition
or an abstract computation, then every modified value must be listed
in "writes" and every accessed external variable not mentioned in
the spec must be listed in "reads". (Notice that this is a stricter
requirement than before, when the presence of a "writes" clause
did not require to specify "reads".) However, one does not have to
write "reads {}" or "writes {}" if the corresponding lists are empty.
this commit changes the way of tracking occurrences of regions
and type variables for the purposes of generalization, effect
filtering, and effect checks. It restricts the previous
implementation in two aspects:
- a psymbol p can be monomorphic (= non-generalizable) in an effect
only if p depends (= is defined via) a pvsymbol whose type contains
the affected region. See bench/programs/bad-typing/recfun.mlw
for an example. This restriction is required for soundness.
- an argument of a psymbol cannot contain a region shared with
another argument or an external pvsymbol. However, we do not
require (so far) that the argument's type doesn't contain the same
region twice and we allow the result type to contain known regions.
This restriction is not necessary for soundness, and is introduced
only to avoid some unintentional user errors and reduce the gap
between the types that can be implemented in a "let" and the types
that can be declared in a "val".
