caveat: pass-as-reference does not work in chain relations.
That is, 0 < r += 12 will not typecheck even
if x is autodereferencing and (+=) has the
first parameter with the reference marker.
todo: forbid reference markers in logic, in type definitions,
over logical symbols, etc.
todo: update extraction drivers.
- type "ref",
- constructor "mk ref" (never used in Typing)
- projection "contents" (both val and function)
- program function "ref" (alias for "mk ref")
- let-function (!)
- program function (:=)
It is important to attribute the symbols to their
respective modules, since a program with reference
variables may never use ref.Ref and why3.Ref.Ref
is imported automatically.