    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.
    	]"
    	legal: "See notice at end of class."
    	status: "See notice at end of class."
    	date: "$Date: 2006-04-19 15:21:41 -0700 (Wed, 19 Apr 2006) $"
    	revision: "$Revision: 58308 $"

    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)

    	generator: STRING_8
    			-- Name of current object's generating class
    			-- (base class of the type of which it is a direct instance)
    			-- (from ANY)

    	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 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))

    	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: like Current): 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.
    			-- If `n' smaller than count, does nothing.
    		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: like Current)
    			-- 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: like Current
    			-- New object structure recursively duplicated from Current.
    			-- (from ANY)
    		ensure -- from ANY
    			deep_equal: deep_equal (Current, Result)

    	frozen standard_copy (other: like Current)
    			-- 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: like Current
    			-- 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: like Current
    			-- 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: like Current
    			-- 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_bits: INTEGER_32
    			-- Number of bits in a value of type `CHARACTER'
    			-- (from PLATFORM)

    	double_bits: INTEGER_32
    			-- Number of bits in a value of type `DOUBLE'
    			-- Was declared in PLATFORM as synonym of real_64_bits.
    			-- (from PLATFORM)

    	integer_16_bits: INTEGER_32
    			-- (from PLATFORM)

    	integer_32_bits: INTEGER_32
    			-- Number of bits in a value of type `INTEGER'
    			-- Was declared in PLATFORM as synonym of integer_bits.
    			-- (from PLATFORM)

    	integer_64_bits: INTEGER_32
    			-- (from PLATFORM)

    	integer_8_bits: INTEGER_32
    			-- (from PLATFORM)

    	integer_bits: INTEGER_32
    			-- Number of bits in a value of type `INTEGER'
    			-- Was declared in PLATFORM as synonym of integer_32_bits.
    			-- (from PLATFORM)

    	natural_16_bits: INTEGER_32
    			-- (from PLATFORM)

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

    	natural_64_bits: INTEGER_32
    			-- (from PLATFORM)

    	natural_8_bits: INTEGER_32
    			-- (from PLATFORM)

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

    	real_32_bits: INTEGER_32
    			-- Number of bits in a value of type `REAL'
    			-- Was declared in PLATFORM as synonym of real_bits.
    			-- (from PLATFORM)

    	real_64_bits: INTEGER_32
    			-- Number of bits in a value of type `DOUBLE'
    			-- Was declared in PLATFORM as synonym of double_bits.
    			-- (from PLATFORM)

    	real_bits: INTEGER_32
    			-- Number of bits in a value of type `REAL'
    			-- Was declared in PLATFORM as synonym of real_32_bits.
    			-- (from PLATFORM)

    feature -- Access bytes size

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

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

    	double_bytes: INTEGER_32
    			-- Number of bytes in a value of type `DOUBLE'
    			-- Was declared in PLATFORM as synonym of real_64_bytes.
    			-- (from PLATFORM)

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

    	integer_32_bytes: INTEGER_32
    			-- Number of bytes in a value of type `INTEGER'
    			-- Was declared in PLATFORM as synonym of integer_bytes.
    			-- (from PLATFORM)

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

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

    	integer_bytes: INTEGER_32
    			-- Number of bytes in a value of type `INTEGER'
    			-- Was declared in PLATFORM as synonym of integer_32_bytes.
    			-- (from PLATFORM)

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

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

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

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

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

    	real_32_bytes: INTEGER_32
    			-- Number of bytes in a value of type `REAL'
    			-- Was declared in PLATFORM as synonym of real_bytes.
    			-- (from PLATFORM)

    	real_64_bytes: INTEGER_32
    			-- Number of bytes in a value of type `DOUBLE'
    			-- Was declared in PLATFORM as synonym of double_bytes.
    			-- (from PLATFORM)

    	real_bytes: INTEGER_32
    			-- Number of bytes in a value of type `REAL'
    			-- Was declared in PLATFORM as synonym of real_32_bytes.
    			-- (from PLATFORM)

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

    feature -- Access min max values

    	maximum_character_code: INTEGER_32
    			-- Largest supported code for CHARACTER values
    			-- (from PLATFORM)
    		ensure -- from PLATFORM
    			meaningful: Result >= 127

    	maximum_integer: INTEGER_32
    			-- Largest supported value of type INTEGER.
    			-- (from PLATFORM)
    		ensure -- from PLATFORM
    			meaningful: Result >= 0

    	minimum_character_code: INTEGER_32
    			-- Smallest supported code for CHARACTER values
    			-- (from PLATFORM)
    		ensure -- from PLATFORM
    			meaningful: Result <= 0

    	minimum_integer: INTEGER_32
    			-- Smallest supported value of type INTEGER
    			-- (from PLATFORM)
    		ensure -- from PLATFORM
    			meaningful: Result <= 0

    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

    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

    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_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_bytes) <= count

    	read_real_64 (pos: INTEGER_32): REAL_64
    			-- Read REAL_64 at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + double_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 >= 0
    			valid_position: (pos + natural_64_bytes) <= count
    		ensure
    			inserted: i = read_natural_64_be (pos)

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

    feature -- Element change: Little-endian format

    	put_integer_16_le (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_le (pos)

    	put_integer_32_le (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_le (pos)

    	put_integer_64_le (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_le (pos)

    	put_integer_8_le (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_le (pos)

    	put_natural_16_le (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_le (pos)

    	put_natural_32_le (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_le (pos)

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

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

    feature -- Element change: Platform specific

    	put_array (data: ARRAY [NATURAL_8]; pos: INTEGER_32)
    			-- Copy content of `data' into item at position `pos'.
    		require
    			data_not_void: data /= Void
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + data.count) <= count
    		ensure
    			inserted: data.is_equal (read_array (pos, data.count))

    	put_boolean (b: BOOLEAN; pos: INTEGER_32)
    			-- Insert `b' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + boolean_bytes) <= count
    		ensure
    			inserted: b = read_boolean (pos)

    	put_character (c: CHARACTER_8; pos: INTEGER_32)
    			-- Insert `' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + character_bytes) <= count
    		ensure
    			inserted: c = read_character (pos)

    	put_integer_16 (i: INTEGER_16; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + integer_16_bytes) <= count
    		ensure
    			inserted: i = read_integer_16 (pos)

    	put_integer_32 (i: INTEGER_32; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + integer_32_bytes) <= count
    		ensure
    			inserted: i = read_integer_32 (pos)

    	put_integer_64 (i: INTEGER_64; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + integer_64_bytes) <= count
    		ensure
    			inserted: i = read_integer_64 (pos)

    	put_integer_8 (i: INTEGER_8; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + integer_8_bytes) <= count
    		ensure
    			inserted: i = read_integer_8 (pos)

    	put_natural_16 (i: NATURAL_16; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + natural_16_bytes) <= count
    		ensure
    			inserted: i = read_natural_16 (pos)

    	put_natural_32 (i: NATURAL_32; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + natural_32_bytes) <= count
    		ensure
    			inserted: i = read_natural_32 (pos)

    	put_natural_64 (i: NATURAL_64; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + natural_64_bytes) <= count
    		ensure
    			inserted: i = read_natural_64 (pos)

    	put_natural_8 (i: NATURAL_8; pos: INTEGER_32)
    			-- Insert `i' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + natural_8_bytes) <= count
    		ensure
    			inserted: i = read_natural_8 (pos)

    	put_pointer (p: POINTER; pos: INTEGER_32)
    			-- Insert `p' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + pointer_bytes) <= count
    		ensure
    			inserted: p = read_pointer (pos)

    	put_real_32 (r: REAL_32; pos: INTEGER_32)
    			-- Insert `r' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + real_bytes) <= count
    		ensure
    			inserted: r = read_real_32 (pos)

    	put_real_64 (d: REAL_64; pos: INTEGER_32)
    			-- Insert `d' at position `pos'.
    		require
    			pos_nonnegative: pos >= 0
    			valid_position: (pos + double_bytes) <= count
    		ensure
    			inserted: d = read_real_64 (pos)

    feature -- Output

    	io: STD_FILES
    			-- Handle to standard file setup
    			-- (from ANY)

    	out: STRING_8
    			-- New string containing terse printable representation
    			-- of current object
    			-- Was declared in ANY as synonym of tagged_out.
    			-- (from ANY)

    	print (some: ANY)
    			-- Write terse external representation of `some'
    			-- on standard output.
    			-- (from ANY)

    	frozen tagged_out: STRING_8
    			-- New string containing terse printable representation
    			-- of current object
    			-- Was declared in ANY as synonym of out.
    			-- (from ANY)

    feature -- Platform

    	is_dotnet: BOOLEAN is False
    			-- Are we targetting .NET?
    			-- (from PLATFORM)

    	is_little_endian: BOOLEAN
    			-- Is current platform a little endian one?
    			-- (from PLATFORM)

    	frozen is_thread_capable: BOOLEAN
    			-- Is current platform capable of multi-threading?
    			-- (from PLATFORM)

    	is_unix: BOOLEAN
    			-- Are we running on a Unix like platform?
    			-- (from PLATFORM)

    	is_vms: BOOLEAN
    			-- Are we running on VMS?
    			-- (from PLATFORM)

    	frozen is_windows: BOOLEAN
    			-- Are we running on Windows platform?
    			-- (from PLATFORM)

    	operating_environment: OPERATING_ENVIRONMENT
    			-- Objects available from the operating system
    			-- (from ANY)

    feature -- Settings

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

    invariant
    	item_not_null: item = default_pointer implies (count = 0 and is_shared)
    	valid_count: count >= 0

    		-- from ANY
    	reflexive_equality: standard_is_equal (Current)
    	reflexive_conformance: conforms_to (Current)

    indexing
    	library: "EiffelBase: Library of reusable components for Eiffel."
    	copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
    	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
    	source: "[
    		Eiffel Software
    		356 Storke Road, Goleta, CA 93117 USA
    		Telephone 805-685-1006, Fax 805-685-6869
    		Website http://www.eiffel.com
    		Customer support http://support.eiffel.com
    	]"

    end -- class MANAGED_POINTER