This patch allows the uses of aspect/pragma SPARK_Mode in generic units. It
also implements the following rule concerning the interplay between instances
and SPARK_Mode "off":
However, if an instance of a generic unit is enclosed by code where
SPARK_Mode is Off and if any SPARK_Mode specifications occur within the
generic unit, then the corresponding SPARK_Mode specifications occurring
within the instance have no semantic effect.
------------
-- Source --
------------
-- pack_gen_pragmas.ads
generic
package Pack_Gen_Pragmas with SPARK_Mode => On is
Var_1 : Integer := 1
with Volatile, Async_Readers, Effective_Reads;
procedure Force_Body;
private
pragma SPARK_Mode (Off);
Var_2 : Integer := 2
with Volatile, Async_Readers, Effective_Reads;
end Pack_Gen_Pragmas;
-- pack_gen_pragmas.adb
package body Pack_Gen_Pragmas is
procedure Force_Body is begin null; end Force_Body;
end Pack_Gen_Pragmas;
-- pack_pragmas_inst_4.ads
with Pack_Gen_Pragmas;
package Pack_Pragmas_Inst_4 is
package Inst is new Pack_Gen_Pragmas
with SPARK_Mode => Off;
end Pack_Pragmas_Inst_4;
-- pack_pragmas_inst_5.ads
with Pack_Gen_Pragmas;
package Pack_Pragmas_Inst_5 is new Pack_Gen_Pragmas;
pragma SPARK_Mode (On);
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c pack_pragmas_inst_4.ads
$ gcc -c pack_pragmas_inst_5.ads
pack_pragmas_inst_5.ads:3:01: instantiation error at pack_gen_pragmas.ads:3
pack_pragmas_inst_5.ads:3:01: illegal combination of external properties
(SPARK RM 7.1.2(6))
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-08-04 Hristian Kirtchev <kirtc...@adacore.com>
* opt.ads Alphabetize various global flags. New flag
Ignore_Pragma_SPARK_Mode along with a comment on usage.
* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
Pragma SPARK_Mode is now allowed in generic units.
(Analyze_Subprogram_Body_Helper): Do not verify the compatibility
between the SPARK_Mode of a spec and that of a body when inside
a generic.
* sem_ch7.adb (Analyze_Package_Body_Helper): Do not verify the
compatibility between the SPARK_Mode of a spec and that of a
body when inside a generic.
* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration):
Pragma SPARK_Mode is now allowed in generic units.
(Analyze_Package_Instantiation): Save and restore the value of
flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
the governing SPARK_Mode before analyzing the instance.
(Analyze_Subprogram_Instantiation): Save and restore the value
of flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
the governing SPARK_Mode before analyzing the instance.
* sem_ch13.adb (Analyze_Aspect_Specifications): Emulate the
placement of a source pragma when inserting the generated pragma
for aspect SPARK_Mode.
* sem_prag.adb (Analyze_Pragma): Reimplement the handling of
pragma SPARK_Mode to allow for generics and their respective
instantiations.
* sem_util.ads, sem_util.adb (Check_SPARK_Mode_In_Generic): Removed.
(Set_Ignore_Pragma_SPARK_Mode): New routine.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 213553)
+++ sem_ch7.adb (working copy)
@@ -437,11 +437,9 @@
Inspect_Deferred_Constant_Completion (Declarations (N));
end if;
- -- After declarations have been analyzed, the body has been set to have
- -- the final value of SPARK_Mode. Check that the SPARK_Mode for the body
- -- is consistent with the SPARK_Mode for the spec.
+ -- Verify that the SPARK_Mode of the body agrees with that of its spec
- if Present (SPARK_Pragma (Body_Id)) then
+ if not Inside_A_Generic and then Present (SPARK_Pragma (Body_Id)) then
if Present (SPARK_Aux_Pragma (Spec_Id)) then
if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
and then
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 213566)
+++ sem_prag.adb (working copy)
@@ -19116,13 +19116,6 @@
-- pragma SPARK_Mode [(On | Off)];
when Pragma_SPARK_Mode => Do_SPARK_Mode : declare
- Body_Id : Entity_Id;
- Context : Node_Id;
- Mode : Name_Id;
- Mode_Id : SPARK_Mode_Type;
- Spec_Id : Entity_Id;
- Stmt : Node_Id;
-
procedure Check_Pragma_Conformance
(Context_Pragma : Node_Id;
Entity_Pragma : Node_Id;
@@ -19163,7 +19156,7 @@
-- New mode less restrictive than the established mode
if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
- and then Mode_Id = On
+ and then Get_SPARK_Mode_From_Pragma (N) = On
then
Error_Msg_N
("cannot change SPARK_Mode from Off to On", Arg1);
@@ -19176,7 +19169,7 @@
if Present (Entity) then
if Present (Entity_Pragma) then
if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
- and then Mode_Id = On
+ and then Get_SPARK_Mode_From_Pragma (N) = On
then
Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
Error_Msg_Sloc := Sloc (Entity_Pragma);
@@ -19224,9 +19217,36 @@
end if;
end Check_Library_Level_Entity;
+ -- Local variables
+
+ Body_Id : Entity_Id;
+ Context : Node_Id;
+ Inst_Id : Entity_Id;
+ Mode : Name_Id;
+ Mode_Id : SPARK_Mode_Type;
+ Spec_Id : Entity_Id;
+ Stmt : Node_Id;
+
-- Start of processing for Do_SPARK_Mode
begin
+ -- When a SPARK_Mode pragma appears inside an instantiation whose
+ -- enclosing context has SPARK_Mode set to "off", the pragma has
+ -- no semantic effect.
+
+ if Ignore_Pragma_SPARK_Mode then
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
+ return;
+
+ -- Do not analyze the pragma when it appears inside a generic
+ -- because the semantic information of the related context is
+ -- scarce.
+
+ elsif Inside_A_Generic then
+ return;
+ end if;
+
GNAT_Pragma;
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
@@ -19243,15 +19263,15 @@
Mode_Id := Get_SPARK_Mode_Type (Mode);
Context := Parent (N);
- -- Packages and subprograms declared in a generic unit cannot be
- -- subject to the pragma.
+ -- Handle a compilation unit with configuration pragmas
- if Inside_A_Generic then
- Error_Pragma ("incorrect placement of pragma% in a generic");
+ if Nkind (Context) = N_Compilation_Unit_Aux then
+ Context := Parent (Context);
+ end if;
-- The pragma appears in a configuration pragmas file
- elsif No (Context) then
+ if No (Context) then
Check_Valid_Configuration_Pragma;
if Present (SPARK_Mode_Pragma) then
@@ -19263,29 +19283,63 @@
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
- -- When the pragma is placed before the declaration of a unit, it
- -- configures the whole unit.
+ -- The pragma applies to a compilation unit
elsif Nkind (Context) = N_Compilation_Unit then
- Check_Valid_Configuration_Pragma;
- if Nkind (Unit (Context)) in N_Generic_Declaration
- or else (Present (Library_Unit (Context))
- and then Nkind (Unit (Library_Unit (Context))) in
- N_Generic_Declaration)
- then
- Error_Pragma ("incorrect placement of pragma% in a generic");
+ -- The pragma acts as a configuration pragma
+
+ -- pragma SPARK_Mode ...;
+ -- package Pack is ...;
+
+ if List_Containing (N) = Context_Items (Context) then
+ Check_Valid_Configuration_Pragma;
+ SPARK_Mode_Pragma := N;
+ SPARK_Mode := Mode_Id;
+
+ -- The pragma applies to a package instantiation that acts as a
+ -- compilation unit.
+
+ -- package Inst is new Gen ...;
+ -- pragma SPARK_Mode ...;
+
+ elsif Nkind (Unit (Context)) = N_Package_Instantiation then
+ Inst_Id := Defining_Entity (Instance_Spec (Unit (Context)));
+ Check_Library_Level_Entity (Inst_Id);
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Mode_Pragma,
+ Entity_Pragma => Empty,
+ Entity => Empty);
+
+ Set_SPARK_Pragma (Inst_Id, N);
+ Set_SPARK_Pragma_Inherited (Inst_Id, False);
+
+ -- Otherwise the pragma applies to a subprogram instantiation
+ -- that acts as a compilation unit.
+
+ else
+ Spec_Id := Defining_Entity (Unit (Context));
+ Inst_Id := Related_Instance (Spec_Id);
+ Check_Library_Level_Entity (Spec_Id);
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Mode_Pragma,
+ Entity_Pragma => Empty,
+ Entity => Empty);
+
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
+
+ if Present (Inst_Id) then
+ Set_SPARK_Pragma (Inst_Id, N);
+ Set_SPARK_Pragma_Inherited (Inst_Id, False);
+ end if;
end if;
- SPARK_Mode_Pragma := N;
- SPARK_Mode := Mode_Id;
+ -- Otherwise the placement of the pragma within the tree dictates
+ -- its associated construct. Inspect the declarative list where
+ -- the pragma resides to find a potential construct.
- -- The pragma applies to a [library unit] subprogram or package
-
else
- -- Verify the placement of the pragma with respect to package
- -- or subprogram declarations and detect duplicates.
-
Stmt := Prev (N);
while Present (Stmt) loop
@@ -19299,28 +19353,32 @@
raise Pragma_Exit;
end if;
- elsif Nkind (Stmt) in N_Generic_Declaration then
- Error_Pragma
- ("incorrect placement of pragma% on a generic");
+ -- The pragma is associated with a package or subprogram
+ -- instantiation that does not act as a compilation unit.
- -- The pragma applies to a package declaration
+ -- package Inst is new Gen ...;
+ -- pragma SPARK_Mode ...;
- elsif Nkind (Stmt) = N_Package_Declaration then
- Spec_Id := Defining_Entity (Stmt);
- Check_Library_Level_Entity (Spec_Id);
+ elsif Nkind_In (Stmt, N_Function_Instantiation,
+ N_Package_Instantiation,
+ N_Procedure_Instantiation)
+ then
+ Inst_Id := Defining_Entity (Instance_Spec (Stmt));
+ Check_Library_Level_Entity (Inst_Id);
Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Spec_Id),
+ (Context_Pragma => SPARK_Mode_Pragma,
Entity_Pragma => Empty,
Entity => Empty);
- Set_SPARK_Pragma (Spec_Id, N);
- Set_SPARK_Pragma_Inherited (Spec_Id, False);
- Set_SPARK_Aux_Pragma (Spec_Id, N);
- Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+ Set_SPARK_Pragma (Inst_Id, N);
+ Set_SPARK_Pragma_Inherited (Inst_Id, False);
return;
-- The pragma applies to a subprogram declaration
+ -- procedure Proc ...;
+ -- pragma SPARK_Mode ..;
+
elsif Nkind (Stmt) = N_Subprogram_Declaration then
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
@@ -19338,8 +19396,9 @@
elsif not Comes_From_Source (Stmt) then
null;
- -- The pragma does not apply to a legal construct, issue an
- -- error and stop the analysis.
+ -- Otherwise the pragma does not apply to a legal construct
+ -- or it does not appear at the top of a declarative or a
+ -- statement list. Issue an error and stop the analysis.
else
Pragma_Misplaced;
@@ -19349,59 +19408,18 @@
Stmt := Prev (Stmt);
end loop;
- -- Handle all cases where the pragma is actually an aspect and
- -- applies to a library-level package spec, body or subprogram.
+ -- The pragma appears within package declarations
- -- function F ... with SPARK_Mode => ...;
- -- package P with SPARK_Mode => ...;
- -- package body P with SPARK_Mode => ... is
-
- -- The following circuitry simply prepares the proper context
- -- for the general pragma processing mechanism below.
-
- if Nkind (Context) = N_Compilation_Unit_Aux then
- Context := Unit (Parent (Context));
-
- if Nkind_In (Context, N_Package_Declaration,
- N_Subprogram_Declaration)
- then
- Context := Specification (Context);
- end if;
- end if;
-
- -- The pragma is at the top level of a package spec
-
- -- package P is
- -- pragma SPARK_Mode;
-
- -- or
-
- -- package P is
- -- ...
- -- private
- -- pragma SPARK_Mode;
-
if Nkind (Context) = N_Package_Specification then
Spec_Id := Defining_Entity (Context);
+ Check_Library_Level_Entity (Spec_Id);
- -- Pragma applies to private part
+ -- The pragma is at the top of the visible declarations
- if List_Containing (N) = Private_Declarations (Context) then
- Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance
- (Context_Pragma => Empty,
- Entity_Pragma => SPARK_Pragma (Spec_Id),
- Entity => Spec_Id);
- SPARK_Mode_Pragma := N;
- SPARK_Mode := Mode_Id;
+ -- package Pack is
+ -- pragma SPARK_Mode ...;
- Set_SPARK_Aux_Pragma (Spec_Id, N);
- Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
-
- -- Pragma applies to public part
-
- else
- Check_Library_Level_Entity (Spec_Id);
+ if List_Containing (N) = Visible_Declarations (Context) then
Check_Pragma_Conformance
(Context_Pragma => SPARK_Pragma (Spec_Id),
Entity_Pragma => Empty,
@@ -19413,29 +19431,30 @@
Set_SPARK_Pragma_Inherited (Spec_Id, False);
Set_SPARK_Aux_Pragma (Spec_Id, N);
Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
- end if;
- -- The pragma appears as an aspect on a subprogram.
+ -- The pragma is at the top of the private declarations
- -- function F ... with SPARK_Mode => ...;
+ -- package Pack is
+ -- private
+ -- pragma SPARK_Mode ...;
- elsif Nkind_In (Context, N_Function_Specification,
- N_Procedure_Specification)
- then
- Spec_Id := Defining_Entity (Context);
- Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance
- (Context_Pragma => SPARK_Pragma (Spec_Id),
- Entity_Pragma => Empty,
- Entity => Empty);
- Set_SPARK_Pragma (Spec_Id, N);
- Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ else
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity_Pragma => SPARK_Pragma (Spec_Id),
+ Entity => Spec_Id);
+ SPARK_Mode_Pragma := N;
+ SPARK_Mode := Mode_Id;
- -- Pragma is immediately within a package body
+ Set_SPARK_Aux_Pragma (Spec_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
+ end if;
- -- package body P is
- -- pragma SPARK_Mode;
+ -- The pragma appears at the top of package body declarations
+ -- package body Pack is
+ -- pragma SPARK_Mode ...;
+
elsif Nkind (Context) = N_Package_Body then
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Entity (Context);
@@ -19452,11 +19471,35 @@
Set_SPARK_Aux_Pragma (Body_Id, N);
Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
- -- Pragma is immediately within a subprogram body
+ -- The pragma appears at the top of package body statements
- -- function F ... is
+ -- package body Pack is
+ -- begin
-- pragma SPARK_Mode;
+ elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
+ and then Nkind (Parent (Context)) = N_Package_Body
+ then
+ Context := Parent (Context);
+ Spec_Id := Corresponding_Spec (Context);
+ Body_Id := Defining_Entity (Context);
+ Check_Library_Level_Entity (Body_Id);
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity_Pragma => SPARK_Pragma (Body_Id),
+ Entity => Body_Id);
+ SPARK_Mode_Pragma := N;
+ SPARK_Mode := Mode_Id;
+
+ Set_SPARK_Aux_Pragma (Body_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
+
+ -- The pragma appears at the top of subprogram body
+ -- declarations.
+
+ -- procedure Proc ... is
+ -- pragma SPARK_Mode;
+
elsif Nkind (Context) = N_Subprogram_Body then
Spec_Id := Corresponding_Spec (Context);
Context := Specification (Context);
@@ -19471,11 +19514,16 @@
Check_Library_Level_Entity (Body_Id);
+ -- The body is a completion of a previous declaration
+
if Present (Spec_Id) then
Check_Pragma_Conformance
(Context_Pragma => SPARK_Pragma (Body_Id),
Entity_Pragma => SPARK_Pragma (Spec_Id),
Entity => Spec_Id);
+
+ -- The body acts as spec
+
else
Check_Pragma_Conformance
(Context_Pragma => SPARK_Pragma (Body_Id),
@@ -19489,29 +19537,6 @@
Set_SPARK_Pragma (Body_Id, N);
Set_SPARK_Pragma_Inherited (Body_Id, False);
- -- The pragma applies to the statements of a package body
-
- -- package body P is
- -- begin
- -- pragma SPARK_Mode;
-
- elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
- and then Nkind (Parent (Context)) = N_Package_Body
- then
- Context := Parent (Context);
- Spec_Id := Corresponding_Spec (Context);
- Body_Id := Defining_Entity (Context);
- Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance
- (Context_Pragma => Empty,
- Entity_Pragma => SPARK_Pragma (Body_Id),
- Entity => Body_Id);
- SPARK_Mode_Pragma := N;
- SPARK_Mode := Mode_Id;
-
- Set_SPARK_Aux_Pragma (Body_Id, N);
- Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
-
-- The pragma does not apply to a legal construct, issue error
else
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 213547)
+++ sem_ch12.adb (working copy)
@@ -3342,8 +3342,6 @@
Set_Parent_Spec (New_N, Save_Parent);
Rewrite (N, New_N);
- Check_SPARK_Mode_In_Generic (N);
-
-- The aspect specifications are not attached to the tree, and must
-- be copied and attached to the generic copy explicitly.
@@ -3532,6 +3530,9 @@
Needs_Body : Boolean;
Inline_Now : Boolean := False;
+ Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+ -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
Save_Style_Check : constant Boolean := Style_Check;
-- Save style check mode for restore on exit
@@ -3771,6 +3772,12 @@
goto Leave;
else
+ -- If the instance or its context is subject to SPARK_Mode "off",
+ -- set the global flag which signals Analyze_Pragma to ignore all
+ -- SPARK_Mode pragmas within the instance.
+
+ Set_Ignore_Pragma_SPARK_Mode (N);
+
Gen_Decl := Unit_Declaration_Node (Gen_Unit);
-- Initialize renamings map, for error checking, and the list that
@@ -3835,9 +3842,7 @@
Set_Visible_Declarations (Act_Spec, Renaming_List);
end if;
- Act_Decl :=
- Make_Package_Declaration (Loc,
- Specification => Act_Spec);
+ Act_Decl := Make_Package_Declaration (Loc, Specification => Act_Spec);
-- Propagate the aspect specifications from the package declaration
-- template to the instantiated version of the package declaration.
@@ -4277,6 +4282,7 @@
Set_Defining_Identifier (N, Act_Decl_Id);
end if;
+ Ignore_Pragma_SPARK_Mode := Save_IPSM;
Style_Check := Save_Style_Check;
-- Check that if N is an instantiation of System.Dim_Float_IO or
@@ -4311,6 +4317,7 @@
Restore_Env;
end if;
+ Ignore_Pragma_SPARK_Mode := Save_IPSM;
Style_Check := Save_Style_Check;
end Analyze_Package_Instantiation;
@@ -4865,6 +4872,9 @@
-- Local variables
+ Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+ -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
-- to match the visibility of the formal type
@@ -4929,6 +4939,12 @@
Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
else
+ -- If the instance or its context is subject to SPARK_Mode "off",
+ -- set the global flag which signals Analyze_Pragma to ignore all
+ -- SPARK_Mode pragmas within the instance.
+
+ Set_Ignore_Pragma_SPARK_Mode (N);
+
Set_Entity (Gen_Id, Gen_Unit);
Set_Is_Instantiated (Gen_Unit);
@@ -5139,6 +5155,8 @@
Env_Installed := False;
Generic_Renamings.Set_Last (0);
Generic_Renamings_HTable.Reset;
+
+ Ignore_Pragma_SPARK_Mode := Save_IPSM;
end if;
<<Leave>>
@@ -5155,6 +5173,8 @@
if Env_Installed then
Restore_Env;
end if;
+
+ Ignore_Pragma_SPARK_Mode := Save_IPSM;
end Analyze_Subprogram_Instantiation;
-------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 213568)
+++ sem_util.adb (working copy)
@@ -3078,31 +3078,6 @@
end if;
end Check_Result_And_Post_State;
- ---------------------------------
- -- Check_SPARK_Mode_In_Generic --
- ---------------------------------
-
- procedure Check_SPARK_Mode_In_Generic (N : Node_Id) is
- Aspect : Node_Id;
-
- begin
- -- Try to find aspect SPARK_Mode and flag it as illegal
-
- if Has_Aspects (N) then
- Aspect := First (Aspect_Specifications (N));
- while Present (Aspect) loop
- if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
- Error_Msg_Name_1 := Name_SPARK_Mode;
- Error_Msg_N
- ("incorrect placement of aspect % on a generic", Aspect);
- exit;
- end if;
-
- Next (Aspect);
- end loop;
- end if;
- end Check_SPARK_Mode_In_Generic;
-
------------------------------
-- Check_Unprotected_Access --
------------------------------
@@ -16481,6 +16456,128 @@
Set_Entity (N, Val);
end Set_Entity_With_Checks;
+ ----------------------------------
+ -- Set_Ignore_Pragma_SPARK_Mode --
+ ----------------------------------
+
+ procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id) is
+ procedure Set_SPARK_Mode (Expr : Node_Id);
+ -- Set flag Ignore_Pragma_SPARK_Mode based on the argument of aspect or
+ -- pragma SPARK_Mode denoted by Expr.
+
+ --------------------
+ -- Set_SPARK_Mode --
+ --------------------
+
+ procedure Set_SPARK_Mode (Expr : Node_Id) is
+ begin
+ -- When pragma SPARK_Mode with argument "off" applies to an instance,
+ -- all SPARK_Mode pragmas within the instance are ignored.
+
+ if Present (Expr)
+ and then Nkind (Expr) = N_Identifier
+ and then Chars (Expr) = Name_Off
+ then
+ Ignore_Pragma_SPARK_Mode := True;
+ end if;
+ end Set_SPARK_Mode;
+
+ -- Local variables
+
+ Aspects : constant List_Id := Aspect_Specifications (N);
+ Context : constant Node_Id := Parent (N);
+ Args : List_Id;
+ Aspect : Node_Id;
+ Decl : Node_Id;
+
+ -- Start of processing for Set_Ignore_Pragma_SPARK_Mode
+
+ begin
+ -- When the enclosing context of the instance has SPARK_Mode "off", all
+ -- SPARK_Mode pragmas within the instance are ignored. Note that there
+ -- is no point in checking whether the instantiation itself carries
+ -- aspect/pragma SPARK_Mode because it is either illegal ("on") or has
+ -- no effect ("off").
+
+ if SPARK_Mode = Off then
+ Ignore_Pragma_SPARK_Mode := True;
+ return;
+ end if;
+
+ -- Inspect the aspects of the instantiation and locate SPARK_Mode. Note
+ -- that the aspect form of SPARK_Mode precedes a potentially duplicate
+ -- pragma.
+
+ if Present (Aspects) then
+ Aspect := First (Aspects);
+ while Present (Aspect) loop
+ if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
+ Set_SPARK_Mode (Expression (Aspect));
+ return;
+ end if;
+
+ Next (Aspect);
+ end loop;
+ end if;
+
+ -- Peek ahead of the instance and locate pragma SPARK_Mode. Even though
+ -- the pragma is analyzed after the instance, its mode must be known now
+ -- as it governs the legality of SPARK_Mode pragmas within the instance.
+
+ Decl := Empty;
+
+ -- The instance is a compilation unit, the pragma appears on the
+ -- Pragmas_After list.
+
+ if Present (Context)
+ and then Nkind (Context) = N_Compilation_Unit
+ and then Present (Aux_Decls_Node (Context))
+ and then Present (Pragmas_After (Aux_Decls_Node (Context)))
+ then
+ Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
+
+ -- The instance is part of a declarative list, the pragma appears after
+ -- the instance.
+
+ elsif Is_List_Member (N) then
+ Decl := Next (N);
+ end if;
+
+ -- Inspect all declarations following the instance
+
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Pragma then
+ if Get_Pragma_Id (Decl) = Pragma_SPARK_Mode then
+ Args := Pragma_Argument_Associations (Decl);
+
+ -- The pragma argument dictates the mode
+
+ if Present (Args) then
+ Set_SPARK_Mode (Get_Pragma_Arg (First (Args)));
+ end if;
+
+ -- Only the first SPARK_Mode following the instance is
+ -- considered, any extra (illegal) pragmas are ignored.
+
+ exit;
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Decl) then
+ null;
+
+ -- Otherwise a source construct exhaust the range where the pragma
+ -- may appear.
+
+ else
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Set_Ignore_Pragma_SPARK_Mode;
+
------------------------
-- Set_Name_Entity_Id --
------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 213552)
+++ sem_util.ads (working copy)
@@ -327,10 +327,6 @@
-- and post-state. Prag is a [refined] postcondition or a contract-cases
-- pragma. Result_Seen is set when the pragma mentions attribute 'Result.
- procedure Check_SPARK_Mode_In_Generic (N : Node_Id);
- -- Given a generic package [body] or a generic subprogram [body], inspect
- -- the aspect specifications (if any) and flag SPARK_Mode as illegal.
-
procedure Check_Unprotected_Access
(Context : Node_Id;
Expr : Node_Id);
@@ -1841,6 +1837,11 @@
-- If restriction No_Implementation_Identifiers is set, then it checks
-- that the entity is not implementation defined.
+ procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id);
+ -- Determine whether [the enclosing context of] package or subprogram N is
+ -- subject to pragma SPARK_Mode with mode "off". If this is the case, set
+ -- global flag Ignore_Pragma_SPARK_Mode to True.
+
procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id);
pragma Inline (Set_Name_Entity_Id);
-- Sets the Entity_Id value associated with the given name, which is the
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 213537)
+++ sem_ch6.adb (working copy)
@@ -1251,8 +1251,6 @@
end loop;
end;
- Check_SPARK_Mode_In_Generic (N);
-
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
@@ -3743,11 +3741,12 @@
Analyze_Declarations (Declarations (N));
- -- After declarations have been analyzed, the body has been set
- -- its final value of SPARK_Mode. Check that SPARK_Mode for body
- -- is consistent with SPARK_Mode for spec.
+ -- Verify that the SPARK_Mode of the body agrees with that of its spec
- if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
+ if not Inside_A_Generic
+ and then Present (Spec_Id)
+ and then Present (SPARK_Pragma (Body_Id))
+ then
if Present (SPARK_Pragma (Spec_Id)) then
if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
and then
@@ -3757,7 +3756,7 @@
Error_Msg_N ("incorrect application of SPARK_Mode#", N);
Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id));
Error_Msg_NE
- ("\value Off was set for SPARK_Mode on&#", N, Spec_Id);
+ ("\value Off was set for SPARK_Mode on & #", N, Spec_Id);
end if;
elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then
@@ -3767,7 +3766,8 @@
Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
Error_Msg_N ("incorrect application of SPARK_Mode#", N);
Error_Msg_Sloc := Sloc (Spec_Id);
- Error_Msg_NE ("\no value was set for SPARK_Mode on&#", N, Spec_Id);
+ Error_Msg_NE
+ ("\no value was set for SPARK_Mode on & #", N, Spec_Id);
end if;
end if;
Index: opt.ads
===================================================================
--- opt.ads (revision 213536)
+++ opt.ads (working copy)
@@ -648,6 +648,20 @@
-- GNAT
-- Disable generation of ALI file
+ Follow_Links_For_Files : Boolean := False;
+ -- PROJECT MANAGER
+ -- Set to True (-eL) to process the project files in trusted mode. If
+ -- Follow_Links is False, it is assumed that the project doesn't contain
+ -- any file duplicated through symbolic links (although the latter are
+ -- still valid if they point to a file which is outside of the project),
+ -- and that no directory has a name which is a valid source name.
+
+ Follow_Links_For_Dirs : Boolean := False;
+ -- PROJECT MANAGER
+ -- Set to True if directories can be links in this project, and therefore
+ -- additional system calls must be performed to ensure that we always see
+ -- the same full name for each directory.
+
Force_Checking_Of_Elaboration_Flags : Boolean := False;
-- GNATBIND
-- True if binding with forced checking of the elaboration flags
@@ -657,6 +671,13 @@
-- GNATMAKE, GPRMAKE, GPRBUILD
-- Set to force recompilations even when the objects are up-to-date.
+ Front_End_Inlining : Boolean := False;
+ -- GNAT
+ -- Set True to activate inlining by front-end expansion (even on GCC
+ -- targets, where inlining is normally handled by the back end). Set by
+ -- the flag -gnatN (which is now considered obsolescent, since the GCC
+ -- back end can do a better job of inlining than the front end these days.
+
Full_Path_Name_For_Brief_Errors : Boolean := False;
-- PROJECT MANAGER
-- When True, in Brief_Output mode, each error message line
@@ -684,6 +705,10 @@
-- True when switch -gnateG is used. When True, create in a file
-- <source>.prep, if the source is preprocessed.
+ Generate_SCIL : Boolean := False;
+ -- GNAT
+ -- Set True to activate SCIL code generation.
+
Generate_SCO : Boolean := False;
-- GNAT
-- True when switch -fdump-scos (or -gnateS) is used. When True, Source
@@ -728,6 +753,12 @@
-- default value appropriate to the system (in Osint.Initialize), and then
-- reset if a command line switch is used to change the setting.
+ Ignore_Pragma_SPARK_Mode : Boolean := False;
+ -- GNAT
+ -- Set True to ignore the semantics and effects of pragma SPARK_Mode when
+ -- the pragma appears inside an instance whose enclosing context is subject
+ -- to SPARK_Mode "off".
+
Ignore_Rep_Clauses : Boolean := False;
-- GNAT
-- Set True to ignore all representation clauses. Useful when compiling
@@ -798,35 +829,10 @@
-- then elaboration flag checks are to be generated in the binder
-- generated file.
- Generate_SCIL : Boolean := False;
- -- GNAT
- -- Set True to activate SCIL code generation.
-
Invalid_Value_Used : Boolean := False;
-- GNAT
-- Set True if a valid Invalid_Value attribute is encountered
- Follow_Links_For_Files : Boolean := False;
- -- PROJECT MANAGER
- -- Set to True (-eL) to process the project files in trusted mode. If
- -- Follow_Links is False, it is assumed that the project doesn't contain
- -- any file duplicated through symbolic links (although the latter are
- -- still valid if they point to a file which is outside of the project),
- -- and that no directory has a name which is a valid source name.
-
- Follow_Links_For_Dirs : Boolean := False;
- -- PROJECT MANAGER
- -- Set to True if directories can be links in this project, and therefore
- -- additional system calls must be performed to ensure that we always see
- -- the same full name for each directory.
-
- Front_End_Inlining : Boolean := False;
- -- GNAT
- -- Set True to activate inlining by front-end expansion (even on GCC
- -- targets, where inlining is normally handled by the back end). Set by
- -- the flag -gnatN (which is now considered obsolescent, since the GCC
- -- back end can do a better job of inlining than the front end these days.
-
Inline_Processing_Required : Boolean := False;
-- GNAT
-- Set True if inline processing is required. Inline processing is required
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 213552)
+++ sem_ch13.adb (working copy)
@@ -2418,11 +2418,11 @@
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_SPARK_Mode);
- -- When the aspect appears on a package body, insert the
- -- generated pragma at the top of the body declarations to
- -- emulate the behavior of a source pragma.
+ -- When the aspect appears on a package or a subprogram
+ -- body, insert the generated pragma at the top of the body
+ -- declarations to emulate the behavior of a source pragma.
- if Nkind (N) = N_Package_Body then
+ if Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
Decorate (Aspect, Aitem);
Decls := Declarations (N);
@@ -2435,11 +2435,14 @@
Prepend_To (Decls, Aitem);
goto Continue;
- -- When the aspect is associated with package declaration,
- -- insert the generated pragma at the top of the visible
- -- declarations to emulate the behavior of a source pragma.
+ -- When the aspect is associated with a [generic] package
+ -- declaration, insert the generated pragma at the top of
+ -- the visible declarations to emulate the behavior of a
+ -- source pragma.
- elsif Nkind (N) = N_Package_Declaration then
+ elsif Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
Decorate (Aspect, Aitem);
Decls := Visible_Declarations (Specification (N));
