+
Point of view
All features
deferred class NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT]
Summary
top
A NULL-terminated C_ARRAY, useful since many low-level C functions expect to receive such arrays. The NULL (default_pointer in Eiffel) is not counted as an element of the array.
copyright
Copyright (C) 2007-2022: Paolo Redaelli This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
Direct parents
Inherit list: C_ARRAY
Class invariant
top
Overview
top
Features
Creation Note: space allocated in storage must always be capacity+1 large, to store the ending NULL pointer
{}
{ANY}
Creation
{}
{ANY}
Writing:
{ANY}
Adding:
{ANY}
  • add_first (element: ITEM_)
    Performance: O(count), not counting the eventual reallocation.
  • add_last (element: ITEM_)
    Performance: O(1), not counting the eventual reallocation.
  • add (element: ITEM_, index: INTEGER_32)
    Performance: O(count-index), not counting the eventual reallocation
Modification:
{ANY}
  • copy (other: NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT])
    Reinitialize by copying all the items of other.
  • force (element: ITEM_, index: INTEGER_32)
    Make element the item at index, enlarging the collection if necessary (new bounds except index are initialized with default values).
  • from_collection (model: COLLECTION[ITEM_])
    Initialize the current object with the contents of model.
Removing:
{ANY}
Looking and Searching:
{ANY}
Looking and comparison:
{ANY}
Other features:
{ANY}
  • replace_all (old_value: ITEM_, new_value: ITEM_)
    Replace all occurrences of the element old_value by new_value using is_equal for comparison.
  • fast_replace_all (old_value: ITEM_, new_value: ITEM_)
    Replace all occurrences of the element old_value by new_value using basic = for comparison.
  • slice (min: INTEGER_32, max: INTEGER_32): NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT]
    New collection consisting of items at indexes in [min..max].
  • reverse
    Reverse the order of the elements.
struct_size: INTEGER
{ANY}
Implementation
{C_ARRAY, WRAPPER_HANDLER}
Implement manifest generic creation (very low-level):
{}
TODO: unimplemented
{ANY}
Implementation
{WRAPPER, WRAPPER_HANDLER}
Accessing:
{ANY}
Writing:
{ANY}
Adding:
{ANY}
Looking and Searching:
{ANY}
Looking and comparison:
{ANY}
Other features:
{ANY}
Implement manifest generic creation:
{}
{ANY}
Other features:
{ANY}
Agent-based features:
{ANY}
Printing:
{ANY}
{ANY}
{}
Agent-based features:
{ANY}
{}
Indexing:
{ANY}
Implementation
{WRAPPER, WRAPPER_HANDLER}
  • wrapper_or_void (a_pointer: POINTER): ITEM_
    A wrapper for a_pointer or Void if a_pointer default_pointer (NULL in C).
Utility features
{}
Wrapper related exceptions
{}
Various exceptions codes:
{ANY}
{ANY}
Status report:
{ANY}
Basic operations:
{ANY}
  • die (code: INTEGER_32)
    Terminate execution with exit status code, without triggering an exception.
  • raise (name: STRING)
    Raise a developer exception of name name.
  • throw (a_exception: EXCEPTION)
Non-Standard Extensions:
{ANY}
{}
from_external (an_array: POINTER)
effective procedure
{}
top
Initialize the NULL_TERMINATED_C_ARRAY from an_array pointer.
The array is inspected from the beginning to discover the first NULL pointer that marks its end.
require
  • array_not_null: an_array.is_not_null
with_capacity (a_capacity: INTEGER_32)
effective procedure
{}
top
require
  • positive_capacity: a_capacity > 0
is_null_terminated: BOOLEAN
effective function
{ANY}
top
from_external_array (an_array: POINTER, a_length: INTEGER_32)
effective procedure
{}
top
require
  • array_not_null: an_array.is_not_null
  • positive_length: a_length > 0
item (i: INTEGER_32): ITEM_
effective function
{ANY}
top
Item at the corresponding index i.
See also lower, upper, valid_index.
require
    • valid_index(i)
    • valid_index(i)
first: ITEM_
effective function
{ANY}
top
The very first item.
See also last, item.
require
    • not is_empty
    • not is_empty
