indexing
	description: "[
		To easily manage allocation and release of allocated C memory, and
		to perform insertion of basic elements. Byte order is by default
		platform specific.
		Although memory allocation routines do not accept a zero sized pointer
		MANAGED_POINTER does by allocating in fact a 1 byte sized pointer for
		this particular case.
	]"
	library: "Free implementation of ELKS library"
	copyright: "Copyright (c) 1986-2006, Eiffel Software and others"
	license: "Eiffel Forum License v2 (see forum.txt)"
	date: "$Date: 2008-05-23 17:24:07 -0700 (Fri, 23 May 2008) $"
	revision: "$Revision: 170 $"

class interface
	MANAGED_POINTER


create 
	make (n: INTEGER_32)
			-- Allocate item with `n' bytes.
		require
			n_non_negative: n >= 0
		ensure
			item_set: item /= default_pointer
			count_set: count = n
			is_shared_set: not is_shared

	make_from_array (data: ARRAY [NATURAL_8])
			-- Allocate item with `data.count' bytes and copy
			-- content of `data' into item.
		require
			data_not_void: data /= Void
		ensure
			item_set: item /= default_pointer
			count_set: count = data.count
			is_shared_set: not is_shared

	make_from_pointer (a_ptr: POINTER; n: INTEGER_32)
			-- Copy `a_count' bytes from `a_ptr' into current.
		require
			a_ptr_not_null: a_ptr /= default_pointer
			n_non_negative: n >= 0
		ensure
			item_set: item /= default_pointer
			count_set: count = n
			is_shared_set: not is_shared

	share_from_pointer (a_ptr: POINTER; n: INTEGER_32)
			-- Use directly `a_ptr' with count `n' to hold current data.
		require
			a_ptr_valid: a_ptr = default_pointer implies n = 0
			n_non_negative: n >= 0
		ensure
			item_set: item = a_ptr
			count_set: count = n
			is_shared_set: is_shared

