Next: , Previous: BML primary expressions, Up: BML primary expressions


5.3.1 Counter of the Operand Stack

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.