class interface F_MEMORY

creation
   make (sz: INTEGER)
      --  Create a memory block of sz size, in bytes.

      require
         positive: sz > 0
      ensure
         done: size = sz

feature(s) from MEMORY
   --  Removal :

   dispose
      --  Free memory.


   full_collect
      --  Force a full collection cycle if garbage collection is
      --  enabled; do nothing otherwise.


feature(s) from F_MEMORY
   --  Finalisation

   close
      --  Close memory object (free memory, handled 
      --  by finalisation if omitted).

      require
         alive: size /= 0
      ensure
         done: size = 0

feature(s) from F_MEMORY
   --  Copy

   copy (other: like Current)
      --  Copy other memory block. Other MUST be the same size 
      --  as Current.

      require
         other_not_void: other /= Void
      ensure
         size: size = other.size;
         is_equal: is_equal(other)

   is_equal (other: like Current): BOOLEAN
      --  Is other attached to an object considered equal to 
      --  current object ?

      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

feature(s) from F_MEMORY
   is_writable: BOOLEAN
      --  Can this block be written to?


feature(s) from F_MEMORY
   --  Size/Index

   size: INTEGER
      --  Size of the memory block.


   offset (offs: INTEGER): INTEGER
      --  Convert an offset to a position.

      require
         valid: offs >= 0 and offs < size
      ensure
         done: Result = offs + 1

   is_index (idx: INTEGER): BOOLEAN
      --  Is idx a valid index?

      ensure
         done: Result = (idx >= 1 and idx <= size)

feature(s) from F_MEMORY
   byte (index: INTEGER): INTEGER
      --  Get the value of the byte at index position.

      require
         valid: is_index(index)
      ensure
         valid_byte: Result >= 0 and Result <= 255

   set_byte (index, value: INTEGER)
      --  Set the value of the byte at current position.

      require
         writable: is_writable;
         valid_index: is_index(index);
         valid_byte: value >= 0 and value <= 255
      ensure
         done: byte(index) = value

feature(s) from F_MEMORY
   --  Subset

   subset (start, length: INTEGER): F_MEMORY
      --  Get a copy of a subset of the memory 
      --  block.

      require
         valid: is_index(start);
         length: length > 0;
         bounds: is_index(start + length - 1)
      ensure
         is_copy: Result /= Void

   set_subset (idx: INTEGER; sub_set: F_MEMORY)
      --  Set a block of memory inside this one.

      require
         writable: is_writable;
         valid: is_index(idx);
         length: is_index(idx + sub_set.size - 1)
      ensure
         done: subset(idx,sub_set.size).is_equal(sub_set)

feature(s) from F_MEMORY
   --  Get unsigned 16-bit WORDs.

   unsigned_word (idx: INTEGER): INTEGER
      --  Convert this memory block to integer, as a 
      --  machine-order WORD

      require
         valid: is_index(idx);
         word: is_index(idx + 1)
      ensure
         done: Result < Max_unsigned_word and Result >= 0

   little_unsigned_word (idx: INTEGER): INTEGER
      --  Like get_word, little endian order.

      require
         valid: is_index(idx);
         word: is_index(idx + 1)
      ensure
         done: Result < Max_unsigned_word and Result >= 0

   big_unsigned_word (idx: INTEGER): INTEGER
      --  Like get_word, big endian order.

      require
         valid: is_index(idx);
         word: is_index(idx + 1)
      ensure
         done: Result < Max_unsigned_word and Result >= 0

feature(s) from F_MEMORY
   --  Set unsigned 16-bit WORDs.

   set_unsigned_word (idx: INTEGER; value: INTEGER)
      require
         writable: is_writable;
         valid: is_index(idx) and is_index(idx + 1);
         value: value < Max_unsigned_word and value >= 0
      ensure
         done: value = unsigned_word(idx)

   set_little_unsigned_word (idx: INTEGER; value: INTEGER)
      require
         writable: is_writable;
         valid: is_index(idx) and is_index(idx + 1);
         value: value < Max_unsigned_word and value >= 0
      ensure
         done: value = little_unsigned_word(idx)

   set_big_unsigned_word (idx: INTEGER; value: INTEGER)
      require
         writable: is_writable;
         valid: is_index(idx) and is_index(idx + 1);
         value: value < Max_unsigned_word and value >= 0
      ensure
         done: value = big_unsigned_word(idx)