ensure
  • definition: Result = item(lower)
last: ITEM_
effective function
{ANY}
top
The last item.
See also first, item.
require
    • not is_empty
    • not is_empty
ensure
  • definition: Result = item(upper)
put (element: ITEM_, i: INTEGER_32)
effective procedure
{ANY}
top
Make element the item at index i.
See also lower, upper, valid_index, item, swap, force.
require
  • valid_index(i)
ensure
  • item(i) = element
  • count = old count
set_all_with (v: ITEM_)
effective procedure
{ANY}
top
Set all items with value v.
See also set_slice_with.
ensure
  • count = old count
add_first (element: ITEM_)
effective procedure
{ANY}
top
Performance: O(count), not counting the eventual reallocation.
ensure
  • first = element
  • count = 1 + old count
  • lower = old lower
  • upper = 1 + old upper
add_last (element: ITEM_)
effective procedure
{ANY}
top
Performance: O(1), not counting the eventual reallocation.
ensure
  • last = element
  • count = 1 + old count
  • lower = old lower
  • upper = 1 + old upper
add (element: ITEM_, index: INTEGER_32)
effective procedure
{ANY}
top
Performance: O(count-index), not counting the eventual reallocation
require
  • index.in_range(lower, upper + 1)
ensure
  • item(index) = element
  • count = 1 + old count
  • upper = 1 + old upper
copy (other: NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT])
effective procedure
{ANY}
top
Reinitialize by copying all the items of other.
require
    • not immutable
    • same_dynamic_type(other)
        • not immutable
        • same_dynamic_type(other)
          • not immutable
          • same_dynamic_type(other)
          • not immutable
          • same_dynamic_type(other)
        • not immutable
        • same_dynamic_type(other)
        • not immutable
        • same_dynamic_type(other)
ensure
  • is_equal(other)
force (element: ITEM_, index: INTEGER_32)
effective procedure
{ANY}
top
Make element the item at index, enlarging the collection if necessary (new bounds except index are initialized with default values).
See also put, item, swap.
require
  • index >= lower
ensure
  • upper = index.max(old upper)
  • item(index) = element
from_collection (model: COLLECTION[ITEM_])
effective procedure
{ANY}
top
Initialize the current object with the contents of model.
require
  • model /= Void
  • useful_work: model /= Current
ensure
  • count = model.count
remove_first
effective procedure
{ANY}
top
Performance: O(count)
require
  • not is_empty
ensure
  • count = old count - 1
  • lower = old lower + 1 xor upper = old upper - 1
remove_head (n: INTEGER_32)
effective procedure
{ANY}
top
Performance: O(upper-n)
require
  • n > 0 and n <= count
ensure
  • count = old count - n
  • lower = old lower + n xor upper = old upper - n
remove (index: INTEGER_32)
effective procedure
{ANY}
top
Performance: O(count)
require
  • valid_index(index)
ensure
  • count = old count - 1
  • upper = old upper - 1
remove_last
effective procedure
{ANY}
top
Performance: O(1)
require
  • not is_empty
ensure
  • count = old count - 1
  • upper = old upper - 1
remove_tail (n: INTEGER_32)
effective procedure
{ANY}
top
Performance: O(n)
require
  • n > 0 and n <= count
ensure
  • count = old count - n
  • upper = old upper - n
clear_count
effective procedure
{ANY}
top
Discard all items (is_empty is True after that call).
If possible, the actual implementation supposed to keep its internal storage area in order to refill Current in an efficient way.
See also clear_count_and_capacity.
ensure
  • is_empty: count = 0
clear_count_and_capacity
effective procedure
{ANY}
top
Instead of releasing the memory, it is reallocated with with 2 elements.
ensure
  • is_empty: count = 0
first_index_of (element: ITEM_): INTEGER_32
effective function
{ANY}
top
Give the index of the first occurrence of element using is_equal for comparison.
Answer upper + 1 when element is not inside.
See also fast_first_index_of, index_of, last_index_of, reverse_index_of.
ensure
  • definition: Result = index_of(element, lower)
