Patchwork [Ada] Extra semantic rules for aspect Abstract_State and aspect Global

login
register
mail settings
Submitter Arnaud Charlet
Date April 25, 2013, 10:35 a.m.
Message ID <20130425103537.GA10045@adacore.com>
Download mbox | patch
Permalink /patch/239479/
State New
Headers show

Comments

Arnaud Charlet - April 25, 2013, 10:35 a.m.
This patch implements the following formal verification rules:

A package_declaration of generic_package_declaration shall have a completion (a
body) if it contains a non-null Abstract_State aspect specification.

If a subprogram is nested within another and if the Global aspect specification
of the outer subprogram has an entity denoted by a global_item with a
mode_specification of Input, then a global_item of the Global aspect
specification of the inner subprogram shall not denote the same entity with a
mode_selector of In_Out or Out.

------------
-- Source --
------------

--  completion.ads

package Completion is
   package OK_1 with Abstract_State => null is
   end OK_1;

   package OK_2 with Abstract_State => State_OK_2 is
   end OK_2;

   package Error_1 with Abstract_State => State_Error_1 is
   end Error_1;

   generic
      type Formal_Typ is private;
   package OK_3 with Abstract_State => null is
   end OK_3;

   generic
      type Formal_Typ is private;
   package OK_4 with Abstract_State => State_OK_4 is
   end OK_4;

   generic
      type Formal_Typ is private;
   package Error_2 with Abstract_State => State_Error_2 is
   end Error_2;
end Completion;

--  completion.adb

package body Completion is
   package body OK_2 is end OK_2;
   package body OK_4 is end OK_4;
end Completion;

--  nesting.ads

package Nesting
   with Abstract_State => ((Input_State  with Volatile, Input),
                           (Output_State with Volatile, Output))
is
   Input_Var  : Integer;
   Mixed_Var  : Integer;
   Output_Var : Integer;
end Nesting;

--  nesting.adb

package body Nesting is
   procedure Outer
   with Global =>
          (Input  => (Input_State,  Input_Var),
           Output => (Output_State, Output_Var),
           In_Out =>  Mixed_Var);

   procedure Outer is
      procedure OK_1
      with Global => (Output => (Mixed_Var, Output_State, Output_Var));

      procedure OK_2
      with Global => (In_Out => Mixed_Var);

      procedure Error_1
      with Global => (Output => (Input_State, Input_Var));

      procedure Error_2
      with Global => (In_Out => (Input_State, Input_Var));

      procedure OK_1 is begin null; end OK_1;
      procedure OK_2 is begin null; end OK_2;
      procedure Error_1 is begin null; end Error_1;
      procedure Error_2 is begin null; end Error_2;
   begin
      null;
   end Outer;
end Nesting;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnat12 -gnatd.V completion.adb
$ gcc -c -gnat12 -gnatd.V nesting.adb
completion.adb:1:14: missing body for "Error_1" declared at completion.ads:8
completion.adb:1:14: missing body for "Error_2" declared at completion.ads:23
nesting.adb:16:34: global item of mode In_Out or Output cannot reference
  Volatile Input state
nesting.adb:16:47: global item "Input_Var" cannot have mode In_Out or Output
nesting.adb:16:47: item already appears as input of subprogram "Outer"
nesting.adb:19:34: global item of mode In_Out or Output cannot reference
  Volatile Input state
nesting.adb:19:47: global item "Input_Var" cannot have mode In_Out or Output
nesting.adb:19:47: item already appears as input of subprogram "Outer"

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

