Next: Arraylength, Previous: Counter of the operand stack, Up: BML primary expressions
The syntax of a stack-expression is as follows:
stack-expression ::=st(additive-expr)
A stack-expression can only be used in annotation statements (that is: assert, assume, set, unreachable and debug statements, and loop specifications, see Annotation (of) Statements)).
An expression of the form st(N) refers to the value
of the Nth element on the operand stack. The value of the argument
expression N should be between 0 and the value of cntr,
i.e., in the range of the operand stack. A typical use of a stack
expression is to specify a property on the value of the top element of
the operand stack.
For example, the top of the operand stack is greater than 3, or it is greater than the next value on the stack:
// assert st(cntr - 1) > 3 || st(cntr - 1) > st(cntr - 2);