with Ada.Unchecked_Conversion;

package UC with SPARK_Mode is

   --  SPARK knows the 'Size and 'Object_Size of scalar types
   type Short_Short is range -128 .. 127;
   type U8 is mod 2 ** 8;

   --  The following representation clauses are not needed, but serve to
   --  illustrate that in the record type declaration below, U7'Size (and not
   --  U7'Object_Size) is used to check the Object_Size of the record type.
   type U7 is mod 2 ** 7
   with Size => 7,
        Object_Size => 8;

   --  Without the packing instruction, the compiler would complain that
   --  objects of type R do not fit into 8 bits.
   type R is record
      A : U7;
      B : Boolean;
   end record
   with Pack, Object_Size => 8;

   --  In both cases, the Object_Size of all involved types is 8
   function To_U8 is new Ada.Unchecked_Conversion (Source => Short_Short, Target => U8);
   function To_R is new Ada.Unchecked_Conversion (Source => U8, Target => R);
end UC;