2013-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Set_Abstract_States): The attribute now applies
	to generic packages.
	* sem_ch4.adb (Referenced): Moved to sem_util.
	* sem_ch7.adb (Unit_Requires_Body): A [generic] package with
	a non-null abstract state needs a body.
	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Update the calls
	to Collect_Subprogram_Inputs_Outputs.
	(Analyze_Global_Item): Verify the proper usage of an item with mode
	In_Out or Output relative to the enclosing context.
	(Analyze_Pragma): Abstract_State can now be applied to a generic
	package. Do not reset the Analyzed flag for pragmas Depends and Global
	as this is not needed.
	(Appears_In): Moved to library level.
	(Check_Mode_Restiction_In_Enclosing_Context): New routine.
	(Collect_Subprogram_Inputs_Outputs): Moved to library level. Add
	formal parameters Subp_Id, Subp_Inputs, Subp_Outputs and Global
	seen along with comments on usage.
	* sem_util.ads, sem_util.adb (Referenced): New routine.

Patch

Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 198281)
+++ sem_ch7.adb	(working copy)
@@ -2615,6 +2615,16 @@ 
                return True;
             end if;
          end;
+
+      --  A [generic] package that introduces at least one non-null abstract
+      --  state requires completion. A null abstract state always appears as
+      --  the sole element of the state list.
+
+      elsif Ekind_In (P, E_Generic_Package, E_Package)
+        and then Present (Abstract_States (P))
+        and then not Is_Null_State (Node (First_Elmt (Abstract_States (P))))
+      then
+         return True;
       end if;
 
       --  Otherwise search entity chain for entity requiring completion
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 198287)
+++ einfo.adb	(working copy)
@@ -3233,7 +3233,7 @@ 
 
    procedure Set_Abstract_States (Id : E; V : L) is
    begin
-      pragma Assert (Ekind (Id) = E_Package);
+      pragma Assert (Ekind_In (Id, E_Generic_Package, E_Package));
       Set_Elist25 (Id, V);
    end Set_Abstract_States;
 
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 198287)
+++ sem_prag.adb	(working copy)
@@ -181,6 +181,22 @@ 
    --  to Uppercase or Lowercase, then a new string literal with appropriate
    --  casing is constructed.
 
+   function Appears_In (List : Elist_Id; Item_Id : Entity_Id) return Boolean;
+   --  Subsidiary to the analysis of pragma Global and pragma Depends. Query
+   --  whether a particular item appears in a mixed list of nodes and entities.
+   --  It is assumed that all nodes in the list have entities.
+
+   procedure Collect_Subprogram_Inputs_Outputs
+     (Subp_Id      : Entity_Id;
+      Subp_Inputs  : in out Elist_Id;
+      Subp_Outputs : in out Elist_Id;
+      Global_Seen  : out Boolean);
+   --  Subsidiary to the analysis of pragma Global and pragma Depends. Gather
+   --  all inputs and outputs of subprogram Subp_Id in lists Subp_Inputs and
+   --  Subp_Outputs. If the case where the subprogram has no inputs and/or
+   --  outputs, the corresponding returned list is No_Elist. Flag Global_Seen
+   --  is set when the related subprogram has aspect/pragma Global.
+
    function Find_Related_Subprogram
      (Prag             : Node_Id;
       Check_Duplicates : Boolean := False) return Node_Id;
@@ -448,12 +464,6 @@ 
       --  Verify the legality of a single dependency clause. Flag Is_Last
       --  denotes whether Clause is the last clause in the relation.
 
-      function Appears_In
-        (List    : Elist_Id;
-         Item_Id : Entity_Id) return Boolean;
-      --  Determine whether a particular item appears in a mixed list of nodes
-      --  and entities.
-
       procedure Check_Function_Return;
       --  Verify that Funtion'Result appears as one of the outputs
 
@@ -476,10 +486,6 @@ 
       --  Verify that all items from Subp_Items appear in Used_Items. Emit an
       --  error if this is not the case.
 
-      procedure Collect_Subprogram_Inputs_Outputs;
-      --  Gather all inputs and outputs of the subprogram. These are the formal
-      --  parameters and entities classified in pragma Global.
-
       procedure Normalize_Clause (Clause : Node_Id);
       --  Remove a self-dependency "+" from the input list of a clause.
       --  Depending on the contents of the relation, either split the the
