diff mbox series

[COMMITTED,20/35] ada: Expose utility routine for processing of Depends contracts in SPARK

Message ID 20240517083207.130391-20-poulhies@adacore.com
State New
Headers show
Series [COMMITTED,01/35] ada: Add support for 'Object_Size to pragma Compile_Time_{Warning, Error} | expand

Commit Message

Marc Poulhiès May 17, 2024, 8:31 a.m. UTC
From: Piotr Trojanek <trojanek@adacore.com>

Routine Is_Unconstrained_Or_Tagged_Item is now used both in the GNAT
frontend (for checking legality of Depends clauses) and in the GNATprove
backend (for representing implicit inputs in flow graphs).

gcc/ada/

	* sem_prag.adb (Is_Unconstrained_Or_Tagged_Item): Move to
	Sem_Util, so it can be used from GNATprove.
	* sem_util.ads (Is_Unconstrained_Or_Tagged_Item): Move from
	Sem_Prag; spec.
	* sem_util.adb (Is_Unconstrained_Or_Tagged_Item): Move from
	Sem_Prag; body.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/sem_prag.adb | 29 -----------------------------
 gcc/ada/sem_util.adb | 23 +++++++++++++++++++++++
 gcc/ada/sem_util.ads |  5 +++++
 3 files changed, 28 insertions(+), 29 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 02aad4d1caa..f27e40edcbb 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -280,12 +280,6 @@  package body Sem_Prag is
    --  Determine whether dependency clause Clause is surrounded by extra
    --  parentheses. If this is the case, issue an error message.
 
-   function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean;
-   --  Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of
-   --  pragma Depends. Determine whether the type of dependency item Item is
-   --  tagged, unconstrained array, unconstrained private or unconstrained
-   --  record.
-
    procedure Record_Possible_Body_Reference
      (State_Id : Entity_Id;
       Ref      : Node_Id);
@@ -32959,29 +32953,6 @@  package body Sem_Prag is
           and then List_Containing (N) = Private_Declarations (Parent (N));
    end Is_Private_SPARK_Mode;
 
-   -------------------------------------
-   -- Is_Unconstrained_Or_Tagged_Item --
-   -------------------------------------
-
-   function Is_Unconstrained_Or_Tagged_Item
-     (Item : Entity_Id) return Boolean
-   is
-      Typ : constant Entity_Id := Etype (Item);
-   begin
-      if Is_Tagged_Type (Typ) then
-         return True;
-
-      elsif Is_Array_Type (Typ)
-        or else Is_Record_Type (Typ)
-        or else Is_Private_Type (Typ)
-      then
-         return not Is_Constrained (Typ);
-
-      else
-         return False;
-      end if;
-   end Is_Unconstrained_Or_Tagged_Item;
-
    -----------------------------
    -- Is_Valid_Assertion_Kind --
    -----------------------------
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index dd9f868b696..be777d26e46 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -20709,6 +20709,29 @@  package body Sem_Util is
       return T = Universal_Integer or else T = Universal_Real;
    end Is_Universal_Numeric_Type;
 
+   -------------------------------------
+   -- Is_Unconstrained_Or_Tagged_Item --
+   -------------------------------------
+
+   function Is_Unconstrained_Or_Tagged_Item
+     (Item : Entity_Id) return Boolean
+   is
+      Typ : constant Entity_Id := Etype (Item);
+   begin
+      if Is_Tagged_Type (Typ) then
+         return True;
+
+      elsif Is_Array_Type (Typ)
+        or else Is_Record_Type (Typ)
+        or else Is_Private_Type (Typ)
+      then
+         return not Is_Constrained (Typ);
+
+      else
+         return False;
+      end if;
+   end Is_Unconstrained_Or_Tagged_Item;
+
    ------------------------------
    -- Is_User_Defined_Equality --
    ------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 99c60ddf708..4fef8966380 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -2397,6 +2397,11 @@  package Sem_Util is
    pragma Inline (Is_Universal_Numeric_Type);
    --  True if T is Universal_Integer or Universal_Real
 
+   function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean;
+   --  Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of
+   --  pragma Depends. Determine whether the type of dependency item Item is
+   --  tagged, unconstrained array or unconstrained record.
+
    function Is_User_Defined_Equality (Id : Entity_Id) return Boolean;
    --  Determine whether an entity denotes a user-defined equality