The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
MLCFG frontend : bugs with the `old` construct
The MLCFG translation scheme does not handle correctly the old construct:
-
for
oldoccuring in the post-condition of the global 'cfg' function, the duplication of that post-condition to the internal functions generated should replaceold twithat t Initfor the appropriate labelInit. -
for
oldoccuring 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)