@@ -787,38 +793,6 @@ 
          Analyze_Input_List (Inputs);
       end Analyze_Dependency_Clause;
 
-      ----------------
-      -- Appears_In --
-      ----------------
-
-      function Appears_In
-        (List    : Elist_Id;
-         Item_Id : Entity_Id) return Boolean
-      is
-         Elmt : Elmt_Id;
-         Id   : Entity_Id;
-
-      begin
-         if Present (List) then
-            Elmt := First_Elmt (List);
-            while Present (Elmt) loop
-               if Nkind (Node (Elmt)) = N_Defining_Identifier then
-                  Id := Node (Elmt);
-               else
-                  Id := Entity (Node (Elmt));
-               end if;
-
-               if Id = Item_Id then
-                  return True;
-               end if;
-
-               Next_Elmt (Elmt);
-            end loop;
-         end if;
-
-         return False;
-      end Appears_In;
-
       ----------------------------
       --  Check_Function_Return --
       ----------------------------
@@ -961,138 +935,6 @@ 
          end loop;
       end Check_Usage;
 
-      ---------------------------------------
-      -- Collect_Subprogram_Inputs_Outputs --
-      ---------------------------------------
-
-      procedure Collect_Subprogram_Inputs_Outputs is
-         procedure Collect_Global_List
-           (List : Node_Id;
-            Mode : Name_Id := Name_Input);
-         --  Collect all relevant items from a global list
-
-         -------------------------
-         -- Collect_Global_List --
-         -------------------------
-
-         procedure Collect_Global_List
-           (List : Node_Id;
-            Mode : Name_Id := Name_Input)
-         is
-            procedure Collect_Global_Item
-              (Item : Node_Id;
-               Mode : Name_Id);
-            --  Add an item to the proper subprogram input or output collection
-
-            -------------------------
-            -- Collect_Global_Item --
-            -------------------------
-
-            procedure Collect_Global_Item
-              (Item : Node_Id;
-               Mode : Name_Id)
-            is
-            begin
-               if Nam_In (Mode, Name_In_Out, Name_Input) then
-                  Add_Item (Item, Subp_Inputs);
-               end if;
-
-               if Nam_In (Mode, Name_In_Out, Name_Output) then
-                  Add_Item (Item, Subp_Outputs);
-               end if;
-            end Collect_Global_Item;
-
-            --  Local variables
-
-            Assoc : Node_Id;
-            Item  : Node_Id;
-
-         --  Start of processing for Collect_Global_List
-
-         begin
-            --  Single global item declaration
-
-            if Nkind_In (List, N_Identifier, N_Selected_Component) then
-               Collect_Global_Item (List, Mode);
-
-            --  Simple global list or moded global list declaration
-
-            else
-               if Present (Expressions (List)) then
-                  Item := First (Expressions (List));
-                  while Present (Item) loop
-                     Collect_Global_Item (Item, Mode);
-
-                     Next (Item);
-                  end loop;
-
-               else
-                  Assoc := First (Component_Associations (List));
-                  while Present (Assoc) loop
-                     Collect_Global_List
-                       (List => Expression (Assoc),
-                        Mode => Chars (First (Choices (Assoc))));
-
-                     Next (Assoc);
-                  end loop;
-               end if;
-            end if;
-         end Collect_Global_List;
-
-         --  Local variables
-
-         Formal : Entity_Id;
-         Global : Node_Id;
-         List   : Node_Id;
-
-      --  Start of processing for Collect_Subprogram_Inputs_Outputs
-
-      begin
-         --  Process all formal parameters
-
-         Formal := First_Formal (Subp_Id);
-         while Present (Formal) loop
-            if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then
-               Add_Item (Formal, Subp_Inputs);
-            end if;
-
-            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
-               Add_Item (Formal, Subp_Outputs);
-            end if;
-
-            Next_Formal (Formal);
-         end loop;
-
-         --  If the subprogram is subject to pragma Global, traverse all global
-         --  lists and gather the relevant items.
-
-         Global := Find_Aspect (Subp_Id, Aspect_Global);
-         if Present (Global) then
-            Global_Seen := True;
-
-            --  Retrieve the pragma as it contains the analyzed lists
-
-            Global := Aspect_Rep_Item (Global);
-
-            --  The pragma may not have been analyzed because of the arbitrary
-            --  declaration order of aspects. Make sure that it is analyzed for
-            --  the purposes of item extraction.
-
-            if not Analyzed (Global) then
-               Analyze_Global_In_Decl_Part (Global);
-            end if;
-
-            List :=
-              Expression (First (Pragma_Argument_Associations (Global)));
-
-            --  Nothing to be done for a null global list
-
-            if Nkind (List) /= N_Null then
-               Collect_Global_List (List);
-            end if;
-         end if;
-      end Collect_Subprogram_Inputs_Outputs;
-
       ----------------------
       -- Normalize_Clause --
       ----------------------
