1with Inline16_Types; use Inline16_Types;
2
3package body Inline16_Gen
4with SPARK_Mode => On
5is
6   procedure Gfw_Image_Read (Data    : out Payload_Type)
7      with SPARK_Mode => Off
8   is
9      Array_Len     : constant NvU32 := Data'Size / NvU8'Size;
10      Array_Max_Idx : constant NvU32 := Array_Len - 1;
11      type Payload_As_Arr_Type is new Arr_NvU8_Idx32(0 .. Array_Max_Idx);
12      Data_As_Array : Payload_As_Arr_Type with Address => Data'Address;
13   begin
14      null;
15   end Gfw_Image_Read;
16end Inline16_Gen;
17