Pragma Exit_Cases (GNAT Reference Manual)

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.