@@ -1382,7 +1224,11 @@ 
          --  subprogram may depend on. These items are obtained from the
          --  parameter profile or pragma Global (if available).
 
-         Collect_Subprogram_Inputs_Outputs;
+         Collect_Subprogram_Inputs_Outputs
+           (Subp_Id      => Subp_Id,
+            Subp_Inputs  => Subp_Inputs,
+            Subp_Outputs => Subp_Outputs,
+            Global_Seen  => Global_Seen);
 
          --  Verify that every input or output of the subprogram appear in a
          --  dependency.
@@ -1402,7 +1248,11 @@ 
          --  subprogram may depend on. These items are obtained from the
          --  parameter profile or pragma Global (if available).
 
-         Collect_Subprogram_Inputs_Outputs;
+         Collect_Subprogram_Inputs_Outputs
+           (Subp_Id      => Subp_Id,
+            Subp_Inputs  => Subp_Inputs,
+            Subp_Outputs => Subp_Outputs,
+            Global_Seen  => Global_Seen);
 
          --  Ensure that the formal parameters are visible when analyzing all
          --  clauses. This falls out of the general rule of aspects pertaining
@@ -1505,6 +1355,14 @@ 
          --  processing a global list. This routine verifies that Mode is not a
          --  duplicate mode and sets the flag Status.
 
+         procedure Check_Mode_Restiction_In_Enclosing_Context
+           (Item    : Node_Id;
+            Item_Id : Entity_Id);
+         --  Verify that an item of mode In_Out or Output does not appear as an
+         --  input in the Global aspect of an enclosing subprogram. If this is
+         --  the case, emit an error. Item and Item_Id are respectively the
+         --  item and its entity.
+
          procedure Check_Mode_Restriction_In_Function (Mode : Node_Id);
          --  Mode denotes either In_Out or Output. Depending on the kind of the
          --  related subprogram, emit an error if those two modes apply to a
@@ -1574,19 +1432,9 @@ 
                return;
             end if;
 
-            --  The same entity might be referenced through various way. Check
-            --  the entity of the item rather than the item itself.
+            --  At this point we know that the global item is one of the two
+            --  valid choices. Perform mode- and usage-specific checks.
 
-            if Contains (Seen, Item_Id) then
-               Error_Msg_N ("duplicate global item", Item);
-
-            --  Add the entity of the current item to the list of processed
-            --  items.
-
-            else
-               Add_Item (Item_Id, Seen);
-            end if;
-
             if Ekind (Item_Id) = E_Abstract_State
               and then Is_Volatile_State (Item_Id)
             then
@@ -1611,6 +1459,26 @@ 
                      & "Volatile Output state", Item);
                end if;
             end if;
