Table of Contents Previous Chapter

5.18 Class EXCEPTIONS

indexing

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

class interface

feature -- Access

developer_exception_name: STRING

-- Name of last developer-raised exception

require

applicable: is_developer_exception

feature -- Access

Check_instruction: INTEGER

-- Exception code for violated check

Class_invariant: INTEGER

-- Exception code for violated class invariant

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

Void_attached_to_expanded: INTEGER

-- Exception code for attachment of void value

-- to expanded entity

Void_call_target: INTEGER

-- Exception code for violated check

feature -- Status report

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_developer_exception: BOOLEAN

-- Is the last exception originally due to

-- a developer exception?

is_signal: BOOLEAN

-- Is last exception originally due to an external

-- event (operating system signal)?

feature -- Basic operations

die (code: INTEGER)

-- Terminate execution with exit status code,

-- without triggering an exception.

raise (name: STRING)

-- Raise a developer exception of name name.

end