Next: Stack expressions, Previous: BML primary expressions, Up: BML primary expressions
The syntax of a cntr-expression is as follows:
cntr-expression ::= cntr
The primary cntr
can only be used in annotation statements
(that is: assert, assume, set, unreachable and debug statements, and loop
specifications, see Annotation (of) Statements). Its value is the current size of the operand stack.