2.16 Pragma Assertion_Level

Syntax:

pragma Assertion_Level (LEVEL_IDENTIFIER
                        [, depends => DEPENDENCY_DESCRIPTOR]);

DEPENDENCY_DESCRIPTOR ::= LEVEL_IDENTIFIER | LEVEL_IDENTIFIER_LIST

LEVEL_IDENTIFIER_LIST ::= '[' LEVEL_IDENTIFIER {, LEVEL_IDENTIFIER} ']'

For the semantics of this pragma, see the SPARK 2014 Reference Manual, section 11.4.3.