indexing
	description: "Properties of the memory management mechanism. This class may be used as ancestor by classes needing its facilities."

class interface
	MEM_INFO

create 

	make (memory: INTEGER)
			-- Update Current for memory type.
			-- Was declared in MEM_INFO as synonym of make and update.
		ensure

feature -- Initialization

	make (memory: INTEGER)
			-- Update Current for memory type.
			-- Was declared in MEM_INFO as synonym of make and update.
		ensure

			-- Update Current for memory type.
			-- Was declared in MEM_INFO as synonym of make and update.
		ensure
	
feature -- Access

	C_memory: INTEGER is 2
			-- Code for the C memory managed
			-- by the garbage collector
			-- (from MEM_CONST)

	Eiffel_memory: INTEGER is 1
			-- Code for the Eiffel memory managed
			-- by the garbage collector
			-- (from MEM_CONST)

	Full_collector: INTEGER is 0
			-- Statistics for full collections
			-- (from MEM_CONST)

	Incremental_collector: INTEGER is 1
			-- Statistics for incremental collections
			-- (from MEM_CONST)

	Total_memory: INTEGER is 0
			-- Code for all the memory managed
			-- by the garbage collector
			-- (from MEM_CONST)

	type: INTEGER
			-- Memory type (Total, Eiffel, C)
	
feature -- Measurement

	free: INTEGER
			-- Number of bytes still free for type
			-- before last call to update
		ensure
			computed: Result = total - used - overhead

	overhead: INTEGER
			-- Number of bytes used by memory management
			-- scheme for type before last call to update

	total: INTEGER
			-- Total number of bytes allocated for type
			-- before last call to update

	used: INTEGER
			-- Number of bytes used for type
			-- before last call to update
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	consistent_memory: total = free + used + overhead;

end -- class MEM_INFO