+2017-04-25 Arnaud Charlet <charlet@adacore.com>
+
+ * rtsfind.ads (SPARK_Implicit_Load): New procedure for forced
+ loading of an entity.
+ * rtsfind.adb (SPARK_Implicit_Load): Body with a pattern
+ previously repeated in the analysis.
+ * sem_ch9.adb (Analyze_Protected_Type_Declaration): use new
+ procedure SPARK_Implicit_Load. (Analyze_Task_Type_Declaration):
+ use new procedure SPARK_Implicit_Load.
+ * sem_ch10.adb (Analyze_Compilation_Unit): Use new procedure
+ SPARK_Implicit_Load.
+
+2017-04-25 Javier Miranda <miranda@adacore.com>
+
+ * sem_util.adb (New_Copy_Tree): By default
+ copying of defining identifiers is prohibited because
+ this would introduce an entirely new entity into the
+ tree. This patch introduces an exception to this general
+ rule: the declaration of constants and variables located in
+ Expression_With_Action nodes.
+ (Copy_Itype_With_Replacement): Renamed as Copy_Entity_With_Replacement.
+ (In_Map): New subprogram.
+ (Visit_Entity): New subprogram.
+ (Visit_Node): Handle EWA_Level,
+ EWA_Inner_Scope_Level, and take care of defining entities defined
+ in Expression_With_Action nodes.
+
+2017-04-25 Thomas Quinot <quinot@adacore.com>
+
+ * exp_ch6.adb: minor comment edit.
+ * sinfo.ads, sinfo.adb: New Null_Statement attribute for null
+ procedure specifications that come from source.
+ * par-ch6.adb (P_Subprogram, case of a null procedure): Set new
+ Null_Statement attribute.
+ * par_sco.adb (Traverse_Declarations_Or_Statements): For a null
+ procedure, generate statement SCO for the generated NULL statement.
+ * sem_ch6.adb (Analyze_Null_Procedure): Use null statement from
+ parser, if available.
+
2017-04-04 Andreas Krebbel <krebbel@linux.vnet.ibm.com>
* system-linux-s390.ads: Use Long_Integer'Size to define
-- Ada 2005 (AI-348): Generate body for a null procedure. In most
-- cases this is superfluous because calls to it will be automatically
-- inlined, but we definitely need the body if preconditions for the
- -- procedure are present.
+ -- procedure are present, or if performing coverage analysis.
elsif Nkind (Specification (N)) = N_Procedure_Specification
and then Null_Present (Specification (N))
Error_Msg_SP ("only procedures can be null");
else
Set_Null_Present (Specification_Node);
+ Set_Null_Statement (Specification_Node,
+ New_Node (N_Null_Statement, Prev_Token_Ptr));
end if;
goto Subprogram_Declaration;
Process_Decisions_Defer
(Parameter_Specifications (Spec), 'X');
- -- Case of a null procedure: generate a NULL statement SCO
+ -- Case of a null procedure: generate SCO for fictitious
+ -- NULL statement located at the NULL keyword in the
+ -- procedure specification.
if Nkind (N) = N_Subprogram_Declaration
and then Nkind (Spec) = N_Procedure_Specification
and then Null_Present (Spec)
then
- Traverse_Degenerate_Subprogram (N);
+ Traverse_Degenerate_Subprogram (Null_Statement (Spec));
-- Case of an expression function: generate a statement SCO
-- for the expression (and then decision SCOs for any nested
end loop;
end Set_RTU_Loaded;
+ -------------------------
+ -- SPARK_Implicit_Load --
+ -------------------------
+
+ procedure SPARK_Implicit_Load (E : RE_Id) is
+ Unused : Entity_Id;
+
+ begin
+ pragma Assert (GNATprove_Mode);
+
+ -- Force loading of a predefined unit
+ Unused := RTE (E);
+ end SPARK_Implicit_Load;
+
end Rtsfind;
procedure Set_RTU_Loaded (N : Node_Id);
-- Register the predefined unit N as already loaded
+ procedure SPARK_Implicit_Load (E : RE_Id);
+ -- Force loading of the unit containing the entity E; only needed in
+ -- GNATprove mode when processing code that implicitly references a
+ -- given entity.
+
end Rtsfind;
N_Function_Instantiation)
then
declare
- Spec : Node_Id;
- Unused : Entity_Id;
+ Spec : Node_Id;
begin
case Nkind (Unit_Node) is
pragma Assert (Nkind (Spec) in N_Subprogram_Specification);
- -- Only subprogram with no parameters can act as "main", and if
- -- it is a function, it needs to return an integer.
+ -- Main subprogram must have no parameters, and if it is a
+ -- function, it must return an integer.
if No (Parameter_Specifications (Spec))
and then (Nkind (Spec) = N_Procedure_Specification
or else
Is_Integer_Type (Etype (Result_Definition (Spec))))
then
- Unused := RTE (RE_Interrupt_Priority);
+ SPARK_Implicit_Load (RE_Interrupt_Priority);
end if;
end;
end if;
Designator : Entity_Id;
Form : Node_Id;
Null_Body : Node_Id := Empty;
+ Null_Stmt : Node_Id := Null_Statement (Spec);
Prev : Entity_Id;
begin
-- the first case the body is analyzed at the freeze point, in the other
-- it replaces the null procedure declaration.
+ -- For a null procedure that comes from source, a NULL statement is
+ -- provided by the parser, which carries the source location of the
+ -- NULL keyword, and has Comes_From_Source set. For a null procedure
+ -- from expansion, create one now.
+
+ if No (Null_Stmt) then
+ Null_Stmt := Make_Null_Statement (Loc);
+ end if;
+
Null_Body :=
Make_Subprogram_Body (Loc,
Specification => New_Copy_Tree (Spec),
Declarations => New_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (Make_Null_Statement (Loc))));
+ Statements => New_List (Null_Stmt)));
-- Create new entities for body and formals
-- force the loading of the Ada.Real_Time package.
if GNATprove_Mode then
- declare
- Unused : Entity_Id;
-
- begin
- Unused := RTE (RO_RT_Time);
- end;
+ SPARK_Implicit_Load (RO_RT_Time);
end if;
end Analyze_Delay_Relative;
-- calls originating from protected subprograms and entries.
if GNATprove_Mode then
- declare
- Unused : Entity_Id;
-
- begin
- Unused := RTE (RE_Interrupt_Priority);
- end;
+ SPARK_Implicit_Load (RE_Interrupt_Priority);
end if;
end Analyze_Protected_Type_Declaration;
-- calls originating from tasks.
if GNATprove_Mode then
- declare
- Unused : Entity_Id;
-
- begin
- Unused := RTE (RE_Interrupt_Priority);
- end;
+ SPARK_Implicit_Load (RE_Interrupt_Priority);
end if;
end Analyze_Task_Type_Declaration;
New_Sloc : Source_Ptr := No_Location;
New_Scope : Entity_Id := Empty) return Node_Id
is
+ EWA_Level : Nat := 0;
+ -- By default copying of defining identifiers is prohibited because this
+ -- would introduce an entirely new entity into the tree. The exception
+ -- to this general rule are declaration of constants and variables
+ -- located in Expression_With_Action nodes.
+
+ EWA_Inner_Scope_Level : Nat := 0;
+ -- Level of internal scope of defined in EWAs. Used to avoid creating
+ -- variables for declarations located in blocks or subprograms defined
+ -- in Expression_With_Action nodes.
+
------------------------------------
-- Auxiliary Data and Subprograms --
------------------------------------
(Old_Elist : Elist_Id) return Elist_Id;
-- Called during second phase to copy element list doing replacements
- procedure Copy_Itype_With_Replacement (New_Itype : Entity_Id);
- -- Called during the second phase to process a copied Itype. The actual
+ procedure Copy_Entity_With_Replacement (New_Entity : Entity_Id);
+ -- Called during the second phase to process a copied Entity. The actual
-- copy happened during the first phase (so that we could make the entry
-- in the mapping), but we still have to deal with the descendants of
- -- the copied Itype and copy them where necessary.
+ -- the copied Entity and copy them where necessary.
function Copy_List_With_Replacement (Old_List : List_Id) return List_Id;
-- Called during second phase to copy list doing replacements
function Copy_Node_With_Replacement (Old_Node : Node_Id) return Node_Id;
-- Called during second phase to copy node doing replacements
+ function In_Map (E : Entity_Id) return Boolean;
+ -- Return True if E is one of the old entities specified in the set of
+ -- mappings to be applied to entities in the tree (ie. Map).
+
procedure Visit_Elist (E : Elist_Id);
-- Called during first phase to visit all elements of an Elist
+ procedure Visit_Entity (Old_Entity : Entity_Id);
+ -- Called during first phase to visit subsidiary fields of a defining
+ -- entity which is not an itype, and also create a copy and make an
+ -- entry in the replacement map for the new copy.
+
procedure Visit_Field (F : Union_Id; N : Node_Id);
-- Visit a single field, recursing to call Visit_Node or Visit_List if
-- the field is a syntactic descendant of the current node (i.e. its
return New_Elist;
end Copy_Elist_With_Replacement;
- ---------------------------------
- -- Copy_Itype_With_Replacement --
- ---------------------------------
+ ----------------------------------
+ -- Copy_Entity_With_Replacement --
+ ----------------------------------
-- This routine exactly parallels its phase one analog Visit_Itype,
- procedure Copy_Itype_With_Replacement (New_Itype : Entity_Id) is
+ procedure Copy_Entity_With_Replacement (New_Entity : Entity_Id) is
begin
-- Translate Next_Entity, Scope, and Etype fields, in case they
-- reference entities that have been mapped into copies.
- Set_Next_Entity (New_Itype, Assoc (Next_Entity (New_Itype)));
- Set_Etype (New_Itype, Assoc (Etype (New_Itype)));
+ Set_Next_Entity (New_Entity, Assoc (Next_Entity (New_Entity)));
+ Set_Etype (New_Entity, Assoc (Etype (New_Entity)));
if Present (New_Scope) then
- Set_Scope (New_Itype, New_Scope);
+ Set_Scope (New_Entity, New_Scope);
else
- Set_Scope (New_Itype, Assoc (Scope (New_Itype)));
+ Set_Scope (New_Entity, Assoc (Scope (New_Entity)));
end if;
-- Copy referenced fields
- if Is_Discrete_Type (New_Itype) then
- Set_Scalar_Range (New_Itype,
- Copy_Node_With_Replacement (Scalar_Range (New_Itype)));
+ if Is_Discrete_Type (New_Entity) then
+ Set_Scalar_Range (New_Entity,
+ Copy_Node_With_Replacement (Scalar_Range (New_Entity)));
- elsif Has_Discriminants (Base_Type (New_Itype)) then
- Set_Discriminant_Constraint (New_Itype,
+ elsif Has_Discriminants (Base_Type (New_Entity)) then
+ Set_Discriminant_Constraint (New_Entity,
Copy_Elist_With_Replacement
- (Discriminant_Constraint (New_Itype)));
+ (Discriminant_Constraint (New_Entity)));
- elsif Is_Array_Type (New_Itype) then
- if Present (First_Index (New_Itype)) then
- Set_First_Index (New_Itype,
+ elsif Is_Array_Type (New_Entity) then
+ if Present (First_Index (New_Entity)) then
+ Set_First_Index (New_Entity,
First (Copy_List_With_Replacement
- (List_Containing (First_Index (New_Itype)))));
+ (List_Containing (First_Index (New_Entity)))));
end if;
- if Is_Packed (New_Itype) then
- Set_Packed_Array_Impl_Type (New_Itype,
+ if Is_Packed (New_Entity) then
+ Set_Packed_Array_Impl_Type (New_Entity,
Copy_Node_With_Replacement
- (Packed_Array_Impl_Type (New_Itype)));
+ (Packed_Array_Impl_Type (New_Entity)));
end if;
end if;
- end Copy_Itype_With_Replacement;
+ end Copy_Entity_With_Replacement;
--------------------------------
-- Copy_List_With_Replacement --
return New_Node;
end Copy_Node_With_Replacement;
+ ------------
+ -- In_Map --
+ ------------
+
+ function In_Map (E : Entity_Id) return Boolean is
+ Elmt : Elmt_Id;
+ Ent : Entity_Id;
+
+ begin
+ if Present (Map) then
+ Elmt := First_Elmt (Map);
+ while Present (Elmt) loop
+ Ent := Node (Elmt);
+
+ if Ent = E then
+ return True;
+ end if;
+
+ Next_Elmt (Elmt);
+ Next_Elmt (Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end In_Map;
-------------------
-- New_Copy_Hash --
-------------------
end if;
end Visit_Elist;
+ ------------------
+ -- Visit_Entity --
+ ------------------
+
+ procedure Visit_Entity (Old_Entity : Entity_Id) is
+ New_E : Entity_Id;
+
+ begin
+ pragma Assert (not Is_Itype (Old_Entity));
+ pragma Assert (Nkind (Old_Entity) in N_Entity);
+
+ -- Restrict entity creation to variable declarations. There is no
+ -- need to create variables declared in inner scopes.
+
+ if not Ekind_In (Old_Entity, E_Constant, E_Variable)
+ or else EWA_Inner_Scope_Level > 0
+ then
+ return;
+ end if;
+
+ New_E := New_Copy (Old_Entity);
+
+ -- The new entity has all the attributes of the old one, and we
+ -- just copy the contents of the entity. However, the back-end
+ -- needs different names for debugging purposes, so we create a
+ -- new internal name for it in all cases.
+
+ Set_Chars (New_E, New_Internal_Name ('T'));
+
+ -- Add new association to map
+
+ NCT_Assoc.Set (Old_Entity, New_E);
+
+ -- Visit descendants that eventually get copied
+
+ Visit_Field (Union_Id (Etype (Old_Entity)), Old_Entity);
+ end Visit_Entity;
+
-----------------
-- Visit_Field --
-----------------
procedure Visit_Node (N : Node_Or_Entity_Id) is
begin
+ if Nkind (N) = N_Expression_With_Actions then
+ EWA_Level := EWA_Level + 1;
+
+ elsif EWA_Level > 0
+ and then Nkind_In (N, N_Block_Statement,
+ N_Subprogram_Body,
+ N_Subprogram_Declaration)
+ then
+ EWA_Inner_Scope_Level := EWA_Inner_Scope_Level + 1;
+
-- Handle case of an Itype, which must be copied
- if Nkind (N) in N_Entity and then Is_Itype (N) then
+ elsif Nkind (N) in N_Entity and then Is_Itype (N) then
-- Nothing to do if already in the list. This can happen with an
-- Itype entity that appears more than once in the tree. Note that
end if;
Visit_Itype (N);
+
+ -- Handle defining entities in Expression_With_Action nodes
+
+ elsif Nkind (N) in N_Entity and then EWA_Level > 0 then
+
+ -- Nothing to do if already in the hash table
+
+ if Present (NCT_Assoc.Get (Entity_Id (N))) then
+ return;
+ end if;
+
+ Visit_Entity (N);
end if;
-- Visit descendants
Visit_Field (Field3 (N), N);
Visit_Field (Field4 (N), N);
Visit_Field (Field5 (N), N);
+
+ if EWA_Level > 0
+ and then Nkind_In (N, N_Block_Statement,
+ N_Subprogram_Body,
+ N_Subprogram_Declaration)
+ then
+ EWA_Inner_Scope_Level := EWA_Inner_Scope_Level - 1;
+
+ elsif Nkind (N) = N_Expression_With_Actions then
+ EWA_Level := EWA_Level - 1;
+ end if;
end Visit_Node;
-- Start of processing for New_Copy_Tree
begin
NCT_Assoc.Get_First (Old_E, New_E);
while Present (New_E) loop
- if Is_Itype (New_E) then
- Copy_Itype_With_Replacement (New_E);
+
+ -- Skip entities that were not created in the first phase (that
+ -- is, old entities specified by the caller in the set of mappings
+ -- to be applied to the tree).
+
+ if Is_Itype (New_E)
+ or else No (Map)
+ or else not In_Map (Old_E)
+ then
+ Copy_Entity_With_Replacement (New_E);
end if;
NCT_Assoc.Get_Next (Old_E, New_E);
return Flag18 (N);
end Non_Aliased_Prefix;
- function Null_Present
- (N : Node_Id) return Boolean is
- begin
- pragma Assert (False
- or else NT (N).Nkind = N_Component_List
- or else NT (N).Nkind = N_Procedure_Specification
- or else NT (N).Nkind = N_Record_Definition);
- return Flag13 (N);
- end Null_Present;
-
function Null_Excluding_Subtype
(N : Node_Id) return Boolean is
begin
return Flag14 (N);
end Null_Exclusion_In_Return_Present;
+ function Null_Present
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Component_List
+ or else NT (N).Nkind = N_Procedure_Specification
+ or else NT (N).Nkind = N_Record_Definition);
+ return Flag13 (N);
+ end Null_Present;
+
function Null_Record_Present
(N : Node_Id) return Boolean is
begin
return Flag17 (N);
end Null_Record_Present;
+ function Null_Statement
+ (N : Node_Id) return Node_Id is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Procedure_Specification);
+ return Node2 (N);
+ end Null_Statement;
+
function Object_Definition
(N : Node_Id) return Node_Id is
begin
Set_Flag18 (N, Val);
end Set_Non_Aliased_Prefix;
- procedure Set_Null_Present
- (N : Node_Id; Val : Boolean := True) is
- begin
- pragma Assert (False
- or else NT (N).Nkind = N_Component_List
- or else NT (N).Nkind = N_Procedure_Specification
- or else NT (N).Nkind = N_Record_Definition);
- Set_Flag13 (N, Val);
- end Set_Null_Present;
-
procedure Set_Null_Excluding_Subtype
(N : Node_Id; Val : Boolean := True) is
begin
Set_Flag14 (N, Val);
end Set_Null_Exclusion_In_Return_Present;
+ procedure Set_Null_Present
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Component_List
+ or else NT (N).Nkind = N_Procedure_Specification
+ or else NT (N).Nkind = N_Record_Definition);
+ Set_Flag13 (N, Val);
+ end Set_Null_Present;
+
procedure Set_Null_Record_Present
(N : Node_Id; Val : Boolean := True) is
begin
Set_Flag17 (N, Val);
end Set_Null_Record_Present;
+ procedure Set_Null_Statement
+ (N : Node_Id; Val : Node_Id) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Procedure_Specification);
+ Set_Node2 (N, Val);
+ end Set_Null_Statement;
+
procedure Set_Object_Definition
(N : Node_Id; Val : Node_Id) is
begin
-- N_Procedure_Specification
-- Sloc points to PROCEDURE
-- Defining_Unit_Name (Node1)
+ -- Null_Statement (Node2-Sem) NULL statement for body, if Null_Present
-- Parameter_Specifications (List3) (set to No_List if no formal part)
-- Generic_Parent (Node5-Sem)
-- Null_Present (Flag13) set for null procedure case (Ada 2005 feature)
function Non_Aliased_Prefix
(N : Node_Id) return Boolean; -- Flag18
- function Null_Present
- (N : Node_Id) return Boolean; -- Flag13
-
function Null_Excluding_Subtype
(N : Node_Id) return Boolean; -- Flag16
function Null_Exclusion_In_Return_Present
(N : Node_Id) return Boolean; -- Flag14
+ function Null_Present
+ (N : Node_Id) return Boolean; -- Flag13
+
function Null_Record_Present
(N : Node_Id) return Boolean; -- Flag17
+ function Null_Statement
+ (N : Node_Id) return Node_Id; -- Node2
+
function Object_Definition
(N : Node_Id) return Node_Id; -- Node4
procedure Set_Non_Aliased_Prefix
(N : Node_Id; Val : Boolean := True); -- Flag18
- procedure Set_Null_Present
- (N : Node_Id; Val : Boolean := True); -- Flag13
-
procedure Set_Null_Excluding_Subtype
(N : Node_Id; Val : Boolean := True); -- Flag16
procedure Set_Null_Exclusion_In_Return_Present
(N : Node_Id; Val : Boolean := True); -- Flag14
+ procedure Set_Null_Present
+ (N : Node_Id; Val : Boolean := True); -- Flag13
+
procedure Set_Null_Record_Present
(N : Node_Id; Val : Boolean := True); -- Flag17
+ procedure Set_Null_Statement
+ (N : Node_Id; Val : Node_Id); -- Node2
+
procedure Set_Object_Definition
(N : Node_Id; Val : Node_Id); -- Node4
N_Procedure_Specification =>
(1 => True, -- Defining_Unit_Name (Node1)
- 2 => False, -- unused
+ 2 => False, -- Null_Statement (Node2-Sem)
3 => True, -- Parameter_Specifications (List3)
4 => False, -- unused
5 => False), -- Generic_Parent (Node5-Sem)
pragma Inline (No_Side_Effect_Removal);
pragma Inline (No_Truncation);
pragma Inline (Non_Aliased_Prefix);
- pragma Inline (Null_Present);
pragma Inline (Null_Excluding_Subtype);
pragma Inline (Null_Exclusion_Present);
pragma Inline (Null_Exclusion_In_Return_Present);
+ pragma Inline (Null_Present);
pragma Inline (Null_Record_Present);
+ pragma Inline (Null_Statement);
pragma Inline (Object_Definition);
pragma Inline (Of_Present);
pragma Inline (Original_Discriminant);
pragma Inline (Set_Null_Exclusion_In_Return_Present);
pragma Inline (Set_Null_Present);
pragma Inline (Set_Null_Record_Present);
+ pragma Inline (Set_Null_Statement);
pragma Inline (Set_Object_Definition);
pragma Inline (Set_Of_Present);
pragma Inline (Set_Original_Discriminant);