+2014-08-04 Claire Dross <dross@adacore.com>
+
+ * exp_util.adb (Get_First_Parent_With_Ext_Axioms_For_Entity):
+ For an instance, look at the scope before the generic parent.
+
+2014-08-04 Yannick Moy <moy@adacore.com>
+
+ * lib-writ.ads: Update comments.
+ * sem_disp.ads, sem_disp.adb (Inherited_Subprograms): Add
+ parameters to filter inherited subprograms.
+
2014-08-04 Robert Dewar <dewar@adacore.com>
* gnat_rm.texi: Add section on use of address clause for memory
and then Has_Annotate_Pragma_For_External_Axiomatization (E)
then
return E;
+ end if;
- -- E is a package instance, in which case it is axiomatized iff the
- -- corresponding generic package is Axiomatized.
+ -- If E's scope is axiomatized, E is axiomatized.
- elsif Ekind (E) = E_Package
- and then Present (Generic_Parent (Decl))
- then
- return
- Get_First_Parent_With_Ext_Axioms_For_Entity (Generic_Parent (Decl));
+ declare
+ First_Ax_Parent_Scope : Entity_Id := Empty;
- -- Otherwise, look at E's scope instead if present
+ begin
+ if Present (Scope (E)) then
+ First_Ax_Parent_Scope :=
+ Get_First_Parent_With_Ext_Axioms_For_Entity (Scope (E));
+ end if;
- elsif Present (Scope (E)) then
- return
- Get_First_Parent_With_Ext_Axioms_For_Entity (Scope (E));
+ if Present (First_Ax_Parent_Scope) then
+ return First_Ax_Parent_Scope;
+ end if;
- -- Else there is no such axiomatized package
+ -- otherwise, if E is a package instance, it is axiomatized if the
+ -- corresponding generic package is axiomatized.
- else
- return Empty;
- end if;
+ if Ekind (E) = E_Package
+ and then Present (Generic_Parent (Decl))
+ then
+ return
+ Get_First_Parent_With_Ext_Axioms_For_Entity
+ (Generic_Parent (Decl));
+ else
+ return Empty;
+ end if;
+ end;
end Get_First_Parent_With_Ext_Axioms_For_Entity;
---------------------
procedure Write_ALI (Object : Boolean);
-- This procedure writes the library information for the current main unit
-- The Object parameter is true if an object file is created, and false
- -- otherwise.
+ -- otherwise. Note that the pseudo-object file generated in GNATProve mode
+ -- does count as an object file from this point of view.
--
-- Note: in the case where we are not generating code (-gnatc mode), this
-- routine only writes an ALI file if it cannot find an existing up to
-- Inherited_Subprograms --
---------------------------
- function Inherited_Subprograms (S : Entity_Id) return Subprogram_List is
+ function Inherited_Subprograms
+ (S : Entity_Id;
+ No_Interfaces : Boolean := False;
+ Interfaces_Only : Boolean := False) return Subprogram_List
+ is
Result : Subprogram_List (1 .. 6000);
-- 6000 here is intended to be infinity. We could use an expandable
-- table, but it would be awfully heavy, and there is no way that we
-- Start of processing for Inherited_Subprograms
begin
+ pragma Assert (not (No_Interfaces and Interfaces_Only));
+
if Present (S) and then Is_Dispatching_Operation (S) then
-- Deal with direct inheritance
- Parent_Op := S;
- loop
- Parent_Op := Overridden_Operation (Parent_Op);
- exit when No (Parent_Op);
-
- if Is_Subprogram (Parent_Op)
- or else Is_Generic_Subprogram (Parent_Op)
- then
- Store_IS (Parent_Op);
- end if;
- end loop;
+ if not Interfaces_Only then
+ Parent_Op := S;
+ loop
+ Parent_Op := Overridden_Operation (Parent_Op);
+ exit when No (Parent_Op)
+ or else
+ (No_Interfaces
+ and then
+ Is_Interface (Find_Dispatching_Type (Parent_Op)));
+
+ if Is_Subprogram (Parent_Op)
+ or else
+ Is_Generic_Subprogram (Parent_Op)
+ then
+ Store_IS (Parent_Op);
+ end if;
+ end loop;
+ end if;
-- Now deal with interfaces
- declare
- Tag_Typ : Entity_Id;
- Prim : Entity_Id;
- Elmt : Elmt_Id;
+ if not No_Interfaces then
+ declare
+ Tag_Typ : Entity_Id;
+ Prim : Entity_Id;
+ Elmt : Elmt_Id;
- begin
- Tag_Typ := Find_Dispatching_Type (S);
+ begin
+ Tag_Typ := Find_Dispatching_Type (S);
- if Is_Concurrent_Type (Tag_Typ) then
- Tag_Typ := Corresponding_Record_Type (Tag_Typ);
- end if;
+ if Is_Concurrent_Type (Tag_Typ) then
+ Tag_Typ := Corresponding_Record_Type (Tag_Typ);
+ end if;
- -- Search primitive operations of dispatching type
+ -- Search primitive operations of dispatching type
- if Present (Tag_Typ)
- and then Present (Primitive_Operations (Tag_Typ))
- then
- Elmt := First_Elmt (Primitive_Operations (Tag_Typ));
- while Present (Elmt) loop
- Prim := Node (Elmt);
+ if Present (Tag_Typ)
+ and then Present (Primitive_Operations (Tag_Typ))
+ then
+ Elmt := First_Elmt (Primitive_Operations (Tag_Typ));
+ while Present (Elmt) loop
+ Prim := Node (Elmt);
- -- The following test eliminates some odd cases in which
- -- Ekind (Prim) is Void, to be investigated further ???
+ -- The following test eliminates some odd cases in which
+ -- Ekind (Prim) is Void, to be investigated further ???
- if not (Is_Subprogram (Prim)
- or else
- Is_Generic_Subprogram (Prim))
- then
- null;
+ if not (Is_Subprogram (Prim)
+ or else
+ Is_Generic_Subprogram (Prim))
+ then
+ null;
-- For [generic] subprogram, look at interface alias
- elsif Present (Interface_Alias (Prim))
- and then Alias (Prim) = S
- then
- -- We have found a primitive covered by S
+ elsif Present (Interface_Alias (Prim))
+ and then Alias (Prim) = S
+ then
+ -- We have found a primitive covered by S
- Store_IS (Interface_Alias (Prim));
- end if;
+ Store_IS (Interface_Alias (Prim));
+ end if;
- Next_Elmt (Elmt);
- end loop;
- end if;
- end;
+ Next_Elmt (Elmt);
+ end loop;
+ end if;
+ end;
+ end if;
end if;
return Result (1 .. N);
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
type Subprogram_List is array (Nat range <>) of Entity_Id;
-- Type returned by Inherited_Subprograms function
- function Inherited_Subprograms (S : Entity_Id) return Subprogram_List;
+ function Inherited_Subprograms
+ (S : Entity_Id;
+ No_Interfaces : Boolean := False;
+ Interfaces_Only : Boolean := False) return Subprogram_List;
-- Given the spec of a subprogram, this function gathers any inherited
- -- subprograms from direct inheritance or via interfaces. The list is
- -- a list of entity id's of the specs of inherited subprograms. Returns
- -- a null array if passed an Empty spec id. Note that the returned array
+ -- subprograms from direct inheritance or via interfaces. The list is a
+ -- list of entity id's of the specs of inherited subprograms. Returns a
+ -- null array if passed an Empty spec id. Note that the returned array
-- only includes subprograms and generic subprograms (and excludes any
- -- other inherited entities, in particular enumeration literals).
+ -- other inherited entities, in particular enumeration literals). If
+ -- No_Interfaces is True, only return inherited subprograms not coming
+ -- from an interface. If Interfaces_Only is True, only return inherited
+ -- subprograms from interfaces. Otherwise, subprograms inherited directly
+ -- come first, starting with the closest ancestors, and are followed by
+ -- subprograms inherited from interfaces. At most one of No_Interfaces
+ -- and Interfaces_Only should be True.
function Is_Dynamically_Tagged (N : Node_Id) return Boolean;
-- Used to determine whether a call is dispatching, i.e. if is an