+
+            --  Verify that an output does not appear as an input in an
+            --  enclosing subprogram.
+
+            if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
+               Check_Mode_Restiction_In_Enclosing_Context (Item, Item_Id);
+            end if;
+
+            --  The same entity might be referenced through various way. Check
+            --  the entity of the item rather than the item itself.
+
+            if Contains (Seen, Item_Id) then
+               Error_Msg_N ("duplicate global item", Item);
+
+            --  Add the entity of the current item to the list of processed
+            --  items.
+
+            else
+               Add_Item (Item_Id, Seen);
+            end if;
          end Analyze_Global_Item;
 
          --------------------------
@@ -1629,6 +1497,53 @@ 
             Status := True;
          end Check_Duplicate_Mode;
 
+         ------------------------------------------------
+         -- Check_Mode_Restiction_In_Enclosing_Context --
+         ------------------------------------------------
+
+         procedure Check_Mode_Restiction_In_Enclosing_Context
+           (Item    : Node_Id;
+            Item_Id : Entity_Id)
+         is
+            Dummy   : Boolean;
+            Inputs  : Elist_Id := No_Elist;
+            Outputs : Elist_Id := No_Elist;
+            Subp_Id : Entity_Id;
+
+         begin
+            --  Traverse the scope stack looking for enclosing subprograms
+            --  subject to aspect/pragma Global.
+
+            Subp_Id := Scope (Current_Scope);
+            while Present (Subp_Id) and then Subp_Id /= Standard_Standard loop
+               if Is_Subprogram (Subp_Id)
+                 and then Has_Aspect (Subp_Id, Aspect_Global)
+               then
+                  Collect_Subprogram_Inputs_Outputs
+                    (Subp_Id      => Subp_Id,
+                     Subp_Inputs  => Inputs,
+                     Subp_Outputs => Outputs,
+                     Global_Seen  => Dummy);
+
+                  --  The item is classified as In_Out or Output but appears as
+                  --  an Input in an enclosing subprogram.
+
+                  if Appears_In (Inputs, Item_Id)
+                    and then not Appears_In (Outputs, Item_Id)
+                  then
+                     Error_Msg_NE
+                       ("global item & cannot have mode In_Out or Output",
+                        Item, Item_Id);
+                     Error_Msg_NE
+                       ("\item already appears as input of subprogram &",
+                        Item, Subp_Id);
+                  end if;
+               end if;
+
+               Subp_Id := Scope (Subp_Id);
+            end loop;
+         end Check_Mode_Restiction_In_Enclosing_Context;
+
          ----------------------------------------
          -- Check_Mode_Restriction_In_Function --
          ----------------------------------------
@@ -8559,7 +8474,9 @@ 
                Par := Unit (Par);
             end if;
 
-            if Nkind (Par) /= N_Package_Declaration then
+            if not Nkind_In (Par, N_Generic_Package_Declaration,
+                                  N_Package_Declaration)
+            then
                Pragma_Misplaced;
                return;
             end if;
@@ -10660,11 +10577,6 @@ 
 
             Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
 
-            --  The pragma is analyzed at the end of the declarative part which
-            --  contains the related subprogram. Reset the analyzed flag.
-
-            Set_Analyzed (N, False);
-
             --  When the aspect/pragma appears on a subprogram body, perform
             --  the full analysis now.
 
@@ -11906,11 +11818,6 @@ 
 
             Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
 
-            --  The pragma is analyzed at the end of the declarative part which
-            --  contains the related subprogram. Reset the analyzed flag.
-
-            Set_Analyzed (N, False);
-
             --  When the aspect/pragma appears on a subprogram body, perform
             --  the full analysis now.
 
@@ -17895,6 +17802,35 @@ 
    end Analyze_Test_Case_In_Decl_Part;
 
    ----------------
