class interface ICO_HEADER

creation
   make (a_block: F_MEMORY)
      --  Set associated memory block.

      require
         not_void: a_block /= Void

feature(s) from ICO_HEADER
   --  Memory

   make (a_block: F_MEMORY)
      --  Set associated memory block.

      require
         not_void: a_block /= Void

feature(s) from ICO_HEADER
   --  Memory

   set (a_block: F_MEMORY)
      --  Set associated memory block.

      require
         not_void: a_block /= Void

feature(s) from ICO_HEADER
   --  Operation(s)

   is_valid: BOOLEAN
      --  Check layout.


   count: INTEGER
      --  Number of entries.

      require
         valid: is_valid

   entry (n: INTEGER): ICO_ENTRY
      --  Entry block.

      require
         valid: is_valid;
         min: n >= 1;
         max: n <= count
      ensure
         not_void: Result /= Void

   has_bitmap (an_entry: ICO_ENTRY): BOOLEAN
      --  Is there a bitmap pointed to by that entry.

      require
         valid: is_valid;
         not_void: an_entry /= Void

   bitmap (an_entry: ICO_ENTRY): ICO_BITMAP
      --  Bitmap corresponding to an entry.

      require
         valid: is_valid;
         not_void: an_entry /= Void;
         has_bitmap: has_bitmap(an_entry)
      ensure
         not_void: Result /= Void

invariant
   valid_memory: memory /= Void;

end of ICO_HEADER