Counter of the Operand Stack - BML Reference Manual

Next: Stack Expressions, 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.