+   -- Appears_In --
+   ----------------
+
+   function Appears_In (List : Elist_Id; Item_Id : Entity_Id) return Boolean is
+      Elmt : Elmt_Id;
+      Id   : Entity_Id;
+
+   begin
+      if Present (List) then
+         Elmt := First_Elmt (List);
+         while Present (Elmt) loop
+            if Nkind (Node (Elmt)) = N_Defining_Identifier then
+               Id := Node (Elmt);
+            else
+               Id := Entity (Node (Elmt));
+            end if;
+
+            if Id = Item_Id then
+               return True;
+            end if;
+
+            Next_Elmt (Elmt);
+         end loop;
+      end if;
+
+      return False;
+   end Appears_In;
+
+   ----------------
    -- Check_Kind --
    ----------------
 
@@ -18007,6 +17943,143 @@ 
       end if;
    end Check_Applicable_Policy;
 
+   ---------------------------------------
+   -- Collect_Subprogram_Inputs_Outputs --
+   ---------------------------------------
+
+   procedure Collect_Subprogram_Inputs_Outputs
+     (Subp_Id      : Entity_Id;
+      Subp_Inputs  : in out Elist_Id;
+      Subp_Outputs : in out Elist_Id;
+      Global_Seen  : out Boolean)
+   is
+      procedure Collect_Global_List
+        (List : Node_Id;
+         Mode : Name_Id := Name_Input);
+      --  Collect all relevant items from a global list
+
+      -------------------------
+      -- Collect_Global_List --
+      -------------------------
+
+      procedure Collect_Global_List
+        (List : Node_Id;
+         Mode : Name_Id := Name_Input)
+      is
+         procedure Collect_Global_Item
+           (Item : Node_Id;
+            Mode : Name_Id);
+         --  Add an item to the proper subprogram input or output collection
+
+         -------------------------
+         -- Collect_Global_Item --
+         -------------------------
+
+         procedure Collect_Global_Item
+           (Item : Node_Id;
+            Mode : Name_Id)
+         is
+         begin
+            if Nam_In (Mode, Name_In_Out, Name_Input) then
+               Add_Item (Item, Subp_Inputs);
+            end if;
+
+            if Nam_In (Mode, Name_In_Out, Name_Output) then
+               Add_Item (Item, Subp_Outputs);
+            end if;
+         end Collect_Global_Item;
+
+         --  Local variables
+
+         Assoc : Node_Id;
+         Item  : Node_Id;
+
+      --  Start of processing for Collect_Global_List
+
+      begin
+         --  Single global item declaration
+
+         if Nkind_In (List, N_Identifier, N_Selected_Component) then
+            Collect_Global_Item (List, Mode);
+
+         --  Simple global list or moded global list declaration
+
+         else
+            if Present (Expressions (List)) then
+               Item := First (Expressions (List));
+               while Present (Item) loop
+                  Collect_Global_Item (Item, Mode);
+
+                  Next (Item);
+               end loop;
+
+            else
+               Assoc := First (Component_Associations (List));
+               while Present (Assoc) loop
+                  Collect_Global_List
+                    (List => Expression (Assoc),
+                     Mode => Chars (First (Choices (Assoc))));
+
+                  Next (Assoc);
+               end loop;
+            end if;
+         end if;
+      end Collect_Global_List;
+
+      --  Local variables
+
+      Formal : Entity_Id;
+      Global : Node_Id;
+      List   : Node_Id;
+
+   --  Start of processing for Collect_Subprogram_Inputs_Outputs
+
+   begin
+      Global_Seen := False;
+
+      --  Process all formal parameters
+
+      Formal := First_Formal (Subp_Id);
+      while Present (Formal) loop
+         if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then
+            Add_Item (Formal, Subp_Inputs);
+         end if;
+
+         if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+            Add_Item (Formal, Subp_Outputs);
+         end if;
+
+         Next_Formal (Formal);
+      end loop;
+
+      --  If the subprogram is subject to pragma Global, traverse all global
+      --  lists and gather the relevant items.
+
+      Global := Find_Aspect (Subp_Id, Aspect_Global);
+      if Present (Global) then
+         Global_Seen := True;
+
+         --  Retrieve the pragma as it contains the analyzed lists
+
+         Global := Aspect_Rep_Item (Global);
+         List   := Expression (First (Pragma_Argument_Associations (Global)));
+
+         --  The pragma may not have been analyzed because of the arbitrary
+         --  declaration order of aspects. Make sure that it is analyzed for
+         --  the purposes of item extraction.
+
+         if not Analyzed (List) then
+            Analyze_Global_In_Decl_Part (Global);
+         end if;
+
+         --  Nothing to be done for a null global list
+
+         if Nkind (List) /= N_Null then
+            Collect_Global_List (List);
+         end if;
+      end if;
+   end Collect_Subprogram_Inputs_Outputs;
+
    ---------------------------------
    -- Delay_Config_Pragma_Analyze --
    ---------------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 198289)
