class EXCEPTIONS

Features exported to INTERNALS_HANDLER

Facilities for adapting the exception handling mechanism. This class may be used as ancestor by classes needing its facilities.

Direct parents

non-conformant parents

ANY

Summary

exported features

Various exceptions codes:

Status report:

Basic operations:

Non-Standard Extensions:

Details

Check_instruction: INTEGER

Exception code for violated check.

Class_invariant: INTEGER

Exception code for violated class invariant.

Developer_exception: INTEGER

Exception code for developer exception.

Incorrect_inspect_value: INTEGER

Exception code for inspect value which is not one of the inspect constants, if there is no Else_part

Loop_invariant: INTEGER

Exception code for violated loop invariant

Loop_variant: INTEGER

Exception code for non-decreased loop variant

No_more_memory: INTEGER

Exception code for failed memory allocation

Postcondition: INTEGER

Exception code for violated postcondition.

Precondition: INTEGER

Exception code for violated precondition.

Routine_failure: INTEGER

Exception code for failed routine.

Os_signal: INTEGER

Exception code for a signal received from the OS.

Void_attached_to_expanded: INTEGER

Exception code for attachment of Void value to expanded entity.

Void_call_target: INTEGER

Exception code for feature applied to Void reference

System_level_type_error: INTEGER

Exception code for the system-level type error (this kind of error mostly arise whith covariant redefinition).

developer_exception_name: STRING

Name of last developer-raised exception.

require

  • applicable: is_developer_exception

is_developer_exception: BOOLEAN

Is the last exception originally due to a developer exception?

is_developer_exception_of_name (name: STRING): BOOLEAN

Is the last exception originally due to a developer exception of name name?

assertion_violation: BOOLEAN

Is last exception originally due to a violated assertion or non-decreasing variant?

exception: INTEGER

Code of last exception that occurred.

is_signal: BOOLEAN

Is last exception originally due to an external event (operating system signal) ?

die (code: INTEGER)

Terminate execution with exit status code, without triggering an exception.

raise (name: STRING)

Raise a developer exception of name name.

signal_number: INTEGER

Signal Number received from OS. Zero if exception is not an OS signal.

developer_exception_name_memory: REFERENCE [E_][STRING]
raise_exception (code: INTEGER)