feature -- Access

	count: INTEGER_32
			-- Number of elements that Current can hold.

	generating_type: STRING_8
			-- Name of current object's generating type
			-- (type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generating_type_not_void: Result /= Void
			generating_type_not_empty: not Result.is_empty

	generator: STRING_8
			-- Name of current object's generating class
			-- (base class of the type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generator_not_void: Result /= Void
			generator_not_empty: not Result.is_empty

	is_shared: BOOLEAN
			-- Is item shared with another memory area?

	item: POINTER
			-- Access to allocated memory.
	
feature -- Comparison

	frozen deep_equal (some: ?ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void
			-- or attached to isomorphic object structures?
			-- (from ANY)
		ensure -- from ANY
			shallow_implies_deep: standard_equal (some, other) implies Result
			both_or_none_void: (some = Void) implies (Result = (other = Void))
			same_type: (Result and (some /= Void)) implies (other /= Void and then some.same_type (other))
			symmetric: Result implies deep_equal (other, some)

	frozen equal (some: ?ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void or attached
			-- to objects considered equal?
			-- (from ANY)
		ensure -- from ANY
			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))

	frozen is_deep_equal (other: MANAGED_POINTER): BOOLEAN
			-- Are `Current' and `other' attached to isomorphic object structures?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			shallow_implies_deep: standard_is_equal (other) implies Result
			same_type: Result implies same_type (other)
			symmetric: Result implies other.is_deep_equal (Current)

	is_equal (other: like Current): BOOLEAN
			-- Is `other' attached to an object considered equal to current object?
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			symmetric: Result implies other.is_equal (Current)
			consistent: standard_is_equal (other) implies Result

	frozen standard_equal (some: ?ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void or attached to
			-- field-by-field identical objects of the same type?
			-- Always uses default object comparison criterion.
			-- (from ANY)
		ensure -- from ANY
			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))

	frozen standard_is_equal (other: MANAGED_POINTER): BOOLEAN
			-- Is `other' attached to an object of the same type
			-- as current object, and field-by-field identical to it?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			same_type: Result implies same_type (other)
			symmetric: Result implies other.standard_is_equal (Current)
	
feature -- Status report

	conforms_to (other: ANY): BOOLEAN
			-- Does type of current object conform to type
			-- of `other' (as per Eiffel: The Language, chapter 13)?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void

	same_type (other: ANY): BOOLEAN
			-- Is type of current object identical to type of `other'?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			definition: Result = (conforms_to (other) and other.conforms_to (Current))
	
feature -- Resizing

	resize (n: INTEGER_32)
			-- Reallocate item to hold `n' bytes.
		require
			n_non_negative: n >= 0
			not_shared: not is_shared
	
feature -- Duplication

	copy (other: like Current)
			-- Update current object using fields of object attached
			-- to `other', so as to yield equal objects. If is_shared
			-- and current is not large enough to hold `other' create
			-- a new pointer area and is_shared is set to `False'.
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		ensure -- from ANY
			is_equal: is_equal (other)
		ensure then
			sharing_status_not_preserved: (old is_shared and not is_shared) implies (other.count > old count)

	frozen deep_copy (other: MANAGED_POINTER)
			-- Effect equivalent to that of:
			--		copy (`other' . deep_twin)
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			deep_equal: deep_equal (Current, other)

	frozen deep_twin: MANAGED_POINTER
			-- New object structure recursively duplicated from Current.
			-- (from ANY)
		ensure -- from ANY
			deep_twin_not_void: Result /= Void
			deep_equal: deep_equal (Current, Result)

	frozen standard_copy (other: MANAGED_POINTER)
			-- Copy every field of `other' onto corresponding field
			-- of current object.
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		ensure -- from ANY
			is_standard_equal: standard_is_equal (other)

	frozen standard_twin: MANAGED_POINTER
			-- New object field-by-field identical to `other'.
			-- Always uses default copying semantics.
			-- (from ANY)
		ensure -- from ANY
			standard_twin_not_void: Result /= Void
			equal: standard_equal (Result, Current)

	frozen twin: MANAGED_POINTER
			-- New object equal to `Current'
			-- twin calls copy; to change copying/twining semantics, redefine copy.
			-- (from ANY)
		ensure -- from ANY
			twin_not_void: Result /= Void
			is_equal: Result.is_equal (Current)
	
feature -- Basic operations

	frozen default: ?MANAGED_POINTER
			-- Default value of object's type
			-- (from ANY)

	frozen default_pointer: POINTER
			-- Default value of type `POINTER'
			-- (Avoid the need to write `p'.default for
			-- some `p' of type `POINTER'.)
			-- (from ANY)

	default_rescue
			-- Process exception for routines with no Rescue clause.
			-- (Default: do nothing.)
			-- (from ANY)

	frozen do_nothing
			-- Execute a null action.
			-- (from ANY)
	
feature -- Access bits size

	boolean_bits: INTEGER_32
			-- Number of bits in a value of type `BOOLEAN'
			-- (from PLATFORM)

	character_32_bits: INTEGER_32 is 32
			-- Number of bits in a value of type `CHARACTER_32'
			-- (from PLATFORM)

	character_8_bits: INTEGER_32 is 8
			-- Number of bits in a value of type `CHARACTER_8'
			-- (from PLATFORM)

	integer_16_bits: INTEGER_32 is 16
			-- Number of bits in a value of type `INTEGER_16'
			-- (from PLATFORM)

	integer_32_bits: INTEGER_32 is 32
			-- Number of bits in a value of type `INTEGER_32'
			-- (from PLATFORM)

	integer_64_bits: INTEGER_32 is 64
			-- Number of bits in a value of type `INTEGER_64'
			-- (from PLATFORM)

	integer_8_bits: INTEGER_32 is 8
			-- Number of bits in a value of type `INTEGER_8'
			-- (from PLATFORM)

	natural_16_bits: INTEGER_32 is 16
			-- Number of bits in a value of type `NATURAL_16'
			-- (from PLATFORM)

	natural_32_bits: INTEGER_32 is 32
			-- Number of bits in a value of type `NATURAL_32'
			-- (from PLATFORM)

	natural_64_bits: INTEGER_32 is 64
			-- Number of bits in a value of type `NATURAL_64'
			-- (from PLATFORM)

	natural_8_bits: INTEGER_32 is 8
			-- Number of bits in a value of type `NATURAL_8'
			-- (from PLATFORM)

	pointer_bits: INTEGER_32
			-- Number of bits in a value of type `POINTER'
			-- (from PLATFORM)

	real_32_bits: INTEGER_32 is 32
			-- Number of bits in a value of type `REAL_32'
			-- (from PLATFORM)

	real_64_bits: INTEGER_32 is 64
			-- Number of bits in a value of type `REAL_64'
			-- (from PLATFORM)
	
feature -- Access bytes size

	boolean_bytes: INTEGER_32
			-- Number of bytes in a value of type `BOOLEAN'
			-- (from PLATFORM)

	character_32_bytes: INTEGER_32 is 4
			-- Number of bytes in a value of type `CHARACTER_32'
			-- (from PLATFORM)

	character_8_bytes: INTEGER_32 is 1
			-- Number of bytes in a value of type `CHARACTER_8'
			-- (from PLATFORM)

	integer_16_bytes: INTEGER_32 is 2
			-- Number of bytes in a value of type `INTEGER_16'
			-- (from PLATFORM)

	integer_32_bytes: INTEGER_32 is 4
			-- Number of bytes in a value of type `INTEGER_32'
			-- (from PLATFORM)

	integer_64_bytes: INTEGER_32 is 8
			-- Number of bytes in a value of type `INTEGER_64'
			-- (from PLATFORM)

	integer_8_bytes: INTEGER_32 is 1
			-- Number of bytes in a value of type `INTEGER_8'
			-- (from PLATFORM)

	natural_16_bytes: INTEGER_32 is 2
			-- Number of bytes in a value of type `NATURAL_16'
			-- (from PLATFORM)

	natural_32_bytes: INTEGER_32 is 4
			-- Number of bytes in a value of type `NATURAL_32'
			-- (from PLATFORM)

	natural_64_bytes: INTEGER_32 is 8
			-- Number of bytes in a value of type `NATURAL_64'
			-- (from PLATFORM)

	natural_8_bytes: INTEGER_32 is 1
			-- Number of bytes in a value of type `NATURAL_8'
			-- (from PLATFORM)

	pointer_bytes: INTEGER_32
			-- Number of bytes in a value of type `POINTER'
			-- (from PLATFORM)

	real_32_bytes: INTEGER_32 is 4
			-- Number of bytes in a value of type `REAL_32'
			-- (from PLATFORM)

	real_64_bytes: INTEGER_32 is 8
			-- Number of bytes in a value of type `REAL_64'
			-- (from PLATFORM)
	
feature -- Access: Big-endian format

	read_integer_16_be (pos: INTEGER_32): INTEGER_16
			-- Read INTEGER_16 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_16_bytes) <= count

	read_integer_32_be (pos: INTEGER_32): INTEGER_32
			-- Read INTEGER at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_32_bytes) <= count

	read_integer_64_be (pos: INTEGER_32): INTEGER_64
			-- Read INTEGER_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_64_bytes) <= count

	read_integer_8_be (pos: INTEGER_32): INTEGER_8
			-- Read INTEGER_8 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_8_bytes) <= count

	read_natural_16_be (pos: INTEGER_32): NATURAL_16
			-- Read NATURAL_16 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_16_bytes) <= count

	read_natural_32_be (pos: INTEGER_32): NATURAL_32
			-- Read NATURAL_32 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_32_bytes) <= count

	read_natural_64_be (pos: INTEGER_32): NATURAL_64
			-- Read NATURAL_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_64_bytes) <= count

	read_natural_8_be (pos: INTEGER_32): NATURAL_8
			-- Read NATURAL_8 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_8_bytes) <= count

	read_real_32_be (pos: INTEGER_32): REAL_32
			-- Read REAL_32 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + real_32_bytes) <= count

	read_real_64_be (pos: INTEGER_32): REAL_64
			-- Read REAL_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + real_64_bytes) <= count
	