feature(s) from F_MEMORY
   --  Signed WORD (16 bits, 2 bytes).

   word (idx: INTEGER): INTEGER
      --  Convert the two bytes at idx to integer as 
      --  a machine unsigned_word.

      require
         valid: is_index(idx);
         word: is_index(idx + 1)
      ensure
         done: Result < Max_word and Result > - Max_word

   little_word (idx: INTEGER): INTEGER
      --  Little endian signed word.

      require
         valid: is_index(idx);
         word: is_index(idx + 1)
      ensure
         done: Result < Max_word and Result > - Max_word

   big_word (idx: INTEGER): INTEGER
      --  Big endian signed word.

      require
         valid: is_index(idx);
         word: is_index(idx + 1)
      ensure
         done: Result < Max_word and Result > - Max_word

feature(s) from F_MEMORY
   --  Set 16-bit unsigned WORD.

   set_word (idx: INTEGER; value: INTEGER)
      require
         writable: is_writable;
         valid: is_index(idx) and is_index(idx + 1);
         value: value < Max_word and value > - Max_word
      ensure
         done: value = word(idx)

   set_little_word (idx: INTEGER; value: INTEGER)
      require
         writable: is_writable;
         valid: is_index(idx) and is_index(idx + 1);
         value: value < Max_word and value > - Max_word
      ensure
         done: value = little_word(idx)

   set_big_word (idx: INTEGER; value: INTEGER)
      require
         writable: is_writable;
         valid: is_index(idx) and is_index(idx + 1);
         value: value < Max_word and value > - Max_word
      ensure
         done: value = big_word(idx)

feature(s) from F_MEMORY
   --  DWORD

   double_word (idx: INTEGER): INTEGER
      --  Get (signed) 32-bit integer starting atidx, 
      --  machine byte order.

      require
         valid: is_index(idx);
         dword: is_index(idx + 3)

   little_double_word (idx: INTEGER): INTEGER
      --  Get little endian (signed) 32-bit integer.

      require
         valid: is_index(idx);
         dword: is_index(idx + 3)

   big_double_word (idx: INTEGER): INTEGER
      --  Get big endian (signed) 32-bit integer.

      require
         valid: is_index(idx);
         dword: is_index(idx + 3)

feature(s) from F_MEMORY
   --  Set DWORD

   set_double_word (idx: INTEGER; value: INTEGER)
      --  Set (signed) 32-bit integer at idx.
      --  Machine byte order.

      require
         writable: is_writable;
         valid: is_index(idx);
         dword: is_index(idx + 3)
      ensure
         done: double_word(idx) = value

   set_little_double_word (idx: INTEGER; value: INTEGER)
      --  Set little endian (signed) 32-bit integer at idx.

      require
         writable: is_writable;
         valid: is_index(idx);
         dword: is_index(idx + 3)
      ensure
         done: little_double_word(idx) = value

   set_big_double_word (idx: INTEGER; value: INTEGER)
      --  Set big endian (signed) 32-bit integer at idx.

      require
         writable: is_writable;
         valid: is_index(idx);
         dword: is_index(idx + 3)
      ensure
         done: big_double_word(idx) = value

feature(s) from F_MEMORY
   --  C String

   cstring (idx, length: INTEGER): STRING
      --  Read system dependent string, character width is 
      --  the same as the system's CHARACTER. Scanning 
      --  terminates at first 0 or length whichever happens 
      --  first. NOTE: length is in bytes.

      require
         valid_index: is_index(idx);
         valid_length: length > 0;
         valid_end: is_index(idx + length - 1)

   byte_cstring (idx, length: INTEGER): STRING
      --  Read string with 8-bit characters, up to 
      --  a zero byte or length.

      require
         valid_index: is_index(idx);
         valid_length: length > 0;
         valid_end: is_index(idx + length - 1)

   set_cstring (idx, length: INTEGER; str: STRING)
      require
         writable: is_writable;
         valid_index: is_index(idx);
         valid_length: length > 0;
         valid_end: is_index(idx + length - 1);
         valid_str: str /= Void
      ensure
         done: cstring(idx,length).is_equal(str)

   set_byte_cstring (idx, length: INTEGER; str: STRING)
      --  Write string with one byte per characters, 
      --  bytes between str.count + 1 and length are 
      --  set to zero.

      require
         writable: is_writable;
         valid_index: is_index(idx);
         valid_length: length > 0;
         valid_end: is_index(idx + length - 1);
         valid_str: str /= Void
      ensure
         done: byte_cstring(idx,length).is_equal(str)

feature(s) from F_MEMORY
   --  Bit operations

   bit_and (a, b: INTEGER): INTEGER
      --  Bitwise AND (like C '&')


   bit_or (a, b: INTEGER): INTEGER
      --  Bitwise OR (like C '|')


   bit_xor (a, b: INTEGER): INTEGER
      --  Bitwise XOR (like C '^')


feature(s) from F_MEMORY
   --  Constants

   Max_word: INTEGER
      --  2^15


   Max_unsigned_word: INTEGER
      --  2^16


invariant
   implementation:  -- ? Integer_bits >= 32

end of F_MEMORY