+2019-07-03 Ed Schonberg <schonberg@adacore.com>
+
+ * inline.adb (Process_Formals_In_Aspects): New procedure within
+ Expand_Inlined_Call, to perform a replacement of references to
+ formals that appear in aspect specifications within the body
+ being inlined.
+
2019-07-03 Justin Squirek <squirek@adacore.com>
* sem_ch8.adb (Analyze_Object_Renaming): Add call to search for
-- thunk generated for it. Replace a return statement with an assignment
-- to the target of the call, with appropriate conversions if needed.
+ function Process_Formals_In_Aspects (N : Node_Id)
+ return Traverse_Result;
+ -- Because aspects are linked indirectly to the rest of the tree,
+ -- replacement of formals appearing in aspect specifications must
+ -- be performed in a separate pass, using an instantiation of the
+ -- previous subprogram over aspect specifications reachable from N.
+
function Process_Sloc (Nod : Node_Id) return Traverse_Result;
-- If the call being expanded is that of an internal subprogram, set the
-- sloc of the generated block to that of the call itself, so that the
procedure Replace_Formals is new Traverse_Proc (Process_Formals);
+ --------------------------------
+ -- Process_Formals_In_Aspects --
+ --------------------------------
+
+ function Process_Formals_In_Aspects (N : Node_Id)
+ return Traverse_Result
+ is
+ A : Node_Id;
+ begin
+ if Has_Aspects (N) then
+ A := First (Aspect_Specifications (N));
+ while Present (A) loop
+ Replace_Formals (Expression (A));
+
+ Next (A);
+ end loop;
+ end if;
+ return OK;
+ end Process_Formals_In_Aspects;
+
+ procedure Replace_Formals_In_Aspects is
+ new Traverse_Proc (Process_Formals_In_Aspects);
+
------------------
-- Process_Sloc --
------------------
-- Attach block to tree before analysis and rewriting.
Replace_Formals (Blk);
+ Replace_Formals_In_Aspects (Blk);
Set_Parent (Blk, N);
if GNATprove_Mode then
+2019-07-03 Ed Schonberg <schonberg@adacore.com>
+
+ * gnat.dg/inline16.adb, gnat.dg/inline16_gen.adb,
+ gnat.dg/inline16_gen.ads, gnat.dg/inline16_types.ads: New
+ testcase.
+
2019-07-03 Justin Squirek <squirek@adacore.com>
* gnat.dg/renaming13.adb, gnat.dg/renaming14.adb: New testcases.
--- /dev/null
+-- { dg-do compile }
+-- { dg-options "-gnatN" }
+
+with Inline16_Types; use Inline16_Types;
+with Inline16_Gen;
+
+procedure Inline16 is
+ type TYPE1 is record
+ f1 : NvU32;
+ f2 : NvU32;
+ f3 : NvU32;
+ end record
+ with Size => 96, Object_Size => 96;
+
+ package Gfw_Image_Read_Pkg1 is new Inline16_Gen (Payload_Type => TYPE1);
+ use Gfw_Image_Read_Pkg1;
+ procedure Get_Boot_Block_Info(Status : out Integer)
+ is
+ Ifr_Fixed_Min : TYPE1;
+ begin
+ Gfw_Image_Read(Ifr_Fixed_Min);
+ Status := 13;
+ end Get_Boot_Block_Info;
+begin
+ null;
+end Inline16;
--- /dev/null
+with Inline16_Types; use Inline16_Types;
+
+package body Inline16_Gen
+with SPARK_Mode => On
+is
+ procedure Gfw_Image_Read (Data : out Payload_Type)
+ with SPARK_Mode => Off
+ is
+ Array_Len : constant NvU32 := Data'Size / NvU8'Size;
+ Array_Max_Idx : constant NvU32 := Array_Len - 1;
+ type Payload_As_Arr_Type is new Arr_NvU8_Idx32(0 .. Array_Max_Idx);
+ Data_As_Array : Payload_As_Arr_Type with Address => Data'Address;
+ begin
+ null;
+ end Gfw_Image_Read;
+end Inline16_Gen;
--- /dev/null
+generic
+ type Payload_Type is private;
+package Inline16_Gen
+with SPARK_Mode => On
+is
+ procedure Gfw_Image_Read(Data : out Payload_Type)
+ with Inline_Always;
+
+end Inline16_Gen;
--- /dev/null
+package Inline16_Types with SPARK_Mode is
+
+ type NvU8 is mod 2 ** 8 with Size => 8;
+ type NvU32 is mod 2 ** 32 with Size => 32;
+
+ type Arr_NvU8_Idx32 is array (NvU32 range <>) of NvU8;
+end Inline16_Types;