+++ sem_util.adb	(working copy)
@@ -12964,6 +12964,40 @@ 
       Set_Sloc (Endl, Loc);
    end Process_End_Label;
 
+   ----------------
+   -- Referenced --
+   ----------------
+
+   function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean is
+      Seen : Boolean := False;
+
+      function Is_Reference (N : Node_Id) return Traverse_Result;
+      --  Determine whether node N denotes a reference to Id. If this is the
+      --  case, set global flag Seen to True and stop the traversal.
+
+      function Is_Reference (N : Node_Id) return Traverse_Result is
+      begin
+         if Is_Entity_Name (N)
+           and then Present (Entity (N))
+           and then Entity (N) = Id
+         then
+            Seen := True;
+            return Abandon;
+         else
+            return OK;
+         end if;
+      end Is_Reference;
+
+      procedure Inspect_Expression is new Traverse_Proc (Is_Reference);
+
+   --  Start of processing for Referenced
+
+   begin
+      Inspect_Expression (Expr);
+
+      return Seen;
+   end Referenced;
+
    ------------------------------------
    -- References_Generic_Formal_Type --
    ------------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 198288)
+++ sem_util.ads	(working copy)
@@ -1358,6 +1358,9 @@ 
    --  parameter Ent gives the entity to which the End_Label refers,
    --  and to which cross-references are to be generated.
 
+   function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean;
+   --  Determine whether entity Id is referenced within expression Expr
+
    function References_Generic_Formal_Type (N : Node_Id) return Boolean;
    --  Returns True if the expression Expr contains any references to a
    --  generic type. This can only happen within a generic template.
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 198289)
+++ sem_ch4.adb	(working copy)
@@ -3510,10 +3510,6 @@ 
       --  Determine whether if expression If_Expr lacks an else part or if it
       --  has one, it evaluates to True.
 
-      function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean;
-      --  Determine whether entity Id is referenced within expression Expr
-      --  This should be moved to sem_util ???
-
       --------------------
       -- Is_Empty_Range --
       --------------------
@@ -3565,43 +3561,6 @@ 
                        and then Is_True (Expr_Value (Else_Expr)));
       end No_Else_Or_Trivial_True;
 
-      ----------------
-      -- Referenced --
-      ----------------
-
-      function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean is
-         Seen : Boolean := False;
-
-         function Is_Reference (N : Node_Id) return Traverse_Result;
-         --  Determine whether node N denotes a reference to Id. If this is the
-         --  case, set global flag Seen to True and stop the traversal.
-
-         ------------------
-         -- Is_Reference --
-         ------------------
-
-         function Is_Reference (N : Node_Id) return Traverse_Result is
-         begin
-            if Is_Entity_Name (N)
-              and then Present (Entity (N))
-              and then Entity (N) = Id
-            then
-               Seen := True;
-               return Abandon;
-            else
-               return OK;
-            end if;
-         end Is_Reference;
-
-         procedure Inspect_Expression is new Traverse_Proc (Is_Reference);
-
-      --  Start of processing for Referenced
-
-      begin
-         Inspect_Expression (Expr);
-         return Seen;
-      end Referenced;
-
       --  Local variables
 
       Cond    : constant Node_Id := Condition (N);