index_of (element: ITEM_, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
top
Using is_equal for comparison, gives the index of the first occurrence of element at or after start_index.
Return upper + 1 if the search for element failed.
See also fast_index_of, reverse_index_of, first_index_of.
ensure
  • Result.in_range(start_index, upper + 1)
  • valid_index(Result) implies (create {SAFE_EQUAL}).test(element, item(Result))
reverse_index_of (element: ITEM_, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
top
Using is_equal for comparison, gives the index of the first occurrence of element at or before start_index.
Search is done in reverse direction, which means from the start_index down to the lower index . Answer lower -1 when the search fail.
See also fast_reverse_index_of, last_index_of, index_of.
require
  • valid_index(start_index)
ensure
  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result).is_equal(element)
fast_first_index_of (element: ITEM_): INTEGER_32
effective function
{ANY}
top
Note: comparison is done using the address of the wrapped structure.
ensure
  • definition: Result = fast_index_of(element, lower)
fast_index_of (element: ITEM_, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
top
Note: comparison is done using the address of the wrapped structure.
ensure
  • Result.in_range(start_index, upper + 1)
  • valid_index(Result) implies element = item(Result)
fast_reverse_index_of (element: ITEM_, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
top
Note: comparison is done using the address of the wrapped structure
require
  • valid_index(start_index)
ensure
  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result) = element
is_equal (other: NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT]): BOOLEAN
effective function
{ANY}
top
Do both collections have the same lower, upper, and items?
The basic = is used for comparison of items. Complexity: O(count)
require
    • other /= Void
        • other /= Void
          • other /= Void
          • other /= Void
        • other /= Void
        • other /= Void
ensure
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
  • Result implies lower = other.lower and upper = other.upper
all_default: BOOLEAN
effective function
{ANY}
top
Do all items have their type's default value?
 Note: for
non Void items, the test is performed with the
is_default predicate.
See also clear_all.
occurrences (element: ITEM_): INTEGER_32
effective function
{ANY}
top
Number of occurrences of element using is_equal for comparison.
See also fast_occurrences, index_of.
ensure
  • Result >= 0
fast_occurrences (element: ITEM_): INTEGER_32
effective function
{ANY}
top
Number of occurrences of element using basic its handle (or default_pointer) for comparison.
ensure
  • Result >= 0
replace_all (old_value: ITEM_, new_value: ITEM_)
effective procedure
{ANY}
top
Replace all occurrences of the element old_value by new_value using is_equal for comparison.
This feature is obsolete: Unimplemented!
fast_replace_all (old_value: ITEM_, new_value: ITEM_)
effective procedure
{ANY}
top
Replace all occurrences of the element old_value by new_value using basic = for comparison.
This feature is obsolete: Unimplemented!
slice (min: INTEGER_32, max: INTEGER_32): NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT]
effective function
{ANY}
top
New collection consisting of items at indexes in [min..max].
This feature is obsolete: Unimplemented!
reverse
effective procedure
{ANY}
top
Reverse the order of the elements.
This feature is obsolete: Unimplemented!
count: INTEGER_32
effective function
{ANY}
top
Number of available items in the hoard.
See also is_empty
ensure
  • Result >= 0
upper: INTEGER_32
writable attribute
{ANY}
top
Maximum index.
See also lower, valid_index, item.
lower: INTEGER_32
is 0
constant attribute
{ANY}
top
Minimum index.
See also upper, valid_index, item.
is_empty: BOOLEAN
effective function
{ANY}
top
Is the hoard empty ?
See also count.
ensure
  • definition: Result = count = 0
new_iterator: ITERATOR[ITEM_]
effective function
{ANY}
top
ensure
  • Result /= Void
  • Result.generation = generation
as_c_array: NATIVE_ARRAY[POINTER]
effective function
{ANY}
top
Current collection as a C array meant to be passed to C functions expectiong an array of wrapped items.
Result - at C level - will be a Item**, i.e. a pointer to pointers to Item structures or - in other words - an array of pointers to Items.
writable attribute
{C_ARRAY, WRAPPER_HANDLER}
top
capacity: INTEGER_32
writable attribute
{C_ARRAY, WRAPPER_HANDLER}
top
manifest_make (needed_capacity: INTEGER_32)
effective procedure
{}
top
Manifest creation of a LLVM_TYPE_ARRAY
require
  • needed_capacity > 0
