procedure Decorate (Asp : Node_Id; Prag : Node_Id);
-- Establish linkages between an aspect and its corresponding pragma
- procedure Insert_After_SPARK_Mode
- (Prag : Node_Id;
- Ins_Nod : Node_Id;
- Decls : List_Id);
+ procedure Insert_Pragma
+ (Prag : Node_Id;
+ Is_Instance : Boolean := False);
-- Subsidiary to the analysis of aspects
-- Abstract_State
- -- Ghost
- -- Initializes
- -- Initial_Condition
- -- Refined_State
- -- Insert node Prag before node Ins_Nod. If Ins_Nod is for pragma
- -- SPARK_Mode, then skip SPARK_Mode. Decls is the associated declarative
- -- list where Prag is to reside.
-
- procedure Insert_Pragma (Prag : Node_Id);
- -- Subsidiary to the analysis of aspects
-- Attach_Handler
-- Contract_Cases
-- Depends
+ -- Ghost
-- Global
+ -- Initial_Condition
+ -- Initializes
-- Post
-- Pre
-- Refined_Depends
-- Refined_Global
+ -- Refined_State
-- SPARK_Mode
-- Warnings
-- Insert pragma Prag such that it mimics the placement of a source
- -- pragma of the same kind.
- --
- -- procedure Proc (Formal : ...) with Global => ...;
- --
- -- procedure Proc (Formal : ...);
- -- pragma Global (...);
+ -- pragma of the same kind. Flag Is_Generic should be set when the
+ -- context denotes a generic instance.
--------------
-- Decorate --
Set_Parent (Prag, Asp);
end Decorate;
- -----------------------------
- -- Insert_After_SPARK_Mode --
- -----------------------------
-
- procedure Insert_After_SPARK_Mode
- (Prag : Node_Id;
- Ins_Nod : Node_Id;
- Decls : List_Id)
- is
- Decl : Node_Id := Ins_Nod;
-
- begin
- -- Skip SPARK_Mode
-
- if Present (Decl)
- and then Nkind (Decl) = N_Pragma
- and then Pragma_Name (Decl) = Name_SPARK_Mode
- then
- Decl := Next (Decl);
- end if;
-
- if Present (Decl) then
- Insert_Before (Decl, Prag);
-
- -- Aitem acts as the last declaration
-
- else
- Append_To (Decls, Prag);
- end if;
- end Insert_After_SPARK_Mode;
-
-------------------
-- Insert_Pragma --
-------------------
- procedure Insert_Pragma (Prag : Node_Id) is
+ procedure Insert_Pragma
+ (Prag : Node_Id;
+ Is_Instance : Boolean := False)
+ is
Aux : Node_Id;
Decl : Node_Id;
Decls : List_Id;
Set_Visible_Declarations (Specification (N), Decls);
end if;
- Prepend_To (Decls, Prag);
+ -- The visible declarations of a generic instance have the
+ -- following structure:
+
+ -- <renamings of generic formals>
+ -- <renamings of internally-generated spec and body>
+ -- <first source declaration>
+
+ -- Insert the pragma before the first source declaration by
+ -- skipping the instance "header".
+
+ if Is_Instance then
+ Decl := First (Decls);
+ while Present (Decl) and then not Comes_From_Source (Decl) loop
+ Decl := Next (Decl);
+ end loop;
+
+ -- The instance "header" is followed by at least one source
+ -- declaration.
+
+ if Present (Decl) then
+ Insert_Before (Decl, Prag);
+
+ -- Otherwise the pragma is placed after the instance "header"
+
+ else
+ Append_To (Decls, Prag);
+ end if;
+
+ -- Otherwise this is not a generic instance
+
+ else
+ Prepend_To (Decls, Prag);
+ end if;
-- When the aspect is associated with a protected unit declaration,
-- insert the generated pragma at the top of the visible declarations
when Aspect_Abstract_State => Abstract_State : declare
Context : Node_Id := N;
- Decl : Node_Id;
- Decls : List_Id;
begin
-- When aspect Abstract_State appears on a generic package,
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Abstract_State);
- Decorate (Aspect, Aitem);
-
- Decls := Visible_Declarations (Specification (Context));
- -- In general pragma Abstract_State must be at the top
- -- of the existing visible declarations to emulate its
- -- source counterpart. The only exception to this is a
- -- generic instance in which case the pragma must be
- -- inserted after the association renamings.
-
- if Present (Decls) then
- Decl := First (Decls);
-
- -- The visible declarations of a generic instance have
- -- the following structure:
-
- -- <renamings of generic formals>
- -- <renamings of internally-generated spec and body>
- -- <first source declaration>
-
- -- The pragma must be inserted before the first source
- -- declaration, skip the instance "header".
-
- if Is_Generic_Instance (Defining_Entity (Context)) then
- while Present (Decl)
- and then not Comes_From_Source (Decl)
- loop
- Decl := Next (Decl);
- end loop;
- end if;
-
- -- When aspects Abstract_State, Ghost,
- -- Initial_Condition and Initializes are out of order,
- -- ensure that pragma SPARK_Mode is always at the top
- -- of the declarations to properly enabled/suppress
- -- errors.
-
- Insert_After_SPARK_Mode
- (Prag => Aitem,
- Ins_Nod => Decl,
- Decls => Decls);
-
- -- Otherwise the pragma forms a new declarative list
-
- else
- Set_Visible_Declarations
- (Specification (Context), New_List (Aitem));
- end if;
+ Decorate (Aspect, Aitem);
+ Insert_Pragma
+ (Prag => Aitem,
+ Is_Instance =>
+ Is_Generic_Instance (Defining_Entity (Context)));
else
Error_Msg_NE
-- declarations or after an object, a [generic] subprogram, or
-- a type declaration.
- when Aspect_Ghost => Ghost : declare
- Decls : List_Id;
-
- begin
+ when Aspect_Ghost =>
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Pragma_Name => Name_Ghost);
Decorate (Aspect, Aitem);
-
- -- When the aspect applies to a [generic] package, insert
- -- the pragma at the top of the visible declarations. This
- -- emulates the placement of a source pragma.
-
- if Nkind_In (N, N_Generic_Package_Declaration,
- N_Package_Declaration)
- then
- Decls := Visible_Declarations (Specification (N));
-
- if No (Decls) then
- Decls := New_List;
- Set_Visible_Declarations (N, Decls);
- end if;
-
- -- When aspects Abstract_State, Ghost, Initial_Condition
- -- and Initializes are out of order, ensure that pragma
- -- SPARK_Mode is always at the top of the declarations to
- -- properly enabled/suppress errors.
-
- Insert_After_SPARK_Mode
- (Prag => Aitem,
- Ins_Nod => First (Decls),
- Decls => Decls);
-
- -- Otherwise the context is an object, [generic] subprogram
- -- or type declaration.
-
- else
- Insert_Pragma (Aitem);
- end if;
-
+ Insert_Pragma (Aitem);
goto Continue;
- end Ghost;
-- Global
when Aspect_Initial_Condition => Initial_Condition : declare
Context : Node_Id := N;
- Decls : List_Id;
begin
-- When aspect Initial_Condition appears on a generic
if Nkind_In (Context, N_Generic_Package_Declaration,
N_Package_Declaration)
then
- Decls := Visible_Declarations (Specification (Context));
-
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name =>
Name_Initial_Condition);
- Decorate (Aspect, Aitem);
-
- if No (Decls) then
- Decls := New_List;
- Set_Visible_Declarations (Context, Decls);
- end if;
- -- When aspects Abstract_State, Ghost, Initial_Condition
- -- and Initializes are out of order, ensure that pragma
- -- SPARK_Mode is always at the top of the declarations to
- -- properly enabled/suppress errors.
+ Decorate (Aspect, Aitem);
+ Insert_Pragma
+ (Prag => Aitem,
+ Is_Instance =>
+ Is_Generic_Instance (Defining_Entity (Context)));
- Insert_After_SPARK_Mode
- (Prag => Aitem,
- Ins_Nod => First (Decls),
- Decls => Decls);
+ -- Otherwise the context is illegal
else
Error_Msg_NE
when Aspect_Initializes => Initializes : declare
Context : Node_Id := N;
- Decls : List_Id;
begin
-- When aspect Initializes appears on a generic package,
if Nkind_In (Context, N_Generic_Package_Declaration,
N_Package_Declaration)
then
- Decls := Visible_Declarations (Specification (Context));
-
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Initializes);
- Decorate (Aspect, Aitem);
-
- if No (Decls) then
- Decls := New_List;
- Set_Visible_Declarations (Context, Decls);
- end if;
- -- When aspects Abstract_State, Ghost, Initial_Condition
- -- and Initializes are out of order, ensure that pragma
- -- SPARK_Mode is always at the top of the declarations to
- -- properly enabled/suppress errors.
+ Decorate (Aspect, Aitem);
+ Insert_Pragma
+ (Prag => Aitem,
+ Is_Instance =>
+ Is_Generic_Instance (Defining_Entity (Context)));
- Insert_After_SPARK_Mode
- (Prag => Aitem,
- Ins_Nod => First (Decls),
- Decls => Decls);
+ -- Otherwise the context is illegal
else
Error_Msg_NE
-- Refined_State
- when Aspect_Refined_State => Refined_State : declare
- Decls : List_Id;
+ when Aspect_Refined_State =>
- begin
-- The corresponding pragma for Refined_State is inserted in
-- the declarations of the related package body. This action
-- synchronizes both the source and from-aspect versions of
-- the pragma.
if Nkind (N) = N_Package_Body then
- Decls := Declarations (N);
-
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_State);
- Decorate (Aspect, Aitem);
-
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (N, Decls);
- end if;
- -- Pragma Refined_State must be inserted after pragma
- -- SPARK_Mode in the tree. This ensures that any error
- -- messages dependent on SPARK_Mode will be properly
- -- enabled/suppressed.
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
- Insert_After_SPARK_Mode
- (Prag => Aitem,
- Ins_Nod => First (Decls),
- Decls => Decls);
+ -- Otherwise the context is illegal
else
Error_Msg_NE
end if;
goto Continue;
- end Refined_State;
-- Relative_Deadline
-- is the entity of the related subprogram. Subp_Decl is the declaration
-- of the related subprogram. Sets flag Legal when the pragma is legal.
+ procedure Analyze_If_Present (Id : Pragma_Id);
+ -- Inspect the remainder of the list containing pragma N and look for
+ -- a pragma that matches Id. If found, analyze the pragma.
+
procedure Analyze_Part_Of
(Item_Id : Entity_Id;
State : Node_Id;
-- UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part
-- should be set when Comp comes from a record variant.
- procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id);
- -- Subsidiary routine to the analysis of pragmas Abstract_State,
- -- Initial_Condition and Initializes. Determine whether pragma First
- -- appears before pragma Second. If this is not the case, emit an error.
-
procedure Check_Duplicate_Pragma (E : Entity_Id);
-- Check if a rep item of the same name as the current pragma is already
-- chained as a rep pragma to the given entity. If so give a message
-- Determines if the placement of the current pragma is appropriate
-- for a configuration pragma.
- function Is_Followed_By_Pragma (Prag_Nam : Name_Id) return Boolean;
- -- Determine whether pragma N is followed by another pragma denoted by
- -- its name Prag_Nam. It is assumed that N is a list member.
-
function Is_In_Context_Clause return Boolean;
-- Returns True if pragma appears within the context clause of a unit,
-- and False for any other placement (does not generate any messages).
Subp_Decl := Empty;
Legal := False;
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
GNAT_Pragma;
Check_Arg_Count (1);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
end Analyze_Depends_Global;
+ ------------------------
+ -- Analyze_If_Present --
+ ------------------------
+
+ procedure Analyze_If_Present (Id : Pragma_Id) is
+ Stmt : Node_Id;
+
+ begin
+ pragma Assert (Is_List_Member (N));
+
+ -- Inspect the declarations or statements following pragma N looking
+ -- for another pragma whose Id matches the caller's request. If it is
+ -- available, analyze it.
+
+ Stmt := Next (N);
+ while Present (Stmt) loop
+ if Nkind (Stmt) = N_Pragma and then Get_Pragma_Id (Stmt) = Id then
+ Analyze_Pragma (Stmt);
+ exit;
+
+ -- The first source declaration or statement immediately following
+ -- N ends the region where a pragma may appear.
+
+ elsif Comes_From_Source (Stmt) then
+ exit;
+ end if;
+
+ Next (Stmt);
+ end loop;
+ end Analyze_If_Present;
+
---------------------
-- Analyze_Part_Of --
---------------------
-- Post_Class.
begin
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
-- Change the name of pragmas Pre, Pre_Class, Post and Post_Class to
-- offer uniformity among the various kinds of pre/postconditions by
-- rewriting the pragma identifier. This allows the retrieval of the
Subp_Id := Defining_Entity (Subp_Decl);
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Pre_Post_Condition_In_Decl_Part.
+
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
if Nkind_In (Subp_Decl, N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
+ -- The legality checks of pragmas Precondition and Postcondition
+ -- are affected by the SPARK mode in effect and the volatility of
+ -- the context. Analyze all pragmas in a specific order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
Analyze_Pre_Post_Condition_In_Decl_Part (N);
end if;
-
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Pre_Post_Condition_In_Decl_Part.
-
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
end Analyze_Pre_Post_Condition;
-----------------------------------------
Body_Id := Empty;
Legal := False;
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
GNAT_Pragma;
Check_Arg_Count (1);
Check_No_Identifiers;
end if;
end Check_Component;
- -----------------------------
- -- Check_Declaration_Order --
- -----------------------------
-
- procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id) is
- procedure Check_Aspect_Specification_Order;
- -- Inspect the aspect specifications of the context to determine the
- -- proper order.
-
- --------------------------------------
- -- Check_Aspect_Specification_Order --
- --------------------------------------
-
- procedure Check_Aspect_Specification_Order is
- Asp_First : constant Node_Id := Corresponding_Aspect (First);
- Asp_Second : constant Node_Id := Corresponding_Aspect (Second);
- Asp : Node_Id;
-
- begin
- -- Both aspects must be part of the same aspect specification list
-
- pragma Assert
- (List_Containing (Asp_First) = List_Containing (Asp_Second));
-
- -- Try to reach Second starting from First in a left to right
- -- traversal of the aspect specifications.
-
- Asp := Next (Asp_First);
- while Present (Asp) loop
-
- -- The order is ok, First is followed by Second
-
- if Asp = Asp_Second then
- return;
- end if;
-
- Next (Asp);
- end loop;
-
- -- If we get here, then the aspects are out of order
-
- SPARK_Msg_N ("aspect % cannot come after aspect %", First);
- end Check_Aspect_Specification_Order;
-
- -- Local variables
-
- Stmt : Node_Id;
-
- -- Start of processing for Check_Declaration_Order
-
- begin
- -- Cannot check the order if one of the pragmas is missing
-
- if No (First) or else No (Second) then
- return;
- end if;
-
- -- Set up the error names in case the order is incorrect
-
- Error_Msg_Name_1 := Pragma_Name (First);
- Error_Msg_Name_2 := Pragma_Name (Second);
-
- if From_Aspect_Specification (First) then
-
- -- Both pragmas are actually aspects, check their declaration
- -- order in the associated aspect specification list. Otherwise
- -- First is an aspect and Second a source pragma.
-
- if From_Aspect_Specification (Second) then
- Check_Aspect_Specification_Order;
- end if;
-
- -- Abstract_States is a source pragma
-
- else
- if From_Aspect_Specification (Second) then
- SPARK_Msg_N ("pragma % cannot come after aspect %", First);
-
- -- Both pragmas are source constructs. Try to reach First from
- -- Second by traversing the declarations backwards.
-
- else
- Stmt := Prev (Second);
- while Present (Stmt) loop
-
- -- The order is ok, First is followed by Second
-
- if Stmt = First then
- return;
- end if;
-
- Prev (Stmt);
- end loop;
-
- -- If we get here, then the pragmas are out of order
-
- SPARK_Msg_N ("pragma % cannot come after pragma %", First);
- end if;
- end if;
- end Check_Declaration_Order;
-
----------------------------
-- Check_Duplicate_Pragma --
----------------------------
end if;
end Is_Configuration_Pragma;
- ---------------------------
- -- Is_Followed_By_Pragma --
- ---------------------------
-
- function Is_Followed_By_Pragma (Prag_Nam : Name_Id) return Boolean is
- Stmt : Node_Id;
-
- begin
- pragma Assert (Is_List_Member (N));
-
- -- Inspect the declarations or statements following pragma N looking
- -- for another pragma whose name matches the caller's request.
-
- Stmt := Next (N);
- while Present (Stmt) loop
- if Nkind (Stmt) = N_Pragma
- and then Pragma_Name (Stmt) = Prag_Nam
- then
- return True;
-
- -- The first source declaration or statement immediately following
- -- N ends the region where a pragma may appear.
-
- elsif Comes_From_Source (Stmt) then
- exit;
- end if;
-
- Next (Stmt);
- end loop;
-
- return False;
- end Is_Followed_By_Pragma;
-
--------------------------
-- Is_In_Context_Clause --
--------------------------
Pack_Id := Defining_Entity (Pack_Decl);
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Pack_Id);
+
+ -- The legality checks of pragmas Abstract_State, Initializes, and
+ -- Initial_Condition are affected by the SPARK mode in effect. In
+ -- addition, these three pragmas are subject to an inherent order:
+
+ -- 1) Abstract_State
+ -- 2) Initializes
+ -- 3) Initial_Condition
+
+ -- Analyze all these pragmas in the order outlined above
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
Analyze_Abstract_State (States, Pack_Id);
end if;
- -- Verify the declaration order of pragmas Abstract_State and
- -- Initializes.
-
- Check_Declaration_Order
- (First => N,
- Second => Get_Pragma (Pack_Id, Pragma_Initializes));
-
- -- Chain the pragma on the contract for completeness
-
- Add_Contract_Item (N, Pack_Id);
+ Analyze_If_Present (Pragma_Initializes);
+ Analyze_If_Present (Pragma_Initial_Condition);
end Abstract_State;
------------
-- POLICY_IDENTIFIER ::= Check | Disable | Ignore
-- Note: Check and Ignore are language-defined. Disable is a GNAT
- -- implementation defined addition that results in totally ignoring
+ -- implementation-defined addition that results in totally ignoring
-- the corresponding assertion. If Disable is specified, then the
-- argument of the assertion is not even analyzed. This is useful
-- when the aspect/pragma argument references entities in a with'ed
Obj_Id : Entity_Id;
begin
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
GNAT_Pragma;
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
if Ekind (Obj_Id) = E_Variable then
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_External_Property_In_Decl_Part.
+
+ Add_Contract_Item (N, Obj_Id);
+
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
-- code.
Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
end if;
- -- Chain the pragma on the contract for further processing by
- -- Analyze_External_Property_In_Decl_Part.
-
- Add_Contract_Item (N, Obj_Id);
-
-- Otherwise the external property applies to a constant
else
Obj_Id := Defining_Entity (Obj_Decl);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Obj_Id);
-
-- The object declaration must be a library-level variable with
-- an initialization expression. The expression must depend on
-- a variable, parameter, or another constant_after_elaboration,
return;
end if;
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Obj_Id);
+
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Pragma_As_Ghost (N, Obj_Id);
+
-- Analyze the Boolean expression (if any)
if Present (Arg1) then
Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
end if;
-
- -- Chain the pragma on the contract for completeness
-
- Add_Contract_Item (N, Obj_Id);
end Constant_After_Elaboration;
--------------------
Check_No_Identifiers;
Check_Arg_Count (1);
- -- The pragma is analyzed at the end of the declarative part which
- -- contains the related subprogram. Reset the analyzed flag.
-
- Set_Analyzed (N, False);
-
-- Ensure the proper placement of the pragma. Contract_Cases must
-- be associated with a subprogram declaration or a body that acts
-- as a spec.
Spec_Id := Unique_Defining_Entity (Subp_Decl);
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Contract_Cases_In_Decl_Part.
+
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
if Nkind_In (Subp_Decl, N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
+ -- The legality checks of pragma Contract_Cases are affected by
+ -- the SPARK mode in effect and the volatility of the context.
+ -- Analyze all pragmas in a specific order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
Analyze_Contract_Cases_In_Decl_Part (N);
end if;
-
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Contract_Cases_In_Decl_Part.
-
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
end Contract_Cases;
----------------
-- the annotation must instantiate itself.
when Pragma_Depends => Depends : declare
- Global : Node_Id;
Legal : Boolean;
Spec_Id : Entity_Id;
Subp_Decl : Node_Id;
if Nkind_In (Subp_Decl, N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
- -- Pragmas Global and Depends must be analyzed in a specific
- -- order, as the latter depends on the former. When the two
- -- pragmas appear out of order, their analyis is triggered
- -- by pragma Global.
-
- -- pragma Depends ...;
- -- pragma Global ...; <analyze both pragmas here>
-
- -- Wait until pragma Global is encountered
-
- if Is_Followed_By_Pragma (Name_Global) then
- null;
+ -- The legality checks of pragmas Depends and Global are
+ -- affected by the SPARK mode in effect and the volatility
+ -- of the context. In addition these two pragmas are subject
+ -- to an inherent order:
- -- Otherwise pragma Depends is the last of the pair. Analyze
- -- both pragmas when they appear in order.
+ -- 1) Global
+ -- 2) Depends
- -- pragma Global ...;
- -- pragma Depends ...; <analyze both pragmas here>
+ -- Analyze all these pragmas in the order outlined above
- else
- Global := Get_Pragma (Spec_Id, Pragma_Global);
-
- if Present (Global) then
- Analyze_Global_In_Decl_Part (Global);
- end if;
-
- Analyze_Depends_In_Decl_Part (N);
- end if;
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
+ Analyze_If_Present (Pragma_Global);
+ Analyze_Depends_In_Decl_Part (N);
end if;
end if;
end Depends;
return;
end if;
- Spec_Id := Unique_Defining_Entity (Subp_Decl);
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+
+ -- The legality checks of pragma Extension_Visible are affected
+ -- by the SPARK mode in effect. Analyze all pragmas in specific
+ -- order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
-- Mark the pragma as Ghost if the related subprogram is also
-- Ghost. This also ensures that any expansion performed further
-- below will produce Ghost nodes.
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
Mark_Pragma_As_Ghost (N, Spec_Id);
-- Examine the formals of the related subprogram
Check_Static_Boolean_Expression
(Expression (Get_Argument (N, Spec_Id)));
end if;
-
- -- Chain the pragma on the contract for completeness
-
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
end Extensions_Visible;
--------------
-- the annotation must instantiate itself.
when Pragma_Global => Global : declare
- Depends : Node_Id;
Legal : Boolean;
Spec_Id : Entity_Id;
Subp_Decl : Node_Id;
if Nkind_In (Subp_Decl, N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
- -- Pragmas Global and Depends must be analyzed in a specific
- -- order, as the latter depends on the former. When the two
- -- pragmas appear in order, their analysis is triggered by
- -- pragma Depends.
+ -- The legality checks of pragmas Depends and Global are
+ -- affected by the SPARK mode in effect and the volatility
+ -- of the context. In addition these two pragmas are subject
+ -- to an inherent order:
- -- pragma Global ...;
- -- pragma Depends ...; <analyze both pragmas here>
+ -- 1) Global
+ -- 2) Depends
- -- Wait until pragma Global is encountered
+ -- Analyze all these pragmas in the order outlined above
- if Is_Followed_By_Pragma (Name_Depends) then
- null;
-
- -- Otherwise pragma Global is the last of the pair. Analyze
- -- both pragmas when they are out of order.
-
- -- pragma Depends ...;
- -- pragma Global ...; <analyze both pragmas here>
-
- else
- Analyze_Global_In_Decl_Part (N);
-
- Depends := Get_Pragma (Spec_Id, Pragma_Depends);
-
- if Present (Depends) then
- Analyze_Depends_In_Decl_Part (Depends);
- end if;
- end if;
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
+ Analyze_Global_In_Decl_Part (N);
+ Analyze_If_Present (Pragma_Depends);
end if;
end if;
end Global;
Pack_Id : Entity_Id;
begin
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
return;
end if;
- -- The pragma must be analyzed at the end of the visible
- -- declarations of the related package. Save the pragma for later
- -- (see Analyze_Initial_Condition_In_Decl_Part) by adding it to
- -- the contract of the package.
-
Pack_Id := Defining_Entity (Pack_Decl);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Initial_Condition_In_Decl_Part.
- Mark_Pragma_As_Ghost (N, Pack_Id);
+ Add_Contract_Item (N, Pack_Id);
- -- Verify the declaration order of pragma Initial_Condition with
- -- respect to pragmas Abstract_State and Initializes when SPARK
- -- checks are enabled.
+ -- The legality checks of pragmas Abstract_State, Initializes, and
+ -- Initial_Condition are affected by the SPARK mode in effect. In
+ -- addition, these three pragmas are subject to an inherent order:
- if SPARK_Mode /= Off then
- Check_Declaration_Order
- (First => Get_Pragma (Pack_Id, Pragma_Abstract_State),
- Second => N);
+ -- 1) Abstract_State
+ -- 2) Initializes
+ -- 3) Initial_Condition
- Check_Declaration_Order
- (First => Get_Pragma (Pack_Id, Pragma_Initializes),
- Second => N);
- end if;
+ -- Analyze all these pragmas in the order outlined above
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Initial_Condition_In_Decl_Part.
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Abstract_State);
+ Analyze_If_Present (Pragma_Initializes);
- Add_Contract_Item (N, Pack_Id);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Pragma_As_Ghost (N, Pack_Id);
end Initial_Condition;
------------------------
Pack_Id : Entity_Id;
begin
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
Pack_Id := Defining_Entity (Pack_Decl);
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Initializes_In_Decl_Part.
+
+ Add_Contract_Item (N, Pack_Id);
+
+ -- The legality checks of pragmas Abstract_State, Initializes, and
+ -- Initial_Condition are affected by the SPARK mode in effect. In
+ -- addition, these three pragmas are subject to an inherent order:
+
+ -- 1) Abstract_State
+ -- 2) Initializes
+ -- 3) Initial_Condition
+
+ -- Analyze all these pragmas in the order outlined above
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Abstract_State);
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
Mark_Pragma_As_Ghost (N, Pack_Id);
Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
- -- Verify the declaration order of pragmas Abstract_State and
- -- Initializes when SPARK checks are enabled.
-
- if SPARK_Mode /= Off then
- Check_Declaration_Order
- (First => Get_Pragma (Pack_Id, Pragma_Abstract_State),
- Second => N);
- end if;
-
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Initializes_In_Decl_Part.
-
- Add_Contract_Item (N, Pack_Id);
+ Analyze_If_Present (Pragma_Initial_Condition);
end Initializes;
------------
Legal => Legal);
if Legal then
- State_Id := Entity (State);
+
+ -- Add the pragma to the contract of the item. This aids with
+ -- the detection of a missing but required Part_Of indicator.
+
+ Add_Contract_Item (N, Item_Id);
-- The Part_Of indicator turns an object into a constituent of
-- the encapsulating state.
+ State_Id := Entity (State);
+
if Ekind_In (Item_Id, E_Constant, E_Variable) then
Append_Elmt (Item_Id, Part_Of_Constituents (State_Id));
Set_Encapsulating_State (Item_Id, State_Id);
State_Id => State_Id,
Instance => Stmt);
end if;
-
- -- Add the pragma to the contract of the item. This aids with
- -- the detection of a missing but required Part_Of indicator.
-
- Add_Contract_Item (N, Item_Id);
end if;
end Part_Of;
-- the related generic subprogram body is instantiated.
when Pragma_Refined_Depends => Refined_Depends : declare
- Body_Id : Entity_Id;
- Legal : Boolean;
- Ref_Global : Node_Id;
- Spec_Id : Entity_Id;
+ Body_Id : Entity_Id;
+ Legal : Boolean;
+ Spec_Id : Entity_Id;
begin
Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal);
Add_Contract_Item (N, Body_Id);
- -- Pragmas Refined_Global and Refined_Depends must be analyzed
- -- in a specific order, as the latter depends on the former.
- -- When the two pragmas appear out of order, their analysis is
- -- triggered by pragma Refined_Global.
+ -- The legality checks of pragmas Refined_Depends and
+ -- Refined_Global are affected by the SPARK mode in effect and
+ -- the volatility of the context. In addition these two pragmas
+ -- are subject to an inherent order:
- -- pragma Refined_Depends ...;
- -- pragma Refined_Global ...; <analyze both pragmas here>
+ -- 1) Refined_Global
+ -- 2) Refined_Depends
- -- Wait until pragma Refined_Global is enountered
+ -- Analyze all these pragmas in the order outlined above
- if Is_Followed_By_Pragma (Name_Refined_Global) then
- null;
-
- -- Otherwise pragma Refined_Depends is the last of the pair.
- -- Analyze both pragmas when they appear in order.
-
- -- pragma Refined_Global ...;
- -- pragma Refined_Depends ...; <analyze both pragmas here>
-
- else
- Ref_Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
-
- if Present (Ref_Global) then
- Analyze_Refined_Global_In_Decl_Part (Ref_Global);
- end if;
-
- Analyze_Refined_Depends_In_Decl_Part (N);
- end if;
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
+ Analyze_If_Present (Pragma_Refined_Global);
+ Analyze_Refined_Depends_In_Decl_Part (N);
end if;
end Refined_Depends;
-- the related generic subprogram body is instantiated.
when Pragma_Refined_Global => Refined_Global : declare
- Body_Id : Entity_Id;
- Legal : Boolean;
- Ref_Depends : Node_Id;
- Spec_Id : Entity_Id;
+ Body_Id : Entity_Id;
+ Legal : Boolean;
+ Spec_Id : Entity_Id;
begin
Analyze_Refined_Depends_Global_Post (Spec_Id, Body_Id, Legal);
Add_Contract_Item (N, Body_Id);
- -- Pragmas Refined_Global and Refined_Depends must be analyzed
- -- in a specific order, as the latter depends on the former.
- -- When the two pragmas are in order, their analysis must be
- -- triggered by pragma Refined_Depends.
-
- -- pragma Refined_Global ...;
- -- pragma Refined_Depends ...; <analyze both pragmas here>
-
- -- Wait until pragma Refined_Depends is encountered
+ -- The legality checks of pragmas Refined_Depends and
+ -- Refined_Global are affected by the SPARK mode in effect and
+ -- the volatility of the context. In addition these two pragmas
+ -- are subject to an inherent order:
- if Is_Followed_By_Pragma (Name_Refined_Depends) then
- null;
-
- -- Otherwise pragma Refined_Global is the last of the pair.
- -- Analyze both pragmas when they are out of order.
+ -- 1) Refined_Global
+ -- 2) Refined_Depends
- -- pragma Refined_Depends ...;
- -- pragma Refined_Global ...; <analyze both pragmas here>
+ -- Analyze all these pragmas in the order outlined above
- else
- Analyze_Refined_Global_In_Decl_Part (N);
-
- Ref_Depends := Get_Pragma (Body_Id, Pragma_Refined_Depends);
-
- if Present (Ref_Depends) then
- Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
- end if;
- end if;
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
+ Analyze_Refined_Global_In_Decl_Part (N);
+ Analyze_If_Present (Pragma_Refined_Depends);
end if;
end Refined_Global;
-- body because it cannot benefit from forward references.
if Legal then
+
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Body_Id);
+
+ -- The legality checks of pragma Refined_Post are affected by
+ -- the SPARK mode in effect and the volatility of the context.
+ -- Analyze all pragmas in a specific order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
Analyze_Pre_Post_Condition_In_Decl_Part (N);
-- Currently it is not possible to inline pre/postconditions on
-- a subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
-
- -- Chain the pragma on the contract for completeness
-
- Add_Contract_Item (N, Body_Id);
end if;
end Refined_Post;
Spec_Id : Entity_Id;
begin
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
Spec_Id := Corresponding_Spec (Pack_Decl);
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Refined_State_In_Decl_Part.
+
+ Add_Contract_Item (N, Defining_Entity (Pack_Decl));
+
+ -- The legality checks of pragma Refined_State are affected by the
+ -- SPARK mode in effect. Analyze all pragmas in a specific order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
& "states", N, Spec_Id);
return;
end if;
-
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Refined_State_In_Decl_Part.
-
- Add_Contract_Item (N, Defining_Entity (Pack_Decl));
end Refined_State;
-----------------------
Prag := Contract_Test_Cases (Items);
while Present (Prag) loop
if Pragma_Name (Prag) = Name_Test_Case
+ and then Prag /= N
and then String_Equal
(Name, Get_Name_From_CTC_Pragma (Prag))
then
-- Start of processing for Test_Case
begin
- -- Reset the Analyzed flag because the pragma requires further
- -- analysis.
-
- Set_Analyzed (N, False);
-
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
Check_At_Most_N_Arguments (4);
and then Nkind_In (Context, N_Generic_Package_Declaration,
N_Package_Declaration)
then
- Subp_Id := Defining_Entity (Subp_Decl);
+ null;
-- Otherwise the placement is illegal
return;
end if;
+ Subp_Id := Defining_Entity (Subp_Decl);
+
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Test_Case_In_Decl_Part.
+
+ Add_Contract_Item (N, Subp_Id);
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
if Nkind_In (Subp_Decl, N_Subprogram_Body,
N_Subprogram_Body_Stub)
then
+ -- The legality checks of pragma Test_Case are affected by the
+ -- SPARK mode in effect and the volatility of the context.
+ -- Analyze all pragmas in a specific order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
Analyze_Test_Case_In_Decl_Part (N);
end if;
-
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Test_Case_In_Decl_Part.
-
- Add_Contract_Item (N, Subp_Id);
end Test_Case;
--------------------------
return;
end if;
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Spec_Id);
+
+ -- The legality checks of pragma Volatile_Function are affected by
+ -- the SPARK mode in effect. Analyze all pragmas in a specific
+ -- order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
if Present (Arg1) then
Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
end if;
-
- Add_Contract_Item (N, Spec_Id);
end Volatile_Function;
----------------------
if Is_Entity_Name (State) then
State_Id := Entity_Of (State);
+ -- When the abstract state is undefined, it appears as Any_Id. Do
+ -- not continue with the analysis of the clause.
+
+ if State_Id = Any_Id then
+ return;
+
-- Catch any attempts to re-refine a state or refine a state that
-- is not defined in the package declaration.
- if Ekind (State_Id) = E_Abstract_State then
+ elsif Ekind (State_Id) = E_Abstract_State then
Check_Matching_State;
+
else
SPARK_Msg_NE
("& must denote an abstract state", State, State_Id);
projects / gcc.git / commitdiff