Pragma Exit_Cases (GNAT Reference Manual) (original) (raw)

Next: Pragma Export_Function, Previous: Pragma Exceptional_Cases, Up: Implementation Defined Pragmas [Contents][Index]

2.58 Pragma Exit_Cases ¶

Syntax:

pragma Exit_Cases (EXIT_CASE_LIST);

EXIT_CASE_LIST ::= EXIT_CASE {, EXIT_CASE} EXIT_CASE ::= GUARD => EXIT_KIND EXIT_KIND ::= Normal_Return | Exception_Raised | (Exception_Raised => exception_name) GUARD ::= Boolean_expression

For the semantics of this aspect, see the SPARK 2014 Reference Manual, section 6.1.10.