manifest_put (index: INTEGER_32, element: ITEM_)
effective procedure
{}
top
require
  • index >= 0
clear_all
effective procedure
{ANY}
top
ensure
  • stable_upper: upper = old upper
  • stable_lower: lower = old lower
  • all_default
fast_has (an_item: ITEM_): BOOLEAN
effective function
{ANY}
top
ensure
  • definition: Result = valid_index(fast_first_index_of(an_item))
has (an_item: ITEM_): BOOLEAN
effective function
{ANY}
top
ensure
  • definition: Result = valid_index(first_index_of(an_item))
swap (i1: INTEGER_32, i2: INTEGER_32)
effective procedure
{ANY}
top
require
  • valid_index(i1)
  • valid_index(i2)
ensure
  • item(i1) = old item(i2)
  • item(i2) = old item(i1)
  • count = old count
append_collection (another: COLLECTION[ITEM_])
effective procedure
{ANY}
top
require
  • another /= Void
ensure
  • count = another.count + old count
wrapper (a_pointer: POINTER): ITEM_
deferred function
{WRAPPER, WRAPPER_HANDLER}
top
The wrapper for a_pointer.
It could be newly created or retrieved from a cache, a dictionary, from the underlying object, depending on the implementation.
require
  • pointer_not_null: a_pointer.is_not_null
ensure
  • non_void: Result /= Void
  • correct: Result.handle = a_pointer
infix "@" (i: INTEGER_32): E_
frozen
effective function
{ANY}
top
The infix notation which is actually just a synonym for item.
See also item.
require ensure
  • definition: Result = item(i)
set_slice_with (v: ANY, lower_index: INTEGER_32, upper_index: INTEGER_32)
effective procedure
{ANY}
top
Set all items in range [lower_index .. upper_index] with v.
See also set_all_with.
require ensure
append_traversable (other: TRAVERSABLE[E_])
effective procedure
{ANY}
top
Append other to Current.
See also add_last, add_first, add.
require
  • other /= Void
ensure
last_index_of (element: ANY): INTEGER_32
effective function
{ANY}
top
Using is_equal for comparison, gives the index of the last occurrence of element at or before upper.
Search is done in reverse direction, which means from the upper down to the lower index . Answer lower -1 when the search fail.
See also fast_last_index_of, reverse_index_of, index_of.
ensure
  • definition: Result = reverse_index_of(element, upper)
fast_last_index_of (element: ANY): INTEGER_32
effective function
{ANY}
top
Using basic = for comparison, gives the index of the last occurrence of element at or before upper.
Search is done in reverse direction, which means from the upper down to the lower index . Answer lower -1 when the search fail.
See also fast_reverse_index_of, last_index_of.
ensure
  • definition: Result = fast_reverse_index_of(element, upper)
fast_is_equal (other: NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT]): BOOLEAN
deferred function
{ANY}
top
Do both collections have the same lower, upper, and items?
The basic = is used for comparison of items.
See also is_equal, same_items.
ensure
is_equal_map (other: NULL_TERMINATED_C_ARRAY [ITEM_ -> C_STRUCT]): BOOLEAN
effective function
{ANY}
top
Do both collections have the same lower, upper, and items?
This feature is obsolete: Use `is_equal' instead.
same_items (other: COLLECTION[E_]): BOOLEAN
effective function
{ANY}
top
Do both collections have the same items?
The basic = is used for comparison of items and indices are not considered (for example this routine may yield True with Current indexed in range [1..2] and other indexed in range [2..3]).
See also is_equal, fast_is_equal.
require
  • other /= Void
ensure
move (lower_index: INTEGER_32, upper_index: INTEGER_32, distance: INTEGER_32)
effective procedure
{ANY}
top
Move range lower_index ..
upper_index by distance positions. Negative distance moves towards lower indices. Free places get default values.
See also slice, replace_all.
require ensure
manifest_semicolon_check: BOOLEAN
is False
constant attribute
{}
top
enumerate: ENUMERATE[E_]
effective function
{ANY}
top
get_new_iterator: ITERATOR[E_]
frozen
effective function
{ANY}
top
This feature is obsolete: Use `new_iterator' instead. This historical SmartEiffel feature is badly named.
for_each (action: PROCEDURE[TUPLE[TUPLE 1[E_]]])
effective procedure
{ANY}
top
Apply action to every item of Current.
See also for_all, exists, aggregate.
require
  • action /= Void
