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