Open bafain opened 12 years ago
When _ensures is not used to annotate a function like in the following code:
_ensures
_ensures true
The same applies to the annotations _requires when not used to annotate a function and _invariant when not used to annotate a loop.
_requires
_invariant
That error seems to be shown every time the parser comes across a token it cannot parse in that context. So a general error message such as This statement does not belong here would be sufficient.
This statement does not belong here
When
_ensures
is not used to annotate a function like in the following code:The same applies to the annotations
_requires
when not used to annotate a function and_invariant
when not used to annotate a loop.