This patch modifies the front end inlining mechanism to ensure that a package
body is always analyzed with the SPARK_Mode of the enclosing context.
------------
-- Source --
------------
-- front_end_inlining.adc
pragma SPARK_Mode (On);
-- front_end_inlining.ads
package Front_End_Inlining is
procedure P;
end Front_End_Inlining;
-- front_end_inlining.adb
with Ada.Text_IO; use Ada.Text_IO;
package body Front_End_Inlining with SPARK_Mode => Off is
subtype Small_Int is Integer range 0 .. 3;
procedure P is
package Small_Int_IO is new Integer_IO (Small_Int);
begin
null;
end P;
end Front_End_Inlining;
-----------------
-- Compilation --
-----------------
$ gcc -c -gnatec=front_end_inlining.adc -gnatN front_end_inlining.adb
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-10-23 Hristian Kirtchev <kirtc...@adacore.com>
* sem_ch12.adb (Inline_Instance_Body): Alphabetize
local variables and constants. Add constants Save_SM and Save_SMP
to capture SPARK_Mode-related attributes. Compile the inlined
body with the SPARK_Mode of the enclosing context.
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 216583)
+++ sem_ch12.adb (working copy)
@@ -4425,25 +4425,31 @@
Gen_Unit : Entity_Id;
Act_Decl : Node_Id)
is
- Vis : Boolean;
- Gen_Comp : constant Entity_Id :=
- Cunit_Entity (Get_Source_Unit (Gen_Unit));
- Curr_Comp : constant Node_Id := Cunit (Current_Sem_Unit);
- Curr_Scope : Entity_Id := Empty;
- Curr_Unit : constant Entity_Id := Cunit_Entity (Current_Sem_Unit);
- Removed : Boolean := False;
- Num_Scopes : Int := 0;
+ Curr_Comp : constant Node_Id := Cunit (Current_Sem_Unit);
+ Curr_Unit : constant Entity_Id := Cunit_Entity (Current_Sem_Unit);
+ Gen_Comp : constant Entity_Id :=
+ Cunit_Entity (Get_Source_Unit (Gen_Unit));
+ Save_SM : constant SPARK_Mode_Type := SPARK_Mode;
+ Save_SMP : constant Node_Id := SPARK_Mode_Pragma;
+ -- Save all SPARK_Mode-related attributes as removing enclosing scopes
+ -- to provide a clean environment for analysis of the inlined body will
+ -- eliminate any previously set SPARK_Mode.
+
Scope_Stack_Depth : constant Int :=
Scope_Stack.Last - Scope_Stack.First + 1;
Use_Clauses : array (1 .. Scope_Stack_Depth) of Node_Id;
Instances : array (1 .. Scope_Stack_Depth) of Entity_Id;
Inner_Scopes : array (1 .. Scope_Stack_Depth) of Entity_Id;
+ Curr_Scope : Entity_Id := Empty;
List : Elist_Id;
Num_Inner : Int := 0;
+ Num_Scopes : Int := 0;
N_Instances : Int := 0;
+ Removed : Boolean := False;
S : Entity_Id;
+ Vis : Boolean;
begin
-- Case of generic unit defined in another unit. We must remove the
@@ -4574,6 +4580,10 @@
pragma Assert (Num_Inner < Num_Scopes);
+ -- The inlined package body must be analyzed with the SPARK_Mode of
+ -- the enclosing context, otherwise the body may cause bogus errors
+ -- if a configuration SPARK_Mode pragma in in effect.
+
Push_Scope (Standard_Standard);
Scope_Stack.Table (Scope_Stack.Last).Is_Active_Stack_Base := True;
Instantiate_Package_Body
@@ -4587,8 +4597,8 @@
Version => Ada_Version,
Version_Pragma => Ada_Version_Pragma,
Warnings => Save_Warnings,
- SPARK_Mode => SPARK_Mode,
- SPARK_Mode_Pragma => SPARK_Mode_Pragma)),
+ SPARK_Mode => Save_SM,
+ SPARK_Mode_Pragma => Save_SMP)),
Inlined_Body => True);
Pop_Scope;
@@ -4692,7 +4702,9 @@
end loop;
end;
- -- If generic unit is in current unit, current context is correct
+ -- If generic unit is in current unit, current context is correct. Note
+ -- that the context is guaranteed to carry the correct SPARK_Mode as no
+ -- enclosing scopes were removed.
else
Instantiate_Package_Body