feature -- Access: Little-endian format

	read_integer_16_le (pos: INTEGER_32): INTEGER_16
			-- Read INTEGER_16 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_16_bytes) <= count

	read_integer_32_le (pos: INTEGER_32): INTEGER_32
			-- Read INTEGER at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_32_bytes) <= count

	read_integer_64_le (pos: INTEGER_32): INTEGER_64
			-- Read INTEGER_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_64_bytes) <= count

	read_integer_8_le (pos: INTEGER_32): INTEGER_8
			-- Read INTEGER_8 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_8_bytes) <= count

	read_natural_16_le (pos: INTEGER_32): NATURAL_16
			-- Read NATURAL_16 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_16_bytes) <= count

	read_natural_32_le (pos: INTEGER_32): NATURAL_32
			-- Read NATURAL_32 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_32_bytes) <= count

	read_natural_64_le (pos: INTEGER_32): NATURAL_64
			-- Read NATURAL_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_64_bytes) <= count

	read_natural_8_le (pos: INTEGER_32): NATURAL_8
			-- Read NATURAL_8 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_8_bytes) <= count

	read_real_32_le (pos: INTEGER_32): REAL_32
			-- Read REAL_32 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + real_32_bytes) <= count

	read_real_64_le (pos: INTEGER_32): REAL_64
			-- Read REAL_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + real_64_bytes) <= count
	
