pragma SPARK_Mode(On);
with Interfaces.C;
package body Messages_Wrapper is
   use type Interfaces.C.size_t;  -- needed for visibility in precondition

   function Compute_Fletcher_Checksum
           (Buffer : in Interfaces.C.char_array;
            Size   : in Interfaces.C.size_t) return Interfaces.C.unsigned_short
      with
         Global        => null,
         Import        => True,
         Convention    => C,
         Pre           => Size = Buffer'Length,
         External_Name => "compute_fletcher_checksum";

   function Compute_Checksum (Data : in String) return Checksum_Type is
      -- Copy the Ada string Data into the C string Buffer
      Buffer : Interfaces.C.char_array :=
                 Interfaces.C.To_C (Item       => Data,
                                    Append_Nul => False);
      Result : Interfaces.C.unsigned_short;
   begin
      -- Call the C function whose Ada specification is above
      Result := Compute_Fletcher_Checksum (Buffer => Buffer,
                                           Size   => Buffer'Length);
      -- Return the Result converted to Checksum_Type;
      return Checksum_Type (Result);
   end Compute_Checksum;
end Messages_Wrapper;