+2015-05-26 Yannick Moy <moy@adacore.com>
+
+ * inline.adb (Has_Initialized_Type): Adapt to new names.
+ * sem_aux.adb, sem_aux.ads (Get_Low_Bound, Number_Components,
+ Subprogram_Body, Subprogram_Body_Entity, Subprogram_Spec,
+ Subprogram_Specification): New query functions used in GNATprove.
+ * sem_disp.adb, sem_disp.ads (Is_Overriding_Subprogram): New
+ query functions used in GNATprove.
+ * sem_util.adb, sem_util.adso (Enclosing_Lib_Unit_Node,
+ Get_Cursor_Type, Get_Return_Object, Get_User_Defined_Eq,
+ Is_Double_Precision_Floating_Point_Type,
+ Is_Single_Precision_Floating_Point_Type): New query functions
+ used in GNATprove.
+
2015-05-26 Bob Duff <duff@adacore.com>
* s-rpc.ads (Partition_ID): Increase maximum Partition_ID to
--------------------------
function Has_Initialized_Type (E : Entity_Id) return Boolean is
- E_Body : constant Node_Id := Get_Subprogram_Body (E);
+ E_Body : constant Node_Id := Subprogram_Body (E);
Decl : Node_Id;
begin
end case;
end Get_Binary_Nkind;
+ -------------------
+ -- Get_Low_Bound --
+ -------------------
+
+ function Get_Low_Bound (E : Entity_Id) return Node_Id is
+ begin
+ if Ekind (E) = E_String_Literal_Subtype then
+ return String_Literal_Low_Bound (E);
+ else
+ return Low_Bound (Scalar_Range (E));
+ end if;
+ end Get_Low_Bound;
+
------------------
-- Get_Rep_Item --
------------------
return Empty;
end Next_Tag_Component;
+ -----------------------
+ -- Number_Components --
+ -----------------------
+
+ function Number_Components (Typ : Entity_Id) return Pos is
+ N : Int;
+ Comp : Entity_Id;
+
+ begin
+ N := 0;
+
+ -- We do not call Einfo.First_Component_Or_Discriminant, as this
+ -- function does not skip completely hidden discriminants, which we
+ -- want to skip here.
+
+ if Has_Discriminants (Typ) then
+ Comp := First_Discriminant (Typ);
+ else
+ Comp := First_Component (Typ);
+ end if;
+
+ while Present (Comp) loop
+ N := N + 1;
+ Comp := Next_Component_Or_Discriminant (Comp);
+ end loop;
+
+ return N;
+ end Number_Components;
+
--------------------------
-- Number_Discriminants --
--------------------------
return N;
end Package_Specification;
+ ---------------------
+ -- Subprogram_Body --
+ ---------------------
+
+ function Subprogram_Body (E : Entity_Id) return Node_Id is
+ Body_E : constant Entity_Id := Subprogram_Body_Entity (E);
+
+ begin
+ if No (Body_E) then
+ return Empty;
+ else
+ return Parent (Subprogram_Specification (Body_E));
+ end if;
+ end Subprogram_Body;
+
+ ----------------------------
+ -- Subprogram_Body_Entity --
+ ----------------------------
+
+ function Subprogram_Body_Entity (E : Entity_Id) return Entity_Id is
+ N : Node_Id;
+
+ begin
+ -- Retrieve the declaration for E
+
+ N := Parent (Subprogram_Specification (E));
+
+ -- If this declaration is not a subprogram body, then it must be a
+ -- subprogram declaration, from which we can retrieve the entity for
+ -- the corresponding subprogram body if any.
+
+ if Nkind (N) = N_Subprogram_Body then
+ return E;
+ else
+ return Corresponding_Body (N);
+ end if;
+ end Subprogram_Body_Entity;
+
+ ---------------------
+ -- Subprogram_Spec --
+ ---------------------
+
+ function Subprogram_Spec (E : Entity_Id) return Node_Id is
+ N : Node_Id;
+
+ begin
+ -- Retrieve the declaration for E
+
+ N := Parent (Subprogram_Specification (E));
+
+ -- This declaration is either subprogram declaration or a subprogram
+ -- body, in which case return Empty.
+
+ if Nkind (N) = N_Subprogram_Declaration then
+ return N;
+ else
+ return Empty;
+ end if;
+ end Subprogram_Spec;
+
+ ------------------------------
+ -- Subprogram_Specification --
+ ------------------------------
+
+ function Subprogram_Specification (E : Entity_Id) return Node_Id is
+ N : Node_Id;
+
+ begin
+ N := Parent (E);
+
+ if Nkind (N) = N_Defining_Program_Unit_Name then
+ N := Parent (N);
+ end if;
+
+ -- If the Parent pointer of E is not a subprogram specification node
+ -- (going through an intermediate N_Defining_Program_Unit_Name node
+ -- for subprogram units), then E is an inherited operation. Its parent
+ -- points to the type derivation that produces the inheritance: that's
+ -- the node that generates the subprogram specification. Its alias
+ -- is the parent subprogram, and that one points to a subprogram
+ -- declaration, or to another type declaration if this is a hierarchy
+ -- of derivations.
+
+ if Nkind (N) not in N_Subprogram_Specification then
+ pragma Assert (Present (Alias (E)));
+ N := Subprogram_Specification (Alias (E));
+ end if;
+
+ return N;
+ end Subprogram_Specification;
+
---------------
-- Tree_Read --
---------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, 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- --
-- referencing this entity. It is an error to call this function if Ekind
-- (Op) /= E_Operator.
+ function Get_Low_Bound (E : Entity_Id) return Node_Id;
+ -- For an index subtype or string literal subtype, return its low bound
+
function Get_Unary_Nkind (Op : Entity_Id) return Node_Kind;
-- Op must be an entity with an Ekind of E_Operator. This function returns
-- the Nkind value that would be used to construct a unary operator node
-- The result returned is the next _Tag field in this record, or Empty
-- if this is the last such field.
+ function Number_Components (Typ : Entity_Id) return Pos;
+ -- Typ is a record type, yields number of components (including
+ -- discriminants) in type.
+
function Number_Discriminants (Typ : Entity_Id) return Pos;
-- Typ is a type with discriminants, yields number of discriminants in type
-- derived type, and the subtype is not an unconstrained array subtype
-- (RM 3.3(23.10/3)).
+ function Package_Specification (Pack_Id : Entity_Id) return Node_Id;
+ -- Given an entity for a package or generic package, return corresponding
+ -- package specification. Simplifies handling of child units, and better
+ -- than the old idiom: Specification (Unit_Declaration_Node (Pack_Id)).
+
+ function Subprogram_Body (E : Entity_Id) return Node_Id;
+ -- Given an entity for a subprogram (spec or body), return the
+ -- corresponding subprogram body if any, or else Empty.
+
+ function Subprogram_Body_Entity (E : Entity_Id) return Entity_Id;
+ -- Given an entity for a subprogram (spec or body), return the entity
+ -- corresponding to the subprogram body, which may be the same as E or
+ -- Empty if no body is available.
+
+ function Subprogram_Spec (E : Entity_Id) return Node_Id;
+ -- Given an entity for a subprogram spec, return the corresponding
+ -- subprogram spec if any, or else Empty.
+
+ function Subprogram_Specification (E : Entity_Id) return Node_Id;
+ -- Given an entity for a subprogram, return the corresponding subprogram
+ -- specification. If the entity is an inherited subprogram without
+ -- specification itself, return the specification of the inherited
+ -- subprogram.
+
function Ultimate_Alias (Prim : Entity_Id) return Entity_Id;
pragma Inline (Ultimate_Alias);
-- Return the last entity in the chain of aliased entities of Prim. If Prim
-- it returns the subprogram, task or protected body node for it. The unit
-- may be a child unit with any number of ancestors.
- function Package_Specification (Pack_Id : Entity_Id) return Node_Id;
- -- Given an entity for a package or generic package, return corresponding
- -- package specification. Simplifies handling of child units, and better
- -- than the old idiom: Specification (Unit_Declaration_Node (Pack_Id)).
-
end Sem_Aux;
end if;
end Is_Inherited_Public_Operation;
+ ------------------------------
+ -- Is_Overriding_Subprogram --
+ ------------------------------
+
+ function Is_Overriding_Subprogram (E : Entity_Id) return Boolean is
+ Inherited : constant Subprogram_List := Inherited_Subprograms (E);
+ begin
+ return Inherited'Length > 0;
+ end Is_Overriding_Subprogram;
+
--------------------------
-- Is_Tag_Indeterminate --
--------------------------
function Is_Null_Interface_Primitive (E : Entity_Id) return Boolean;
-- Returns True if E is a null procedure that is an interface primitive
+ function Is_Overriding_Subprogram (E : Entity_Id) return Boolean;
+ -- Returns True if E is an overriding subprogram
+
function Is_Tag_Indeterminate (N : Node_Id) return Boolean;
-- Returns true if the expression N is tag-indeterminate. An expression
-- is tag-indeterminate if it is a call that dispatches on result, and all
end if;
end Enclosing_Comp_Unit_Node;
+ -----------------------------
+ -- Enclosing_Lib_Unit_Node --
+ -----------------------------
+
+ function Enclosing_Lib_Unit_Node (N : Node_Id) return Node_Id is
+ Encl_Unit : Node_Id;
+
+ begin
+ Encl_Unit := Enclosing_Comp_Unit_Node (N);
+
+ while Present (Encl_Unit)
+ and then Nkind (Unit (Encl_Unit)) = N_Subunit
+ loop
+ Encl_Unit := Library_Unit (Encl_Unit);
+ end loop;
+
+ return Encl_Unit;
+ end Enclosing_Lib_Unit_Node;
+
--------------------------
-- Enclosing_CPP_Parent --
--------------------------
return Cursor;
end Get_Cursor_Type;
+ function Get_Cursor_Type (Typ : Entity_Id) return Entity_Id is
+ begin
+ return Etype (Get_Iterable_Type_Primitive (Typ, Name_First));
+ end Get_Cursor_Type;
+
-------------------------------
-- Get_Default_External_Name --
-------------------------------
return R;
end Get_Renamed_Entity;
- -------------------------
- -- Get_Subprogram_Body --
- -------------------------
+ -----------------------
+ -- Get_Return_Object --
+ -----------------------
- function Get_Subprogram_Body (E : Entity_Id) return Node_Id is
+ function Get_Return_Object (N : Node_Id) return Entity_Id is
Decl : Node_Id;
begin
- Decl := Unit_Declaration_Node (E);
-
- if Nkind (Decl) = N_Subprogram_Body then
- return Decl;
-
- -- The below comment is bad, because it is possible for
- -- Nkind (Decl) to be an N_Subprogram_Body_Stub ???
-
- else -- Nkind (Decl) = N_Subprogram_Declaration
-
- if Present (Corresponding_Body (Decl)) then
- return Unit_Declaration_Node (Corresponding_Body (Decl));
-
- -- Imported subprogram case
+ Decl := First (Return_Object_Declarations (N));
+ while Present (Decl) loop
+ exit when Nkind (Decl) = N_Object_Declaration
+ and then Is_Return_Object (Defining_Identifier (Decl));
+ Next (Decl);
+ end loop;
- else
- return Empty;
- end if;
- end if;
- end Get_Subprogram_Body;
+ pragma Assert (Present (Decl));
+ return Defining_Identifier (Decl);
+ end Get_Return_Object;
---------------------------
-- Get_Subprogram_Entity --
return Task_Body_Procedure (Underlying_Type (Root_Type (E)));
end Get_Task_Body_Procedure;
+ -------------------------
+ -- Get_User_Defined_Eq --
+ -------------------------
+
+ function Get_User_Defined_Eq (E : Entity_Id) return Entity_Id is
+ Prim : Elmt_Id;
+ Op : Entity_Id;
+
+ begin
+ Prim := First_Elmt (Collect_Primitive_Operations (E));
+ while Present (Prim) loop
+ Op := Node (Prim);
+
+ if Chars (Op) = Name_Op_Eq
+ and then Etype (Op) = Standard_Boolean
+ and then Etype (First_Formal (Op)) = E
+ and then Etype (Next_Formal (First_Formal (Op))) = E
+ then
+ return Op;
+ end if;
+
+ Next_Elmt (Prim);
+ end loop;
+
+ return Empty;
+ end Get_User_Defined_Eq;
+
-----------------------
-- Has_Access_Values --
-----------------------
end if;
end Is_Descendent_Of;
+ ---------------------------------------------
+ -- Is_Double_Precision_Floating_Point_Type --
+ ---------------------------------------------
+
+ function Is_Double_Precision_Floating_Point_Type
+ (E : Entity_Id) return Boolean is
+ begin
+ return Is_Floating_Point_Type (E)
+ and then Machine_Radix_Value (E) = Uint_2
+ and then Machine_Mantissa_Value (E) = UI_From_Int (53)
+ and then Machine_Emax_Value (E) = Uint_2 ** Uint_10
+ and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_10);
+ end Is_Double_Precision_Floating_Point_Type;
+
-----------------------------
-- Is_Effectively_Volatile --
-----------------------------
end if;
end Is_Selector_Name;
+ ---------------------------------------------
+ -- Is_Single_Precision_Floating_Point_Type --
+ ---------------------------------------------
+
+ function Is_Single_Precision_Floating_Point_Type
+ (E : Entity_Id) return Boolean is
+ begin
+ return Is_Floating_Point_Type (E)
+ and then Machine_Radix_Value (E) = Uint_2
+ and then Machine_Mantissa_Value (E) = Uint_24
+ and then Machine_Emax_Value (E) = Uint_2 ** Uint_7
+ and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_7);
+ end Is_Single_Precision_Floating_Point_Type;
+
-------------------------------------
-- Is_SPARK_05_Initialization_Expr --
-------------------------------------
-- related expression evaluates to True.
function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id;
- -- Returns the enclosing N_Compilation_Unit Node that is the root of a
+ -- Returns the enclosing N_Compilation_Unit node that is the root of a
-- subtree containing N.
+ function Enclosing_Lib_Unit_Node (N : Node_Id) return Node_Id;
+ -- Returns the N_Compilation_Unit node of the library unit that is directly
+ -- or indirectly (through a subunit) at the root of a subtree containing
+ -- N. This may be either the same as Enclosing_Comp_Unit_Node, or if
+ -- Enclosing_Comp_Unit_Node returns a subunit, then the corresponding
+ -- library unit.
+
function Enclosing_CPP_Parent (Typ : Entity_Id) return Entity_Id;
-- Returns the closest ancestor of Typ that is a CPP type.
function Get_Cursor_Type
(Aspect : Node_Id;
Typ : Entity_Id) return Entity_Id;
- -- Find Cursor type in scope of formal container Typ, by locating primitive
- -- operation First. For use in resolving the other primitive operations
- -- of an Iterable type and expanding loops and quantified expressions
- -- over formal containers.
+ -- Find Cursor type in scope of type Typ with Iterable aspect, by locating
+ -- primitive operation First. For use in resolving the other primitive
+ -- operations of an Iterable type and expanding loops and quantified
+ -- expressions over formal containers.
+
+ function Get_Cursor_Type (Typ : Entity_Id) return Entity_Id;
+ -- Find Cursor type in scope of type Typ with Iterable aspect, by locating
+ -- primitive operation First. For use after resolving the primitive
+ -- operations of an Iterable type.
function Get_Default_External_Name (E : Node_Or_Entity_Id) return Node_Id;
-- This is used to construct the string literal node representing a
-- not a renamed entity, returns its argument. It is an error to call this
-- with any other kind of entity.
+ function Get_Return_Object (N : Node_Id) return Entity_Id;
+ -- Given an extended return statement, return the corresponding return
+ -- object, identified as the one for which Is_Return_Object = True.
+
function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id;
-- Nod is either a procedure call statement, or a function call, or an
-- accept statement node. This procedure finds the Entity_Id of the related
-- subprogram or entry and returns it, or if no subprogram can be found,
-- returns Empty.
- function Get_Subprogram_Body (E : Entity_Id) return Node_Id;
- -- Given the entity for a subprogram (E_Function or E_Procedure), return
- -- the corresponding N_Subprogram_Body node. If the corresponding body
- -- is missing (as for an imported subprogram), return Empty.
-
function Get_Task_Body_Procedure (E : Entity_Id) return Node_Id;
pragma Inline (Get_Task_Body_Procedure);
-- Given an entity for a task type or subtype, retrieves the
-- Task_Body_Procedure field from the corresponding task type declaration.
+ function Get_User_Defined_Eq (E : Entity_Id) return Entity_Id;
+ -- For a type entity, return the entity of the primitive equality function
+ -- for the type if it exists, otherwise return Empty.
+
function Has_Access_Values (T : Entity_Id) return Boolean;
-- Returns true if type or subtype T is an access type, or has a component
-- (at any recursive level) that is an access type. This is a conservative
-- This is the RM definition, a type is a descendent of another type if it
-- is the same type or is derived from a descendent of the other type.
+ function Is_Double_Precision_Floating_Point_Type
+ (E : Entity_Id) return Boolean;
+ -- Return whether E is a double precision floating point type,
+ -- characterized by:
+ -- . machine_radix = 2
+ -- . machine_mantissa = 53
+ -- . machine_emax = 2**10
+ -- . machine_emin = 3 - machine_emax
+
function Is_Effectively_Volatile (Id : Entity_Id) return Boolean;
-- The SPARK property "effectively volatile" applies to both types and
-- objects. To qualify as such, an entity must be either volatile or be
-- represent use of the N_Identifier node for a true identifier, when
-- normally such nodes represent a direct name.
+ function Is_Single_Precision_Floating_Point_Type
+ (E : Entity_Id) return Boolean;
+ -- Return whether E is a single precision floating point type,
+ -- characterized by:
+ -- . machine_radix = 2
+ -- . machine_mantissa = 24
+ -- . machine_emax = 2**7
+ -- . machine_emin = 3 - machine_emax
+
function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an initialization
-- expression in SPARK 2005, suitable for initializing an object in an
projects / gcc.git / commitdiff