feature -- Access: Platform specific

	read_array (pos, a_count: INTEGER_32): ARRAY [NATURAL_8]
			-- Read count bytes at position `pos'.
		require
			pos_nonnegative: pos >= 0
			count_positive: a_count > 0
			valid_position: (pos + a_count) <= count
		ensure
			read_array_not_void: Result /= Void
			read_array_valid_count: Result.count = a_count

	read_boolean (pos: INTEGER_32): BOOLEAN
			-- Read BOOLEAN at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + boolean_bytes) <= count

	read_character (pos: INTEGER_32): CHARACTER_8
			-- Read CHARACTER at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + character_8_bytes) <= count

	read_integer_16 (pos: INTEGER_32): INTEGER_16
			-- Read INTEGER_16 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_16_bytes) <= count

	read_integer_32 (pos: INTEGER_32): INTEGER_32
			-- Read INTEGER at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_32_bytes) <= count

	read_integer_64 (pos: INTEGER_32): INTEGER_64
			-- Read INTEGER_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_64_bytes) <= count

	read_integer_8 (pos: INTEGER_32): INTEGER_8
			-- Read INTEGER_8 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_8_bytes) <= count

	read_natural_16 (pos: INTEGER_32): NATURAL_16
			-- Read NATURAL_16 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_16_bytes) <= count

	read_natural_32 (pos: INTEGER_32): NATURAL_32
			-- Read NATURAL_32 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_32_bytes) <= count

	read_natural_64 (pos: INTEGER_32): NATURAL_64
			-- Read NATURAL_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_64_bytes) <= count

	read_natural_8 (pos: INTEGER_32): NATURAL_8
			-- Read NATURAL_8 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_8_bytes) <= count

	read_pointer (pos: INTEGER_32): POINTER
			-- Read POINTER at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + pointer_bytes) <= count

	read_real_32 (pos: INTEGER_32): REAL_32
			-- Read REAL_32 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + real_32_bytes) <= count

	read_real_64 (pos: INTEGER_32): REAL_64
			-- Read REAL_64 at position `pos'.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + real_64_bytes) <= count
	
feature -- Concatenation

	append (other: like Current)
			-- Append `other' at the end of Current.
		require
			not_shared: not is_shared
			other_not_void: other /= Void
	
feature -- Element change: Big-endian format

	put_integer_16_be (i: INTEGER_16; pos: INTEGER_32)
			-- Insert `i' at position `pos' in big-endian format.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_16_bytes) <= count
		ensure
			inserted: i = read_integer_16_be (pos)

	put_integer_32_be (i: INTEGER_32; pos: INTEGER_32)
			-- Insert `i' at position `pos' in big-endian format.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_32_bytes) <= count
		ensure
			inserted: i = read_integer_32_be (pos)

	put_integer_64_be (i: INTEGER_64; pos: INTEGER_32)
			-- Insert `i' at position `pos' in big-endian format.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_64_bytes) <= count
		ensure
			inserted: i = read_integer_64_be (pos)

	put_integer_8_be (i: INTEGER_8; pos: INTEGER_32)
			-- Insert `i' at position `pos' in big-endian format.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + integer_8_bytes) <= count
		ensure
			inserted: i = read_integer_8_be (pos)

	put_natural_16_be (i: NATURAL_16; pos: INTEGER_32)
			-- Insert `i' at position `pos' in big-endian format.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_16_bytes) <= count
		ensure
			inserted: i = read_natural_16_be (pos)

	put_natural_32_be (i: NATURAL_32; pos: INTEGER_32)
			-- Insert `i' at position `pos' in big-endian format.
		require
			pos_nonnegative: pos >= 0
			valid_position: (pos + natural_32_bytes) <= count
		ensure
			inserted: i = read_natural_32_be (pos)

	put_natural_64_be (i: NATURAL_64; pos: INTEGER_32)
			-- Insert `i' at position `pos' in big-endian format.
		require
			pos_nonnegative: pos >=