inline.adb (Has_Initialized_Type): Adapt to new names.

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.

From-SVN: r223674

8 files changed, 328 insertions, 40 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 457b146..960a118 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+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
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index cf53aae..b36ec52 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -3639,7 +3639,7 @@ package body Inline is
    --------------------------
 
    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
diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb
index a6ba49f..63f74d9 100644
--- a/gcc/ada/sem_aux.adb
+++ b/gcc/ada/sem_aux.adb
@@ -472,6 +472,19 @@ package body Sem_Aux is
       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 --
    ------------------
@@ -1361,6 +1374,35 @@ package body Sem_Aux is
       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 --
    --------------------------
@@ -1419,6 +1461,97 @@ package body Sem_Aux is
       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 --
    ---------------
diff --git a/gcc/ada/sem_aux.ads b/gcc/ada/sem_aux.ads
index bb539e2..e3117f2 100644
--- a/gcc/ada/sem_aux.ads
+++ b/gcc/ada/sem_aux.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 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- --
@@ -158,6 +158,9 @@ package Sem_Aux is
    --  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
@@ -369,6 +372,10 @@ package Sem_Aux is
    --  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
 
@@ -381,6 +388,30 @@ package Sem_Aux is
    --  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
@@ -393,9 +424,4 @@ package Sem_Aux is
    --  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;
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index 55e5dcd..52eda74 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -2239,6 +2239,16 @@ package body Sem_Disp is
       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 --
    --------------------------
diff --git a/gcc/ada/sem_disp.ads b/gcc/ada/sem_disp.ads
index 21d1da5..d2aa620 100644
--- a/gcc/ada/sem_disp.ads
+++ b/gcc/ada/sem_disp.ads
@@ -129,6 +129,9 @@ package Sem_Disp is
    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
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 2bf22f6..99bf2ba 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -5674,6 +5674,25 @@ package body Sem_Util is
       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 --
    --------------------------
@@ -7417,6 +7436,11 @@ package body Sem_Util is
       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 --
    -------------------------------
@@ -7771,34 +7795,24 @@ package body Sem_Util is
       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 --
@@ -7878,6 +7892,33 @@ package body Sem_Util is
       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 --
    -----------------------
@@ -11242,6 +11283,20 @@ package body Sem_Util is
       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 --
    -----------------------------
@@ -12703,6 +12758,20 @@ package body Sem_Util is
       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 --
    -------------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index cf74bf7..8394b10 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -529,9 +529,16 @@ package Sem_Util is
    --  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.
 
@@ -814,10 +821,15 @@ package Sem_Util is
    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
@@ -906,22 +918,25 @@ package Sem_Util is
    --  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
@@ -1248,6 +1263,15 @@ package Sem_Util is
    --  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
@@ -1410,6 +1434,15 @@ package Sem_Util is
    --  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