class ASSERTION
Summary
Class invariant
Overview
creation features
exported features
tag: TAG_NAME
writable attribute
expression: EXPRESSION
writable attribute
comment: COMMENT
writable attribute
start_position: POSITION
effective function
pretty (indent_level: INTEGER_32)
effective procedure
short (type: TYPE, h01: STRING, r01: STRING, h02: STRING, r02: STRING, h03: STRING, r03: STRING, h04: STRING, r04: STRING, h05: STRING, r05: STRING, h06: STRING, r06: STRING, h07: STRING, r07: STRING, h08: STRING, r08: STRING, h09: STRING, r09: STRING, h10: STRING, r10: STRING, h11: STRING, r11: STRING, h12: STRING, r12: STRING, h13: STRING, r13: STRING)
effective procedure
use_current (type: TYPE): BOOLEAN
effective function
compile_to_c (type: TYPE)
effective procedure
is_always_true: BOOLEAN
effective function
safety_check (type: TYPE)
effective procedure
accept (visitor: ASSERTION_VISITOR)
effective procedure
Accept to be visited by the visitor.