for_all (test: FUNCTION[TUPLE[TUPLE 1[E_]]]): BOOLEAN
effective function
{ANY}
top
Do all items satisfy test?
See also for_each, exists, aggregate.
require
  • test /= Void
exists (test: FUNCTION[TUPLE[TUPLE 1[E_]]]): BOOLEAN
effective function
{ANY}
top
Does at least one item satisfy test?
See also for_each, for_all, aggregate.
require
  • test /= Void
aggregate (action: FUNCTION[TUPLE[TUPLE 2[E_, E_], E_]], initial: E_): E_
effective function
{ANY}
top
Aggregate all the elements starting from the initial value.
See also for_each, for_all, exists.
require
  • action /= Void
out_in_tagged_out_memory
effective procedure
{ANY}
top
Append terse printable representation of current object in tagged_out_memory.
require
  • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
  • not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
  • append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))
generation: INTEGER_32
writable attribute
{ANY}
top
next_generation
effective procedure
{}
top
ensure
do_all (action: ROUTINE[TUPLE[TUPLE 1[E_]]])
frozen
effective procedure
{ANY}
top
Apply action to every item of Current.
This feature is obsolete: Use `for_each` instead. This feature is not secure because it accepts a FUNCTION, the result of which is lost.
_inline_agent1 (a: ROUTINE[TUPLE[TUPLE 1[E_]]], e: E_)
frozen
effective procedure
{}
top
valid_index (i: INTEGER_32): BOOLEAN
effective function
{ANY}
top
True when i is valid (i.e., inside actual bounds).
See also lower, upper, item.
ensure
wrapper_or_void (a_pointer: POINTER): ITEM_
effective function
{WRAPPER, WRAPPER_HANDLER}
top
A wrapper for a_pointer or Void if a_pointer default_pointer (NULL in C).
A commodity feature to replace the following code snippet: my_gobject: A_WRAPPER local p: POINTER do 
  p := get_foo(handle)
  if p.is_not_null then
    Result := factory.wrapper(p)
  end
end
with
my_gobject: A_G_OBJECT_HEIR
  do
    Result := factory.wrapper_or_void(get_foo(handle))
  end
ensure
  • null_pointer_returns_void: a_pointer.is_null implies Result = Void
  • correct: a_pointer.is_not_null implies Result /= Void and then Result.handle = a_pointer
null_or (a_wrapper: WRAPPER): POINTER
effective function
{}
top
The handle of a_wrapper, or the default_pointer if a_wrapper is Void
ensure
  • definition: Result = default_pointer or else a_wrapper /= Void and then Result = a_wrapper.handle
null_or_string (a_string: ABSTRACT_STRING): POINTER
effective function
{}
top
A pointer to a memory area containing the content of a_string or default_pointer if a_string is Void.
The memory area may be the internal buffer of a_string or a newly allocated one.
ensure
  • definition: Result = default_pointer or a_string /= Void implies Result = a_string.to_external
null_or_array (a_collection: WRAPPER_COLLECTION[WRAPPER]): POINTER
effective function
{}
top
A pointer to the contenct of a_collection or NULL (default_pointer) if a_collection is Void
ensure
  • definition: a_collection = Void implies Result.is_null and a_collection /= Void implies Result.is_not_null
collection_to_c_array (a_collection: COLLECTION[WRAPPER]): FAST_ARRAY[POINTER]
effective function
{}
top
An array containing the pointers to the objects wrapped by a_collection wrappers.
TODO: avoid creating a new array whenever possible.
require
  • a_collection /= Void
  • not a_collection.is_empty
