MLCFG frontend : bugs with the `old` construct
The MLCFG translation scheme does not handle correctly the old
construct:
-
for
old
occuring in the post-condition of the global 'cfg' function, the duplication of that post-condition to the internal functions generated should replaceold t
withat t Init
for the appropriate labelInit
. -
for
old
occuring in a code invariant, the same replacement should occur as well
(Note: I distinguish the case of code invariants since for me it is not so clear that the use of old
should be allowed at all... it is another story)