[Ada] Move routine for detecting special Text_IO packages from GNATprove

Message ID 20200605122338.GA56687@adacore.com
State New
Headers show
Series
  • [Ada] Move routine for detecting special Text_IO packages from GNATprove
Related show

Commit Message

Pierre-Marie de Rodat June 5, 2020, 12:23 p.m.
In GNATprove we were detecting special Text_IO packages by looking at
the Ada[_Wide[_Wide]]_Text_IO_Child subtypes provided by the frontend
Rtsfind spec. However, it seems more elegant to hide those subtypes in
the Rtsfind body and only expose a single query routine. This patch
implements this routine; another patch will move the subtype declaration
into body.

Tested on x86_64-pc-linux-gnu, committed on trunk

2020-06-05  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* rtsfind.ads, rtsfind.adb (Is_Text_IO_Special_Package): Moved
	from the GNATprove backend to the frontend.

Patch

--- gcc/ada/rtsfind.adb
+++ gcc/ada/rtsfind.adb
@@ -759,6 +759,37 @@  package body Rtsfind is
       return Present (E) and then E = Ent;
    end Is_RTU;
 
+   --------------------------------
+   -- Is_Text_IO_Special_Package --
+   --------------------------------
+
+   function Is_Text_IO_Special_Package (E : Entity_Id) return Boolean is
+   begin
+      pragma Assert (Is_Package_Or_Generic_Package (E));
+
+      --  ??? detection with a scope climbing might be more efficient
+
+      for U in Ada_Text_IO_Child loop
+         if Is_RTU (E, U) then
+            return True;
+         end if;
+      end loop;
+
+      for U in Ada_Wide_Text_IO_Child loop
+         if Is_RTU (E, U) then
+            return True;
+         end if;
+      end loop;
+
+      for U in Ada_Wide_Wide_Text_IO_Child loop
+         if Is_RTU (E, U) then
+            return True;
+         end if;
+      end loop;
+
+      return False;
+   end Is_Text_IO_Special_Package;
+
    -----------------------------
    -- Is_Text_IO_Special_Unit --
    -----------------------------

--- gcc/ada/rtsfind.ads
+++ gcc/ada/rtsfind.ads
@@ -3188,6 +3188,12 @@  package Rtsfind is
    --  Wide_Wide_Text_IO.xxx, where xxx is one of the subpackages of Text_IO
    --  that is specially handled as described for Check_Text_IO_Special_Unit.
 
+   function Is_Text_IO_Special_Package (E : Entity_Id) return Boolean;
+   --  Return True iff E is one of the special generic Text_IO packages, which
+   --  Ada RM defines to be nested in Ada.Text_IO, but GNAT defines as its
+   --  private children. This is similar to Is_Text_IO_Special_Unit, but is
+   --  meant to be used on a fully resolved AST, especially in the backends.
+
    function RTE (E : RE_Id) return Entity_Id;
    --  Given the entity defined in the above tables, as identified by the
    --  corresponding value in the RE_Id enumeration type, returns the Id of the