expanded class interface POINTER
   --
   -- References to objects meant to be exchanged with non-Eiffel software.
   --
   -- Note : An Eiffel POINTER is mapped as C type "void *" or as
   -- Java "java.lang.Object" type.
   --

feature(s) from HASHABLE   hash_code: INTEGER
      -- The hash-code value of Current.

      ensure
         good_hash_value: Result >= 0

feature(s) from POINTER   is_null: BOOLEAN
      -- Is the external POINTER a NULL pointer ?


   is_not_null: BOOLEAN
      -- Is the external POINTER a non-NULL pointer ?


   to_string: STRING

   append_in (buffer: STRING)
      -- Append on str a viewable version of Current.


   out_in_tagged_out_memory
      -- Append terse printable represention of current object
      -- in tagged_out_memory.

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

   fill_tagged_out_memory
      -- Append terse printable represention of current object
      -- in tagged_out_memory.


   infix "+" (offset: INTEGER): POINTER
      -- Current moved by an offset of offset bytes.


   to_any: ANY
      -- Dangerous forced conversion. This function assume that Current 
      -- is really a reference to some Eiffel allocated object.


feature(s) from POINTER
   -- For compatibility with the obsolete INTEGER_REF style:

   item: POINTER

   set_item (value: like item)
      ensure
         item = value



end of expanded POINTER