pointer_to_unwrapped_deferred_object: STRING
is "A C function returned a pointer to an unwrapped object which is wrapped by a deferred class. It is not possible to create a correct wrapper."
constant attribute
{}
top
retrieved_object_mismatch: STRING
is "Retrieved_object_mismatch: the Eiffel wrapper associated with a pointer is not an actual wrapper for the object referred by that pointer "
constant attribute
{}
top
copying_an_uncopyable: STRING
is "Trying to copy an uncopyable wrapper: such objects are usually shortly lived"
constant attribute
{}
top
Check_instruction: INTEGER_32
is 1
constant attribute
{ANY}
top
Exception code for violated check.
Class_invariant: INTEGER_32
is 2
constant attribute
{ANY}
top
Exception code for violated class invariant.
Developer_exception: INTEGER_32
is 3
constant attribute
{ANY}
top
Exception code for developer exception.
See also: raise, throw
Incorrect_inspect_value: INTEGER_32
is 4
constant attribute
{ANY}
top
Exception code for inspect statement.
This exception occurs when Void is passed as the expression to inspect ("inspect on STRING only). This exception also occurs when the inspected value selects no branch (when the keyword "else" not used, one "when" branch _must_ be selected). Some value which is not one of the inspect constants, if there is no Else_part
Loop_invariant: INTEGER_32
is 5
constant attribute
{ANY}
top
Exception code for violated loop invariant
Loop_variant: INTEGER_32
is 6
constant attribute
{ANY}
top
Exception code for non-decreased loop variant
No_more_memory: INTEGER_32
is 7
constant attribute
{ANY}
top
Exception code for failed memory allocation
Postcondition: INTEGER_32
is 8
constant attribute
{ANY}
top
Exception code for violated postcondition.
Precondition: INTEGER_32
is 9
constant attribute
{ANY}
top
Exception code for violated precondition.
Routine_failure: INTEGER_32
is 10
constant attribute
{ANY}
top
Exception code for failed routine.
Os_signal: INTEGER_32
is 11
constant attribute
{ANY}
top
Exception code for a signal received from the OS.
Void_attached_to_expanded: INTEGER_32
is 12
constant attribute
{ANY}
top
Exception code for attachment of Void value to expanded entity.
Void_call_target: INTEGER_32
is 13
constant attribute
{ANY}
top
Exception code for feature applied to Void reference
System_level_type_error: INTEGER_32
is 14
constant attribute
{ANY}
top
Exception code for the system-level type error (this kind of error mostly arise with covariant redefinition).
exception_name: STRING
effective function
{ANY}
top
name_of_exception (a_exception: INTEGER_32): STRING
effective function
{ANY}
top
developer_exception: EXCEPTION
effective function
{ANY}
top
The last developer-thrown exception.
require
developer_exception_name: STRING
effective function
{ANY}
top
Name of last developer-raised exception.
require
is_developer_exception: BOOLEAN
effective function
{ANY}
top
Is the last exception originally due to a developer exception?
is_developer_named_exception: BOOLEAN
effective function
{ANY}
top
Is the last exception originally due to a developer exception?
is_developer_exception_of_name (name: STRING): BOOLEAN
effective function
{ANY}
top
Is the last exception originally due to a developer exception of name name?
assertion_violation: BOOLEAN
effective function
{ANY}
top
Is last exception originally due to a violated assertion or non-decreasing variant?
exception: INTEGER_32
{ANY}
top
Code of last exception that occurred.
is_signal: BOOLEAN
effective function
{ANY}
top
Is last exception originally due to an external event (operating system signal) ?
die (code: INTEGER_32)
effective procedure
{ANY}
top
Terminate execution with exit status code, without triggering an exception.
raise (name: STRING)
effective procedure
{ANY}
top
Raise a developer exception of name name.
require
  • name /= Void
throw (a_exception: EXCEPTION)
effective procedure
{ANY}
top
require
  • a_exception /= Void
signal_number: INTEGER_32
{ANY}
top
Signal Number received from OS.
 Zero if exception is not an OS signal.
named_exception: NAMED_EXCEPTION
once function
{}
top
developer_exception_memory: REFERENCE[EXCEPTION]
once function
{}
top
raise_exception (code: INTEGER_32)
{}
top