-- | | |
-- | +--> Process_Variable_Assignment |
-- | | |
- -- | +--> Process_Variable_Reference |
+ -- | +--> Process_Variable_Read |
-- | |
-- +------------------------- Processing phase -------------------------+
-- message, otherwise it emits an error. If flag In_SPARK is set, then
-- string " in SPARK" is added to the end of the message.
- procedure Ensure_Dynamic_Prior_Elaboration
- (N : Node_Id;
- Unit_Id : Entity_Id;
- Prag_Nam : Name_Id);
- -- Guarantee the elaboration of unit Unit_Id with respect to the main unit
- -- by suggesting the use of Elaborate[_All] with name Prag_Nam. N denotes
- -- the related scenario.
-
procedure Ensure_Prior_Elaboration
(N : Node_Id;
Unit_Id : Entity_Id;
-- N denotes the related scenario. Flag In_Task_Body should be set when the
-- need for elaboration is initiated from a task body.
- procedure Ensure_Static_Prior_Elaboration
+ procedure Ensure_Prior_Elaboration_Dynamic
+ (N : Node_Id;
+ Unit_Id : Entity_Id;
+ Prag_Nam : Name_Id);
+ -- Guarantee the elaboration of unit Unit_Id with respect to the main unit
+ -- by suggesting the use of Elaborate[_All] with name Prag_Nam. N denotes
+ -- the related scenario.
+
+ procedure Ensure_Prior_Elaboration_Static
(N : Node_Id;
Unit_Id : Entity_Id;
Prag_Nam : Name_Id);
(Call : Node_Id;
Target_Id : out Entity_Id;
Attrs : out Call_Attributes);
+ pragma Inline (Extract_Call_Attributes);
-- Obtain attributes Attrs associated with call Call. Target_Id is the
-- entity of the call target.
Inst_Id : out Entity_Id;
Gen_Id : out Entity_Id;
Attrs : out Instantiation_Attributes);
+ pragma Inline (Extract_Instantiation_Attributes);
-- Obtain attributes Attrs associated with expanded instantiation Exp_Inst.
-- Inst is the instantiation. Inst_Id is the entity of the instance. Gen_Id
-- is the entity of the generic unit being instantiated.
procedure Extract_Task_Attributes
(Typ : Entity_Id;
Attrs : out Task_Attributes);
+ pragma Inline (Extract_Task_Attributes);
-- Obtain attributes Attrs associated with task type Typ
procedure Extract_Variable_Reference_Attributes
(Ref : Node_Id;
Var_Id : out Entity_Id;
Attrs : out Variable_Attributes);
- -- Obtain attributes Attrs associated with reference Ref which mentions
+ pragma Inline (Extract_Variable_Reference_Attributes);
+ -- Obtain attributes Attrs associated with reference Ref that mentions
-- variable Var_Id.
function Find_Code_Unit (N : Node_Or_Entity_Id) return Entity_Id;
function In_External_Instance
(N : Node_Id;
Target_Decl : Node_Id) return Boolean;
+ pragma Inline (In_External_Instance);
-- Determine whether a target desctibed by its declaration Target_Decl
-- resides in a package instance which is external to scenario N.
In_SPARK : Boolean);
-- Output information concerning call Call which invokes target Target_Id.
-- If flag Info_Msg is set, the routine emits an information message,
- -- otherwise it emits an error. If flag In_SPARK is set, then string " in
- -- SPARK" is added to the end of the message.
+ -- otherwise it emits an error. If flag In_SPARK is set, then the string
+ -- " in SPARK" is added to the end of the message.
procedure Info_Instantiation
(Inst : Node_Id;
Gen_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
+ pragma Inline (Info_Instantiation);
-- Output information concerning instantiation Inst which instantiates
-- generic unit Gen_Id. If flag Info_Msg is set, the routine emits an
-- information message, otherwise it emits an error. If flag In_SPARK
-- is set, then string " in SPARK" is added to the end of the message.
- procedure Info_Variable_Reference
+ procedure Info_Variable_Read
(Ref : Node_Id;
Var_Id : Entity_Id;
Info_Msg : Boolean;
In_SPARK : Boolean);
- -- Output information concerning reference Ref which mentions variable
- -- Var_Id. If flag Info_Msg is set, the routine emits an information
- -- message, otherwise it emits an error. If flag In_SPARK is set, then
- -- string " in SPARK" is added to the end of the message.
+ pragma Inline (Info_Variable_Read);
+ -- Output information concerning reference Ref which reads variable Var_Id.
+ -- If flag Info_Msg is set, the routine emits an information message,
+ -- otherwise it emits an error. If flag In_SPARK is set, then string " in
+ -- SPARK" is added to the end of the message.
function Insertion_Node (N : Node_Id; Ins_Nod : Node_Id) return Node_Id;
pragma Inline (Insertion_Node);
(N : Node_Id;
Target_Decl : Node_Id;
Target_Body : Node_Id) return Boolean;
+ pragma Inline (Is_Guaranteed_ABE);
-- Determine whether scenario N with a target described by its initial
-- declaration Target_Decl and body Target_Decl results in a guaranteed
-- ABE.
-- Determine whether arbitrary entity Id denotes internally generated
-- routine Initial_Condition.
+ function Is_Initialized (Obj_Decl : Node_Id) return Boolean;
+ pragma Inline (Is_Initialized);
+ -- Determine whether object declaration Obj_Decl is initialized
+
function Is_Invariant_Proc (Id : Entity_Id) return Boolean;
pragma Inline (Is_Invariant_Proc);
-- Determine whether arbitrary entity Id denotes an invariant procedure
-- Determine whether arbitrary node N denotes a suitable assignment for ABE
-- processing.
- function Is_Suitable_Variable_Reference (N : Node_Id) return Boolean;
- pragma Inline (Is_Suitable_Variable_Reference);
- -- Determine whether arbitrary node N is a suitable reference to a variable
- -- for ABE processing.
+ function Is_Suitable_Variable_Read (N : Node_Id) return Boolean;
+ pragma Inline (Is_Suitable_Variable_Read);
+ -- Determine whether arbitrary node N is a suitable variable read for ABE
+ -- processing.
function Is_Task_Entry (Id : Entity_Id) return Boolean;
pragma Inline (Is_Task_Entry);
Call_Attrs : Call_Attributes;
Target_Id : Entity_Id;
In_Task_Body : Boolean);
- -- Top level dispatcher for processing of calls. Perform ABE checks and
+ -- Top-level dispatcher for processing of calls. Perform ABE checks and
-- diagnostics for call Call which invokes target Target_Id. Call_Attrs
-- are the attributes of the call. Flag In_Task_Body should be set when
-- the processing is initiated from a task body.
-- should be set when the processing is initiated from a task body.
procedure Process_Variable_Assignment (Asmt : Node_Id);
- -- Perform ABE checks and diagnostics for assignment statement Asmt
-
- procedure Process_Variable_Reference (Ref : Node_Id);
- -- Perform ABE checks and diagnostics for variable reference Ref
+ -- Top level dispatcher for processing of variable assignments. Perform ABE
+ -- checks and diagnostics for assignment statement Asmt.
+
+ procedure Process_Variable_Assignment_Ada
+ (Asmt : Node_Id;
+ Var_Id : Entity_Id);
+ -- Perform ABE checks and diagnostics for assignment statement Asmt that
+ -- updates the value of variable Var_Id using the Ada rules.
+
+ procedure Process_Variable_Assignment_SPARK
+ (Asmt : Node_Id;
+ Var_Id : Entity_Id);
+ -- Perform ABE checks and diagnostics for assignment statement Asmt that
+ -- updates the value of variable Var_Id using the SPARK rules.
+
+ procedure Process_Variable_Read (Ref : Node_Id);
+ -- Perform ABE checks and diagnostics for reference Ref that reads a
+ -- variable.
procedure Push_Active_Scenario (N : Node_Id);
pragma Inline (Push_Active_Scenario);
-- should be set when the traversal is initiated from a task body.
procedure Update_Elaboration_Scenario (New_N : Node_Id; Old_N : Node_Id);
+ pragma Inline (Update_Elaboration_Scenario);
-- Update all relevant internal data structures when scenario Old_N is
-- transformed into scenario New_N by Atree.Rewrite.
return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
end Elaboration_Context_Hash;
- --------------------------------------
- -- Ensure_Dynamic_Prior_Elaboration --
- --------------------------------------
-
- procedure Ensure_Dynamic_Prior_Elaboration
- (N : Node_Id;
- Unit_Id : Entity_Id;
- Prag_Nam : Name_Id)
- is
- procedure Info_Missing_Pragma;
- pragma Inline (Info_Missing_Pragma);
- -- Output information concerning missing Elaborate or Elaborate_All
- -- pragma with name Prag_Nam for scenario N which ensures the prior
- -- elaboration of Unit_Id.
-
- -------------------------
- -- Info_Missing_Pragma --
- -------------------------
-
- procedure Info_Missing_Pragma is
- begin
- -- Internal units are ignored as they cause unnecessary noise
-
- if not In_Internal_Unit (Unit_Id) then
-
- -- The name of the unit subjected to the elaboration pragma is
- -- fully qualified to improve the clarity of the info message.
-
- Error_Msg_Name_1 := Prag_Nam;
- Error_Msg_Qual_Level := Nat'Last;
-
- Error_Msg_NE ("info: missing pragma % for unit &", N, Unit_Id);
- Error_Msg_Qual_Level := 0;
- end if;
- end Info_Missing_Pragma;
-
- -- Local variables
-
- Elab_Attrs : Elaboration_Attributes;
- Level : Enclosing_Level_Kind;
-
- -- Start of processing for Ensure_Dynamic_Prior_Elaboration
-
- begin
- Elab_Attrs := Elaboration_Context.Get (Unit_Id);
-
- -- Nothing to do when the unit is guaranteed prior elaboration by means
- -- of a source Elaborate[_All] pragma.
-
- if Present (Elab_Attrs.Source_Pragma) then
- return;
- end if;
-
- -- Output extra information on a missing Elaborate[_All] pragma when
- -- switch -gnatel (info messages on implicit Elaborate[_All] pragmas
- -- is in effect.
-
- if Elab_Info_Messages then
-
- -- Performance note: parent traversal
-
- Level := Find_Enclosing_Level (N);
-
- -- Declaration level scenario
-
- if (Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N))
- and then Level = Declaration_Level
- then
- null;
-
- -- Library level scenario
-
- elsif Level in Library_Level then
- null;
-
- -- Instantiation library level scenario
-
- elsif Level = Instantiation then
- null;
-
- -- Otherwise the scenario does not appear at the proper level and
- -- cannot possibly act as a top level scenario.
-
- else
- return;
- end if;
-
- Info_Missing_Pragma;
- end if;
- end Ensure_Dynamic_Prior_Elaboration;
-
------------------------------
-- Ensure_Prior_Elaboration --
------------------------------
-- effect.
elsif Dynamic_Elaboration_Checks then
- Ensure_Dynamic_Prior_Elaboration
+ Ensure_Prior_Elaboration_Dynamic
(N => N,
Unit_Id => Unit_Id,
Prag_Nam => Prag_Nam);
else
pragma Assert (Static_Elaboration_Checks);
- Ensure_Static_Prior_Elaboration
+ Ensure_Prior_Elaboration_Static
(N => N,
Unit_Id => Unit_Id,
Prag_Nam => Prag_Nam);
end if;
end Ensure_Prior_Elaboration;
+ --------------------------------------
+ -- Ensure_Prior_Elaboration_Dynamic --
+ --------------------------------------
+
+ procedure Ensure_Prior_Elaboration_Dynamic
+ (N : Node_Id;
+ Unit_Id : Entity_Id;
+ Prag_Nam : Name_Id)
+ is
+ procedure Info_Missing_Pragma;
+ pragma Inline (Info_Missing_Pragma);
+ -- Output information concerning missing Elaborate or Elaborate_All
+ -- pragma with name Prag_Nam for scenario N, which would ensure the
+ -- prior elaboration of Unit_Id.
+
+ -------------------------
+ -- Info_Missing_Pragma --
+ -------------------------
+
+ procedure Info_Missing_Pragma is
+ begin
+ -- Internal units are ignored as they cause unnecessary noise
+
+ if not In_Internal_Unit (Unit_Id) then
+
+ -- The name of the unit subjected to the elaboration pragma is
+ -- fully qualified to improve the clarity of the info message.
+
+ Error_Msg_Name_1 := Prag_Nam;
+ Error_Msg_Qual_Level := Nat'Last;
+
+ Error_Msg_NE ("info: missing pragma % for unit &", N, Unit_Id);
+ Error_Msg_Qual_Level := 0;
+ end if;
+ end Info_Missing_Pragma;
+
+ -- Local variables
+
+ Elab_Attrs : Elaboration_Attributes;
+ Level : Enclosing_Level_Kind;
+
+ -- Start of processing for Ensure_Prior_Elaboration_Dynamic
+
+ begin
+ Elab_Attrs := Elaboration_Context.Get (Unit_Id);
+
+ -- Nothing to do when the unit is guaranteed prior elaboration by means
+ -- of a source Elaborate[_All] pragma.
+
+ if Present (Elab_Attrs.Source_Pragma) then
+ return;
+ end if;
+
+ -- Output extra information on a missing Elaborate[_All] pragma when
+ -- switch -gnatel (info messages on implicit Elaborate[_All] pragmas
+ -- is in effect.
+
+ if Elab_Info_Messages then
+
+ -- Performance note: parent traversal
+
+ Level := Find_Enclosing_Level (N);
+
+ -- Declaration-level scenario
+
+ if (Is_Suitable_Call (N) or else Is_Suitable_Instantiation (N))
+ and then Level = Declaration_Level
+ then
+ null;
+
+ -- Library-level scenario
+
+ elsif Level in Library_Level then
+ null;
+
+ -- Instantiation library-level scenario
+
+ elsif Level = Instantiation then
+ null;
+
+ -- Otherwise the scenario does not appear at the proper level and
+ -- cannot possibly act as a top-level scenario.
+
+ else
+ return;
+ end if;
+
+ Info_Missing_Pragma;
+ end if;
+ end Ensure_Prior_Elaboration_Dynamic;
+
-------------------------------------
- -- Ensure_Static_Prior_Elaboration --
+ -- Ensure_Prior_Elaboration_Static --
-------------------------------------
- procedure Ensure_Static_Prior_Elaboration
+ procedure Ensure_Prior_Elaboration_Static
(N : Node_Id;
Unit_Id : Entity_Id;
Prag_Nam : Name_Id)
function Find_With_Clause
(Items : List_Id;
Withed_Id : Entity_Id) return Node_Id;
- -- Find a non-limited with clause in the list of context items Items
- -- which withs unit Withed_Id. Return Empty if no such clause is found.
+ pragma Inline (Find_With_Clause);
+ -- Find a nonlimited with clause in the list of context items Items
+ -- that withs unit Withed_Id. Return Empty if no such clause is found.
procedure Info_Implicit_Pragma;
pragma Inline (Info_Implicit_Pragma);
Elab_Attrs : Elaboration_Attributes;
Items : List_Id;
- -- Start of processing for Ensure_Static_Prior_Elaboration
+ -- Start of processing for Ensure_Prior_Elaboration_Static
begin
Elab_Attrs := Elaboration_Context.Get (Unit_Id);
if Elab_Info_Messages then
Info_Implicit_Pragma;
end if;
- end Ensure_Static_Prior_Elaboration;
+ end Ensure_Prior_Elaboration_Static;
-----------------------------
-- Extract_Assignment_Name --
Full_Context : Boolean);
-- Add unit Unit_Id to the elaboration context. Prag denotes the pragma
-- which prompted the inclusion of the unit to the elaboration context.
- -- If flag Full_Context is set, examine the non-limited clauses of unit
+ -- If flag Full_Context is set, examine the nonlimited clauses of unit
-- Unit_Id and add each withed unit to the context.
procedure Find_Elaboration_Context (Comp_Unit : Node_Id);
if Full_Context then
- -- Process all non-limited with clauses found in the context of
+ -- Process all nonlimited with clauses found in the context of
-- the current unit. Note that limited clauses do not impose an
-- elaboration order.
In_SPARK => In_SPARK);
end Info_Instantiation;
- -----------------------------
- -- Info_Variable_Reference --
- -----------------------------
+ ------------------------
+ -- Info_Variable_Read --
+ ------------------------
- procedure Info_Variable_Reference
+ procedure Info_Variable_Read
(Ref : Node_Id;
Var_Id : Entity_Id;
Info_Msg : Boolean;
is
begin
Elab_Msg_NE
- (Msg => "reference to variable & during elaboration",
+ (Msg => "read of variable & during elaboration",
N => Ref,
Id => Var_Id,
Info_Msg => Info_Msg,
In_SPARK => In_SPARK);
- end Info_Variable_Reference;
+ end Info_Variable_Read;
--------------------
-- Insertion_Node --
Ekind (Id) = E_Procedure and then Is_Initial_Condition_Procedure (Id);
end Is_Initial_Condition_Proc;
+ --------------------
+ -- Is_Initialized --
+ --------------------
+
+ function Is_Initialized (Obj_Decl : Node_Id) return Boolean is
+ begin
+ -- To qualify, the object declaration must have an expression
+
+ return
+ Present (Expression (Obj_Decl)) or else Has_Init_Expression (Obj_Decl);
+ end Is_Initialized;
+
-----------------------
-- Is_Invariant_Proc --
-----------------------
or else Is_Suitable_Call (N)
or else Is_Suitable_Instantiation (N)
or else Is_Suitable_Variable_Assignment (N)
- or else Is_Suitable_Variable_Reference (N);
+ or else Is_Suitable_Variable_Read (N);
end Is_Suitable_Scenario;
-------------------------------------
-- To qualify, the assignment must meet the following prerequisites:
return
-
- -- The variable must be a source entity and susceptible to warnings
-
Comes_From_Source (Var_Id)
- and then not Warnings_Off (Var_Id)
-- The variable must be declared in the spec of compilation unit U
and then Find_Enclosing_Level (Var_Decl) = Package_Spec
- -- The variable must lack initialization
-
- and then not Has_Init_Expression (Var_Decl)
- and then No (Expression (Var_Decl))
-
-- The assignment must occur in the body of compilation unit U
and then Nkind (N_Unit) = N_Package_Body
and then Present (Corresponding_Body (Var_Unit))
- and then Corresponding_Body (Var_Unit) = N_Unit_Id
-
- -- The package spec must lack pragma Elaborate_Body
-
- and then not Has_Pragma_Elaborate_Body (Var_Unit_Id);
+ and then Corresponding_Body (Var_Unit) = N_Unit_Id;
end Is_Suitable_Variable_Assignment;
- ------------------------------------
- -- Is_Suitable_Variable_Reference --
- ------------------------------------
+ -------------------------------
+ -- Is_Suitable_Variable_Read --
+ -------------------------------
- function Is_Suitable_Variable_Reference (N : Node_Id) return Boolean is
+ function Is_Suitable_Variable_Read (N : Node_Id) return Boolean is
function In_Pragma (Nod : Node_Id) return Boolean;
- -- Determine whether arbitrary node N appears within a pragma
+ -- Determine whether arbitrary node Nod appears within a pragma
+
+ function Is_Variable_Read (Ref : Node_Id) return Boolean;
+ -- Determine whether variable reference Ref constitutes a read
---------------
-- In_Pragma --
return False;
end In_Pragma;
+ ----------------------
+ -- Is_Variable_Read --
+ ----------------------
+
+ function Is_Variable_Read (Ref : Node_Id) return Boolean is
+ function Is_Out_Actual (Call : Node_Id) return Boolean;
+ -- Determine whether the corresponding formal of actual Ref which
+ -- appears in call Call has mode OUT.
+
+ -------------------
+ -- Is_Out_Actual --
+ -------------------
+
+ function Is_Out_Actual (Call : Node_Id) return Boolean is
+ Actual : Node_Id;
+ Call_Attrs : Call_Attributes;
+ Formal : Entity_Id;
+ Target_Id : Entity_Id;
+
+ begin
+ Extract_Call_Attributes
+ (Call => Call,
+ Target_Id => Target_Id,
+ Attrs => Call_Attrs);
+
+ -- Inspect the actual and formal parameters, trying to find the
+ -- corresponding formal for Ref.
+
+ Actual := First_Actual (Call);
+ Formal := First_Formal (Target_Id);
+ while Present (Actual) and then Present (Formal) loop
+ if Actual = Ref then
+ return Ekind (Formal) = E_Out_Parameter;
+ end if;
+
+ Next_Actual (Actual);
+ Next_Formal (Formal);
+ end loop;
+
+ return False;
+ end Is_Out_Actual;
+
+ -- Local variables
+
+ Context : constant Node_Id := Parent (Ref);
+
+ -- Start of processing for Is_Variable_Read
+
+ begin
+ -- The majority of variable references are reads, and they can appear
+ -- in a great number of contexts. To determine whether a reference is
+ -- a read, it is more practical to find out whether it is a write.
+
+ -- A reference is a write when appearing immediately on the left-hand
+ -- side of an assignment.
+
+ if Nkind (Context) = N_Assignment_Statement
+ and then Name (Context) = Ref
+ then
+ return False;
+
+ -- A reference is a write when it acts as an actual in a subprogram
+ -- call and the corresponding formal has mode OUT.
+
+ elsif Nkind_In (Context, N_Function_Call,
+ N_Procedure_Call_Statement)
+ and then Is_Out_Actual (Context)
+ then
+ return False;
+ end if;
+
+ -- Any other reference is a read
+
+ return True;
+ end Is_Variable_Read;
+
-- Local variables
Prag : Node_Id;
Var_Id : Entity_Id;
- -- Start of processing for Is_Suitable_Variable_Reference
+ -- Start of processing for Is_Suitable_Variable_Read
begin
-- This scenario is relevant only when the static model is in effect
return False;
-- Attributes and operator sumbols are not considered to be suitable
- -- references to variables even though they are part of predicate
- -- Is_Entity_Name.
+ -- references even though they are part of predicate Is_Entity_Name.
elsif not Nkind_In (N, N_Expanded_Name, N_Identifier) then
return False;
and then Get_SPARK_Mode_From_Annotation (Prag) = On
and then Is_SPARK_Mode_On_Node (N)
+ -- The reference must denote a variable read
+
+ and then Is_Variable_Read (N)
+
-- The reference must not be considered when it appears in a pragma.
-- If the pragma has run-time semantics, then the reference will be
-- reconsidered once the pragma is expanded.
-- Performance note: parent traversal
and then not In_Pragma (N);
- end Is_Suitable_Variable_Reference;
+ end Is_Suitable_Variable_Read;
-------------------
-- Is_Task_Entry --
Info_Msg => False,
In_SPARK => True);
- elsif Is_Suitable_Variable_Reference (N) then
- Info_Variable_Reference
+ elsif Is_Suitable_Variable_Read (N) then
+ Info_Variable_Read
(Ref => N,
Var_Id => Target_Id,
Info_Msg => False,
procedure Output_Variable_Assignment (N : Node_Id);
-- Emit a specific diagnostic message for assignment statement N
- procedure Output_Variable_Reference (N : Node_Id);
- -- Emit a specific diagnostic message for variable reference N
+ procedure Output_Variable_Read (N : Node_Id);
+ -- Emit a specific diagnostic message for reference N which reads a
+ -- variable.
-------------------
-- Output_Access --
Error_Msg_NE ("\\ variable & assigned #", Error_Nod, Var_Id);
end Output_Variable_Assignment;
- -------------------------------
- -- Output_Variable_Reference --
- -------------------------------
+ --------------------------
+ -- Output_Variable_Read --
+ --------------------------
- procedure Output_Variable_Reference (N : Node_Id) is
+ procedure Output_Variable_Read (N : Node_Id) is
Dummy : Variable_Attributes;
Var_Id : Entity_Id;
Attrs => Dummy);
Error_Msg_Sloc := Sloc (N);
- Error_Msg_NE ("\\ variable & referenced #", Error_Nod, Var_Id);
- end Output_Variable_Reference;
+ Error_Msg_NE ("\\ variable & read #", Error_Nod, Var_Id);
+ end Output_Variable_Read;
-- Local variables
elsif Nkind (N) = N_Assignment_Statement then
Output_Variable_Assignment (N);
- -- Variable references
+ -- Variable read
- elsif Is_Suitable_Variable_Reference (N) then
- Output_Variable_Reference (N);
+ elsif Is_Suitable_Variable_Read (N) then
+ Output_Variable_Read (N);
else
pragma Assert (False);
---------------------------------
procedure Process_Variable_Assignment (Asmt : Node_Id) is
- Var_Id : constant Entity_Id := Entity (Extract_Assignment_Name (Asmt));
- Spec_Id : Entity_Id;
+ Var_Id : constant Entity_Id := Entity (Extract_Assignment_Name (Asmt));
+ Prag : constant Node_Id := SPARK_Pragma (Var_Id);
+
+ SPARK_Rules_On : Boolean;
+ -- This flag is set when the SPARK rules are in effect
begin
+ -- The SPARK rules are in effect when both the assignment and the
+ -- variable are subject to SPARK_Mode On.
+
+ SPARK_Rules_On :=
+ Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = On
+ and then Is_SPARK_Mode_On_Node (Asmt);
+
-- Output relevant information when switch -gnatel (info messages on
-- implicit Elaborate[_All] pragmas) is in effect.
if Elab_Info_Messages then
- Error_Msg_NE
- ("info: assignment to & during elaboration", Asmt, Var_Id);
+ Elab_Msg_NE
+ (Msg => "assignment to & during elaboration",
+ N => Asmt,
+ Id => Var_Id,
+ Info_Msg => True,
+ In_SPARK => SPARK_Rules_On);
end if;
- Spec_Id := Find_Top_Unit (Var_Id);
+ -- The SPARK rules are in effect
+
+ if SPARK_Rules_On then
+ Process_Variable_Assignment_SPARK
+ (Asmt => Asmt,
+ Var_Id => Var_Id);
- -- Generate an implicit Elaborate_Body in the spec
+ -- Otherwise the Ada rules are in effect
- Set_Elaborate_Body_Desirable (Spec_Id);
+ else
+ Process_Variable_Assignment_Ada
+ (Asmt => Asmt,
+ Var_Id => Var_Id);
+ end if;
+ end Process_Variable_Assignment;
- -- No warning is emitted for internal uses. This behaviour parallels
- -- that of the old ABE mechanism.
+ -------------------------------------
+ -- Process_Variable_Assignment_Ada --
+ -------------------------------------
- if GNAT_Mode then
- null;
+ procedure Process_Variable_Assignment_Ada
+ (Asmt : Node_Id;
+ Var_Id : Entity_Id)
+ is
+ Var_Decl : constant Node_Id := Declaration_Node (Var_Id);
+ Spec_Id : constant Entity_Id := Find_Top_Unit (Var_Decl);
+
+ begin
+ -- Emit a warning when an uninitialized variable declared in a package
+ -- spec without a pragma Elaborate_Body is initialized by elaboration
+ -- code within the corresponding body.
+
+ if not Warnings_Off (Var_Id)
+ and then not Is_Initialized (Var_Decl)
+ and then not Has_Pragma_Elaborate_Body (Spec_Id)
+ then
+ -- Generate an implicit Elaborate_Body in the spec
+
+ Set_Elaborate_Body_Desirable (Spec_Id);
- else
Error_Msg_NE
("??variable & can be accessed by clients before this "
& "initialization", Asmt, Var_Id);
Output_Active_Scenarios (Asmt);
end if;
- end Process_Variable_Assignment;
+ end Process_Variable_Assignment_Ada;
- --------------------------------
- -- Process_Variable_Reference --
- --------------------------------
+ ---------------------------------------
+ -- Process_Variable_Assignment_SPARK --
+ ---------------------------------------
+
+ procedure Process_Variable_Assignment_SPARK
+ (Asmt : Node_Id;
+ Var_Id : Entity_Id)
+ is
+ Var_Decl : constant Node_Id := Declaration_Node (Var_Id);
+ Spec_Id : constant Entity_Id := Find_Top_Unit (Var_Decl);
+
+ begin
+ -- Emit an error when an initialized variable declared in a package spec
+ -- without pragma Elaborate_Body is further modified by elaboration code
+ -- within the corresponding body.
+
+ if Is_Initialized (Var_Decl)
+ and then not Has_Pragma_Elaborate_Body (Spec_Id)
+ then
+ Error_Msg_NE
+ ("variable & modified by elaboration code in package body",
+ Asmt, Var_Id);
- procedure Process_Variable_Reference (Ref : Node_Id) is
+ Error_Msg_NE
+ ("\add pragma ""Elaborate_Body"" to spec & to ensure full "
+ & "initialization", Asmt, Spec_Id);
+
+ Output_Active_Scenarios (Asmt);
+ end if;
+ end Process_Variable_Assignment_SPARK;
+
+ ---------------------------
+ -- Process_Variable_Read --
+ ---------------------------
+
+ procedure Process_Variable_Read (Ref : Node_Id) is
Var_Attrs : Variable_Attributes;
Var_Id : Entity_Id;
if Elab_Info_Messages then
Elab_Msg_NE
- (Msg => "reference to variable & during elaboration",
+ (Msg => "read of variable & during elaboration",
N => Ref,
Id => Var_Id,
Info_Msg => True,
In_SPARK => True);
end if;
- -- A source variable reference imposes an Elaborate_All requirement on
- -- the context of the main unit. Determine whethe the context has a
- -- pragma strong enough to meet the requirement.
+ -- Nothing to do when the variable appears within the main unit because
+ -- diagnostics on reads are relevant only for external variables.
- Meet_Elaboration_Requirement
- (N => Ref,
- Target_Id => Var_Id,
- Req_Nam => Name_Elaborate_All);
- end Process_Variable_Reference;
+ if Is_Same_Unit (Var_Attrs.Unit_Id, Cunit_Entity (Main_Unit)) then
+ null;
+
+ -- Nothing to do when the variable is already initialized. Note that the
+ -- variable may be further modified by the external unit.
+
+ elsif Is_Initialized (Declaration_Node (Var_Id)) then
+ null;
+
+ -- Nothing to do when the external unit guarantees the initialization of
+ -- the variable by means of pragma Elaborate_Body.
+
+ elsif Has_Pragma_Elaborate_Body (Var_Attrs.Unit_Id) then
+ null;
+
+ -- A variable read imposes an Elaborate requirement on the context of
+ -- the main unit. Determine whether the context has a pragma strong
+ -- enough to meet the requirement.
+
+ else
+ Meet_Elaboration_Requirement
+ (N => Ref,
+ Target_Id => Var_Id,
+ Req_Nam => Name_Elaborate);
+ end if;
+ end Process_Variable_Read;
--------------------------
-- Push_Active_Scenario --
elsif Is_Suitable_Variable_Assignment (N) then
Process_Variable_Assignment (N);
- -- Variable references
+ -- Variable read
- elsif Is_Suitable_Variable_Reference (N) then
- Process_Variable_Reference (N);
+ elsif Is_Suitable_Variable_Read (N) then
+ Process_Variable_Read (N);
end if;
-- Remove the current scenario from the stack of active scenarios once
elsif Is_Suitable_Access (N)
or else Is_Suitable_Variable_Assignment (N)
- or else Is_Suitable_Variable_Reference (N)
+ or else Is_Suitable_Variable_Read (N)
then
null;
git://gcc.gnu.org / gcc.git / commitdiff