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