You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hanfor allows for a number of broken requirements to be exported without warning (leading to the ultimte requirements parser being unable to parse these requirements). There should be a warning or at least no export of the following ill formed requirements:
CONST someConstant IS None, where no value for a constant was given in Hanfor, thus python None was written in the requirement
CONST some.Constant IS 4, where the variable name contains a . wich is not intended for names in BoogiePL
Requirements that have non-constant variables in their time bounds
Requirements that use enumerators of an enumeration that is unused: the enumerators are not defined as constants if the enumeration is not used in the requirements thus the enumerators are unknown in the Boogie file.
Export while there are variables typed as unknown that are used in the req.
The text was updated successfully, but these errors were encountered:
Hanfor allows for a number of broken requirements to be exported without warning (leading to the ultimte requirements parser being unable to parse these requirements). There should be a warning or at least no export of the following ill formed requirements:
CONST someConstant IS None
, where no value for a constant was given in Hanfor, thus pythonNone
was written in the requirementCONST some.Constant IS 4
, where the variable name contains a.
wich is not intended for names in BoogiePLunknown
that are used in the req.The text was updated successfully, but these errors were encountered: