Pragma Exit_Cases (GNAT Reference Manual)

### 2.59 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)
                     | Program_Exit
    GUARD          ::= Boolean_expression

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