[Ada] Verify Part_Of indicator in non-SPARK code

Message ID 20171215113548.GA70062@adacore.com
State New
Headers show
Series
  • [Ada] Verify Part_Of indicator in non-SPARK code
Related show

Commit Message

Pierre-Marie de Rodat Dec. 15, 2017, 11:35 a.m.
This patch modifies the analysis of Part_Of indicators to verify their
associated rules even when the indicator appears in non-SPARK code. This
prevents possible tamperings of Part_Of constituents of single concurrent
types outside of SPARK code.

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

--  pack.ads

pragma Profile (Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

package Pack with SPARK_Mode is
   protected PO is
   end PO;

   X : Boolean := True with Part_Of => PO;
end Pack;

--  pack.adb

package body Pack is
   protected body PO is
   end PO;
begin
   X := not X;                                                       --  OK
end Pack;

--  flip.adb

pragma Profile (Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

with Pack; use Pack;

procedure Flip with SPARK_Mode => Off is
begin
   X := not X;                                                       --  Error
end Flip;

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

$ gcc -c flip.adb
$ gcc -c pack.adb
flip.adb:8:04: reference to variable "X" cannot appear in this context
flip.adb:8:04: "X" is constituent of single protected type "PO"
flip.adb:8:13: reference to variable "X" cannot appear in this context
flip.adb:8:13: "X" is constituent of single protected type "PO"

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

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Part_Of): The context-specific portion of the
	analysis is now directed to several specialized routines.
	(Check_Part_Of_Abstract_State): New routine.
	(Check_Part_Of_Concurrent_Type): New routine. Reimplement the checks
	involving the item, the single concurrent type, and their respective
	contexts.
	* sem_res.adb (Resolve_Entity_Name): Potential constituents of a single
	concurrent type are now recorded regardless of the SPARK mode.
	* sem_util.adb (Check_Part_Of_Reference): Split some of the tests in
	individual predicates.  A Part_Of reference is legal when it appears
	within the statement list of the object's immediately enclosing
	package.
	(Is_Enclosing_Package_Body): New routine.
	(Is_Internal_Declaration_Or_Body): New routine.
	(Is_Single_Declaration_Or_Body): New routine.
	(Is_Single_Task_Pragma): New routine.

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 255685)
+++ sem_prag.adb	(working copy)
@@ -3168,71 +3168,26 @@ 
       Encap_Id : out Entity_Id;
       Legal    : out Boolean)
    is
-      Encap_Typ   : Entity_Id;
-      Item_Decl   : Node_Id;
-      Pack_Id     : Entity_Id;
-      Placement   : State_Space_Kind;
-      Parent_Unit : Entity_Id;
+      procedure Check_Part_Of_Abstract_State;
+      pragma Inline (Check_Part_Of_Abstract_State);
+      --  Verify the legality of indicator Part_Of when the encapsulator is an
+      --  abstract state.
 
-   begin
-      --  Assume that the indicator is illegal
+      procedure Check_Part_Of_Concurrent_Type;
+      pragma Inline (Check_Part_Of_Concurrent_Type);
+      --  Verify the legality of indicator Part_Of when the encapsulator is a
+      --  single concurrent type.
 
-      Encap_Id := Empty;
-      Legal    := False;
+      ----------------------------------
+      -- Check_Part_Of_Abstract_State --
+      ----------------------------------
 
-      if Nkind_In (Encap, N_Expanded_Name,
-                          N_Identifier,
-                          N_Selected_Component)
-      then
-         Analyze       (Encap);
-         Resolve_State (Encap);
+      procedure Check_Part_Of_Abstract_State is
+         Pack_Id     : Entity_Id;
+         Placement   : State_Space_Kind;
+         Parent_Unit : Entity_Id;
 
-         Encap_Id := Entity (Encap);
-
-         --  The encapsulator is an abstract state
-
-         if Ekind (Encap_Id) = E_Abstract_State then
-            null;
-
-         --  The encapsulator is a single concurrent type (SPARK RM 9.3)
-
-         elsif Is_Single_Concurrent_Object (Encap_Id) then
-            null;
-
-         --  Otherwise the encapsulator is not a legal choice
-
-         else
-            SPARK_Msg_N
-              ("indicator Part_Of must denote abstract state, single "
-               & "protected type or single task type", Encap);
-            return;
-         end if;
-
-      --  This is a syntax error, always report
-
-      else
-         Error_Msg_N
-           ("indicator Part_Of must denote abstract state, single protected "
-            & "type or single task type", Encap);
-         return;
-      end if;
-
-      --  Catch a case where indicator Part_Of denotes the abstract view of a
-      --  variable which appears as an abstract state (SPARK RM 10.1.2 2).
-
-      if From_Limited_With (Encap_Id)
-        and then Present (Non_Limited_View (Encap_Id))
-        and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable
-      then
-         SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap);
-         SPARK_Msg_N ("\& denotes abstract view of object", Encap);
-         return;
-      end if;
-
-      --  The encapsulator is an abstract state
-
-      if Ekind (Encap_Id) = E_Abstract_State then
-
+      begin
          --  Determine where the object, package instantiation or state lives
          --  with respect to the enclosing packages or package bodies.
 
@@ -3250,6 +3205,7 @@ 
             SPARK_Msg_N
               ("indicator Part_Of cannot appear in this context "
                & "(SPARK RM 7.2.6(5))", Indic);
+
             Error_Msg_Name_1 := Chars (Scope (Encap_Id));
             SPARK_Msg_NE
               ("\& is not part of the hidden state of package %",
@@ -3267,14 +3223,14 @@ 
               and then Is_Private_Descendant (Pack_Id)
             then
                --  A variable or state abstraction which is part of the visible
-               --  state of a private child unit (or one of its public
-               --  descendants) must have its Part_Of indicator specified. The
-               --  Part_Of indicator must denote a state abstraction declared
-               --  by either the parent unit of the private unit or by a public
-               --  descendant of that parent unit.
+               --  state of a private child unit or its public descendants must
+               --  have its Part_Of indicator specified. The Part_Of indicator
+               --  must denote a state declared by either the parent unit of
+               --  the private unit or by a public descendant of that parent
+               --  unit.
 
-               --  Find nearest private ancestor (which can be the current unit
-               --  itself).
+               --  Find the nearest private ancestor (which can be the current
+               --  unit itself).
 
                Parent_Unit := Pack_Id;
                while Present (Parent_Unit) loop
@@ -3288,8 +3244,8 @@ 
 
                if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then
                   SPARK_Msg_NE
-                    ("indicator Part_Of must denote abstract state of & "
-                     & "or of its public descendant (SPARK RM 7.2.6(3))",
+                    ("indicator Part_Of must denote abstract state of & or of "
+                     & "its public descendant (SPARK RM 7.2.6(3))",
                      Indic, Parent_Unit);
                   return;
 
@@ -3302,8 +3258,8 @@ 
 
                else
                   SPARK_Msg_NE
-                    ("indicator Part_Of must denote abstract state of & "
-                     & "or of its public descendant (SPARK RM 7.2.6(3))",
+                    ("indicator Part_Of must denote abstract state of & or of "
+                     & "its public descendant (SPARK RM 7.2.6(3))",
                      Indic, Parent_Unit);
                   return;
                end if;
@@ -3315,6 +3271,7 @@ 
                SPARK_Msg_N
                  ("indicator Part_Of cannot appear in this context "
                   & "(SPARK RM 7.2.6(5))", Indic);
+
                Error_Msg_Name_1 := Chars (Pack_Id);
                SPARK_Msg_NE
                  ("\& is declared in the visible part of package %",
@@ -3330,6 +3287,7 @@ 
                SPARK_Msg_NE
                  ("indicator Part_Of must denote an abstract state of "
                   & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
+
                Error_Msg_Name_1 := Chars (Pack_Id);
                SPARK_Msg_NE
                  ("\& is declared in the private part of package %",
@@ -3354,11 +3312,77 @@ 
             return;
          end if;
 
-      --  The encapsulator is a single concurrent type
+         --  At this point it is known that the Part_Of indicator is legal
 
-      else
-         Encap_Typ := Etype (Encap_Id);
+         Legal := True;
+      end Check_Part_Of_Abstract_State;
 
+      -----------------------------------
+      -- Check_Part_Of_Concurrent_Type --
+      -----------------------------------
+
+      procedure Check_Part_Of_Concurrent_Type is
+         function In_Proper_Order
+           (First  : Node_Id;
+            Second : Node_Id) return Boolean;
+         pragma Inline (In_Proper_Order);
+         --  Determine whether node First precedes node Second
+
+         procedure Placement_Error;
+         pragma Inline (Placement_Error);
+         --  Emit an error concerning the illegal placement of the item with
+         --  respect to the single concurrent type.
+
+         ---------------------
+         -- In_Proper_Order --
+         ---------------------
+
+         function In_Proper_Order
+           (First  : Node_Id;
+            Second : Node_Id) return Boolean
+         is
+            N : Node_Id;
+
+         begin
+            if List_Containing (First) = List_Containing (Second) then
+               N := First;
+               while Present (N) loop
+                  if N = Second then
+                     return True;
+                  end if;
+
+                  Next (N);
+               end loop;
+            end if;
+
+            return False;
+         end In_Proper_Order;
+
+         ---------------------
+         -- Placement_Error --
+         ---------------------
+
+         procedure Placement_Error is
+         begin
+            SPARK_Msg_N
+              ("indicator Part_Of must denote a previously declared single "
+               & "protected type or single task type", Encap);
+         end Placement_Error;
+
+         --  Local variables
+
+         Conc_Typ      : constant Entity_Id := Etype (Encap_Id);
+         Encap_Decl    : constant Node_Id   := Declaration_Node (Encap_Id);
+         Encap_Context : constant Node_Id   := Parent (Encap_Decl);
+
+         Item_Context : Node_Id;
+         Item_Decl    : Node_Id;
+         Prv_Decls    : List_Id;
+         Vis_Decls    : List_Id;
+
+      --  Start of processing for Check_Part_Of_Concurrent_Type
+
+      begin
          --  Only abstract states and variables can act as constituents of an
          --  encapsulating single concurrent type.
 
@@ -3370,7 +3394,7 @@ 
          elsif Ekind (Item_Id) = E_Constant then
             Error_Msg_Name_1 := Chars (Encap_Id);
             SPARK_Msg_NE
-              (Fix_Msg (Encap_Typ, "constant & cannot act as constituent of "
+              (Fix_Msg (Conc_Typ, "constant & cannot act as constituent of "
                & "single protected type %"), Indic, Item_Id);
             return;
 
@@ -3379,7 +3403,7 @@ 
          else
             Error_Msg_Name_1 := Chars (Encap_Id);
             SPARK_Msg_NE
-              (Fix_Msg (Encap_Typ, "package instantiation & cannot act as "
+              (Fix_Msg (Conc_Typ, "package instantiation & cannot act as "
                & "constituent of single protected type %"), Indic, Item_Id);
             return;
          end if;
@@ -3398,64 +3422,159 @@ 
             Item_Decl := Declaration_Node (Item_Id);
          end if;
 
-         --  Both the item and its encapsulating single concurrent type must
-         --  appear in the same declarative region (SPARK RM 9.3). Note that
-         --  privacy is ignored.
+         Item_Context := Parent (Item_Decl);
 
-         if Parent (Item_Decl) /= Parent (Declaration_Node (Encap_Id)) then
+         --  The item and the single concurrent type must appear in the same
+         --  declarative region, with the item following the declaration of
+         --  the single concurrent type (SPARK RM 9(3)).
+
+         if Item_Context = Encap_Context then
+            if Nkind_In (Item_Context, N_Package_Specification,
+                                       N_Protected_Definition,
+                                       N_Task_Definition)
+            then
+               Prv_Decls := Private_Declarations (Item_Context);
+               Vis_Decls := Visible_Declarations (Item_Context);
+
+               --  The placement is OK when the single concurrent type appears
+               --  within the visible declarations and the item in the private
+               --  declarations.
+               --
+               --    package Pack is
+               --       protected PO ...
+               --    private
+               --       Constit : ... with Part_Of => PO;
+               --    end Pack;
+
+               if List_Containing (Encap_Decl) = Vis_Decls
+                 and then List_Containing (Item_Decl) = Prv_Decls
+               then
+                  null;
+
+               --  The placement is illegal when the item appears within the
+               --  visible declarations and the single concurrent type is in
+               --  the private declarations.
+               --
+               --    package Pack is
+               --       Constit : ... with Part_Of => PO;
+               --    private
+               --       protected PO ...
+               --    end Pack;
+
+               elsif List_Containing (Item_Decl) = Vis_Decls
+                 and then List_Containing (Encap_Decl) = Prv_Decls
+               then
+                  Placement_Error;
+                  return;
+
+               --  Otherwise both the item and the single concurrent type are
+               --  in the same list. Ensure that the declaration of the single
+               --  concurrent type precedes that of the item.
+
+               elsif not In_Proper_Order
+                           (First  => Encap_Decl,
+                            Second => Item_Decl)
+               then
+                  Placement_Error;
+                  return;
+               end if;
+
+            --  Otherwise both the item and the single concurrent type are
+            --  in the same list. Ensure that the declaration of the single
+            --  concurrent type precedes that of the item.
+
+            elsif not In_Proper_Order
+                        (First  => Encap_Decl,
+                         Second => Item_Decl)
+            then
+               Placement_Error;
+               return;
+            end if;
+
+         --  Otherwise the item and the single concurrent type reside within
+         --  unrelated regions.
+
+         else
             Error_Msg_Name_1 := Chars (Encap_Id);
             SPARK_Msg_NE
-              (Fix_Msg (Encap_Typ, "constituent & must be declared "
+              (Fix_Msg (Conc_Typ, "constituent & must be declared "
                & "immediately within the same region as single protected "
                & "type %"), Indic, Item_Id);
             return;
          end if;
 
-         --  The declaration of the item should follow the declaration of its
-         --  encapsulating single concurrent type and must appear in the same
-         --  declarative region (SPARK RM 9.3).
+         --  At this point it is known that the Part_Of indicator is legal
 
-         declare
-            N : Node_Id;
+         Legal := True;
+      end Check_Part_Of_Concurrent_Type;
 
-         begin
-            N := Next (Declaration_Node (Encap_Id));
-            while Present (N) loop
-               exit when N = Item_Decl;
-               Next (N);
-            end loop;
+   --  Start of processing for Analyze_Part_Of
 
-            --  The single concurrent type might be in the visible part of a
-            --  package, and the declaration of the item in the private part
-            --  of the same package.
+   begin
+      --  Assume that the indicator is illegal
 
-            if No (N) then
-               declare
-                  Pack : constant Node_Id :=
-                           Parent (Declaration_Node (Encap_Id));
-               begin
-                  if Nkind (Pack) = N_Package_Specification
-                    and then not In_Private_Part (Encap_Id)
-                  then
-                     N := First (Private_Declarations (Pack));
-                     while Present (N) loop
-                        exit when N = Item_Decl;
-                        Next (N);
-                     end loop;
-                  end if;
-               end;
-            end if;
+      Encap_Id := Empty;
+      Legal    := False;
 
-            if No (N) then
-               SPARK_Msg_N
-                 ("indicator Part_Of must denote a previously declared "
-                  & "single protected type or single task type", Encap);
-               return;
-            end if;
-         end;
+      if Nkind_In (Encap, N_Expanded_Name,
+                          N_Identifier,
+                          N_Selected_Component)
+      then
+         Analyze       (Encap);
+         Resolve_State (Encap);
+
+         Encap_Id := Entity (Encap);
+
+         --  The encapsulator is an abstract state
+
+         if Ekind (Encap_Id) = E_Abstract_State then
+            null;
+
+         --  The encapsulator is a single concurrent type (SPARK RM 9.3)
+
+         elsif Is_Single_Concurrent_Object (Encap_Id) then
+            null;
+
+         --  Otherwise the encapsulator is not a legal choice
+
+         else
+            SPARK_Msg_N
+              ("indicator Part_Of must denote abstract state, single "
+               & "protected type or single task type", Encap);
+            return;
+         end if;
+
+      --  This is a syntax error, always report
+
+      else
+         Error_Msg_N
+           ("indicator Part_Of must denote abstract state, single protected "
+            & "type or single task type", Encap);
+         return;
       end if;
 
-      Legal := True;
+      --  Catch a case where indicator Part_Of denotes the abstract view of a
+      --  variable which appears as an abstract state (SPARK RM 10.1.2 2).
+
+      if From_Limited_With (Encap_Id)
+        and then Present (Non_Limited_View (Encap_Id))
+        and then Ekind (Non_Limited_View (Encap_Id)) = E_Variable
+      then
+         SPARK_Msg_N ("indicator Part_Of must denote abstract state", Encap);
+         SPARK_Msg_N ("\& denotes abstract view of object", Encap);
+         return;
+      end if;
+
+      --  The encapsulator is an abstract state
+
+      if Ekind (Encap_Id) = E_Abstract_State then
+         Check_Part_Of_Abstract_State;
+
+      --  The encapsulator is a single concurrent type
+
+      else
+         Check_Part_Of_Concurrent_Type;
+      end if;
    end Analyze_Part_Of;
 
    ----------------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 255685)
+++ sem_util.adb	(working copy)
@@ -3281,73 +3281,201 @@ 
    -----------------------------
 
    procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id) is
+      function Is_Enclosing_Package_Body
+        (Body_Decl : Node_Id;
+         Obj_Id    : Entity_Id) return Boolean;
+      pragma Inline (Is_Enclosing_Package_Body);
+      --  Determine whether package body Body_Decl or its corresponding spec
+      --  immediately encloses the declaration of object Obj_Id.
+
+      function Is_Internal_Declaration_Or_Body
+        (Decl : Node_Id) return Boolean;
+      pragma Inline (Is_Internal_Declaration_Or_Body);
+      --  Determine whether declaration or body denoted by Decl is internal
+
+      function Is_Single_Declaration_Or_Body
+        (Decl     : Node_Id;
+         Conc_Typ : Entity_Id) return Boolean;
+      pragma Inline (Is_Single_Declaration_Or_Body);
+      --  Determine whether protected/task declaration or body denoted by Decl
+      --  belongs to single concurrent type Conc_Typ.
+
+      function Is_Single_Task_Pragma
+        (Prag     : Node_Id;
+         Task_Typ : Entity_Id) return Boolean;
+      pragma Inline (Is_Single_Task_Pragma);
+      --  Determine whether pragma Prag belongs to single task type Task_Typ
+
+      -------------------------------
+      -- Is_Enclosing_Package_Body --
+      -------------------------------
+
+      function Is_Enclosing_Package_Body
+        (Body_Decl : Node_Id;
+         Obj_Id    : Entity_Id) return Boolean
+      is
+         Obj_Context : Node_Id;
+
+      begin
+         --  Find the context of the object declaration
+
+         Obj_Context := Parent (Declaration_Node (Obj_Id));
+
+         if Nkind (Obj_Context) = N_Package_Specification then
+            Obj_Context := Parent (Obj_Context);
+         end if;
+
+         --  The object appears immediately within the package body
+
+         if Obj_Context = Body_Decl then
+            return True;
+
+         --  The object appears immediately within the corresponding spec
+
+         elsif Nkind (Obj_Context) = N_Package_Declaration
+           and then Unit_Declaration_Node (Corresponding_Spec (Body_Decl)) =
+                      Obj_Context
+         then
+            return True;
+         end if;
+
+         return False;
+      end Is_Enclosing_Package_Body;
+
+      -------------------------------------
+      -- Is_Internal_Declaration_Or_Body --
+      -------------------------------------
+
+      function Is_Internal_Declaration_Or_Body
+        (Decl : Node_Id) return Boolean
+      is
+      begin
+         if Comes_From_Source (Decl) then
+            return False;
+
+         --  A body generated for an expression function which has not been
+         --  inserted into the tree yet (In_Spec_Expression is True) is not
+         --  considered internal.
+
+         elsif Nkind (Decl) = N_Subprogram_Body
+           and then Was_Expression_Function (Decl)
+           and then not In_Spec_Expression
+         then
+            return False;
+         end if;
+
+         return True;
+      end Is_Internal_Declaration_Or_Body;
+
+      -----------------------------------
+      -- Is_Single_Declaration_Or_Body --
+      -----------------------------------
+
+      function Is_Single_Declaration_Or_Body
+        (Decl     : Node_Id;
+         Conc_Typ : Entity_Id) return Boolean
+      is
+         Spec_Id : constant Entity_Id := Unique_Defining_Entity (Decl);
+
+      begin
+         return
+           Present (Anonymous_Object (Spec_Id))
+             and then Anonymous_Object (Spec_Id) = Conc_Typ;
+      end Is_Single_Declaration_Or_Body;
+
+      ---------------------------
+      -- Is_Single_Task_Pragma --
+      ---------------------------
+
+      function Is_Single_Task_Pragma
+        (Prag     : Node_Id;
+         Task_Typ : Entity_Id) return Boolean
+      is
+         Decl : constant Node_Id := Find_Related_Declaration_Or_Body (Prag);
+
+      begin
+         --  To qualify, the pragma must be associated with single task type
+         --  Task_Typ.
+
+         return
+           Is_Single_Task_Object (Task_Typ)
+             and then Nkind (Decl) = N_Object_Declaration
+             and then Defining_Entity (Decl) = Task_Typ;
+      end Is_Single_Task_Pragma;
+
+      --  Local variables
+
       Conc_Obj : constant Entity_Id := Encapsulating_State (Var_Id);
-      Decl     : Node_Id;
-      OK_Use   : Boolean := False;
       Par      : Node_Id;
       Prag_Nam : Name_Id;
-      Spec_Id  : Entity_Id;
+      Prev     : Node_Id;
 
+   --  Start of processing for Check_Part_Of_Reference
+
    begin
+      --  Nothing to do when the variable was recorded, but did not become a
+      --  constituent of a single concurrent type.
+
+      if No (Conc_Obj) then
+         return;
+      end if;
+
       --  Traverse the parent chain looking for a suitable context for the
       --  reference to the concurrent constituent.
 
-      Par := Parent (Ref);
+      Prev := Ref;
+      Par  := Parent (Prev);
       while Present (Par) loop
          if Nkind (Par) = N_Pragma then
             Prag_Nam := Pragma_Name (Par);
 
             --  A concurrent constituent is allowed to appear in pragmas
             --  Initial_Condition and Initializes as this is part of the
-            --  elaboration checks for the constituent (SPARK RM 9.3).
+            --  elaboration checks for the constituent (SPARK RM 9(3)).
 
             if Nam_In (Prag_Nam, Name_Initial_Condition, Name_Initializes) then
-               OK_Use := True;
-               exit;
+               return;
 
             --  When the reference appears within pragma Depends or Global,
             --  check whether the pragma applies to a single task type. Note
-            --  that the pragma is not encapsulated by the type definition,
+            --  that the pragma may not encapsulated by the type definition,
             --  but this is still a valid context.
 
-            elsif Nam_In (Prag_Nam, Name_Depends, Name_Global) then
-               Decl := Find_Related_Declaration_Or_Body (Par);
-
-               if Nkind (Decl) = N_Object_Declaration
-                 and then Defining_Entity (Decl) = Conc_Obj
-               then
-                  OK_Use := True;
-                  exit;
-               end if;
+            elsif Nam_In (Prag_Nam, Name_Depends, Name_Global)
+              and then Is_Single_Task_Pragma (Par, Conc_Obj)
+            then
+               return;
             end if;
 
-         --  The reference appears somewhere in the definition of the single
-         --  protected/task type (SPARK RM 9.3).
+         --  The reference appears somewhere in the definition of a single
+         --  concurrent type (SPARK RM 9(3)).
 
          elsif Nkind_In (Par, N_Single_Protected_Declaration,
                               N_Single_Task_Declaration)
            and then Defining_Entity (Par) = Conc_Obj
          then
-            OK_Use := True;
-            exit;
+            return;
 
-         --  The reference appears within the expanded declaration or the body
-         --  of the single protected/task type (SPARK RM 9.3).
+         --  The reference appears within the declaration or body of a single
+         --  concurrent type (SPARK RM 9(3)).
 
          elsif Nkind_In (Par, N_Protected_Body,
                               N_Protected_Type_Declaration,
                               N_Task_Body,
                               N_Task_Type_Declaration)
+           and then Is_Single_Declaration_Or_Body (Par, Conc_Obj)
          then
-            Spec_Id := Unique_Defining_Entity (Par);
+            return;
 
-            if Present (Anonymous_Object (Spec_Id))
-              and then Anonymous_Object (Spec_Id) = Conc_Obj
-            then
-               OK_Use := True;
-               exit;
-            end if;
+         --  The reference appears within the statement list of the object's
+         --  immediately enclosing package (SPARK RM 9(3)).
 
+         elsif Nkind (Par) = N_Package_Body
+           and then Nkind (Prev) = N_Handled_Sequence_Of_Statements
+           and then Is_Enclosing_Package_Body (Par, Var_Id)
+         then
+            return;
+
          --  The reference has been relocated within an internally generated
          --  package or subprogram. Assume that the reference is legal as the
          --  real check was already performed in the original context of the
@@ -3357,26 +3485,10 @@ 
                               N_Package_Declaration,
                               N_Subprogram_Body,
                               N_Subprogram_Declaration)
-           and then not Comes_From_Source (Par)
+           and then Is_Internal_Declaration_Or_Body (Par)
          then
-            --  Continue to examine the context if the reference appears in a
-            --  subprogram body which was previously an expression function,
-            --  unless this is during preanalysis (when In_Spec_Expression is
-            --  True), as the body may not yet be inserted in the tree.
+            return;
 
-            if Nkind (Par) = N_Subprogram_Body
-              and then Was_Expression_Function (Par)
-              and then not In_Spec_Expression
-            then
-               null;
-
-            --  Otherwise the reference is legal
-
-            else
-               OK_Use := True;
-               exit;
-            end if;
-
          --  The reference has been relocated to an inlined body for GNATprove.
          --  Assume that the reference is legal as the real check was already
          --  performed in the original context of the reference.
@@ -3385,30 +3497,27 @@ 
            and then Nkind (Par) = N_Subprogram_Body
            and then Chars (Defining_Entity (Par)) = Name_uParent
          then
-            OK_Use := True;
-            exit;
+            return;
          end if;
 
-         Par := Parent (Par);
+         Prev := Par;
+         Par  := Parent (Prev);
       end loop;
 
-      --  The reference is illegal as it appears outside the definition or
-      --  body of the single protected/task type.
+      --  At this point it is known that the reference does not appear within a
+      --  legal context.
 
-      if not OK_Use then
+      Error_Msg_NE
+        ("reference to variable & cannot appear in this context", Ref, Var_Id);
+      Error_Msg_Name_1 := Chars (Var_Id);
+
+      if Is_Single_Protected_Object (Conc_Obj) then
          Error_Msg_NE
-           ("reference to variable & cannot appear in this context",
-            Ref, Var_Id);
-         Error_Msg_Name_1 := Chars (Var_Id);
+           ("\% is constituent of single protected type &", Ref, Conc_Obj);
 
-         if Is_Single_Protected_Object (Conc_Obj) then
-            Error_Msg_NE
-              ("\% is constituent of single protected type &", Ref, Conc_Obj);
-
-         else
-            Error_Msg_NE
-              ("\% is constituent of single task type &", Ref, Conc_Obj);
-         end if;
+      else
+         Error_Msg_NE
+           ("\% is constituent of single task type &", Ref, Conc_Obj);
       end if;
    end Check_Part_Of_Reference;
 
@@ -22127,7 +22236,7 @@ 
    begin
       --  The variable is a constituent of a single protected/task type. Such
       --  a variable acts as a component of the type and must appear within a
-      --  specific region (SPARK RM 9.3). Instead of recording the reference,
+      --  specific region (SPARK RM 9(3)). Instead of recording the reference,
       --  verify its legality now.
 
       if Present (Encap) and then Is_Single_Concurrent_Object (Encap) then
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 255678)
+++ sem_res.adb	(working copy)
@@ -7380,15 +7380,15 @@ 
             then
                Check_Elab_Call (N);
             end if;
+         end if;
 
-            --  The variable may eventually become a constituent of a single
-            --  protected/task type. Record the reference now and verify its
-            --  legality when analyzing the contract of the variable
-            --  (SPARK RM 9.3).
+         --  The variable may eventually become a constituent of a single
+         --  protected/task type. Record the reference now and verify its
+         --  legality when analyzing the contract of the variable
+         --  (SPARK RM 9.3).
 
-            if Ekind (E) = E_Variable then
-               Record_Possible_Part_Of_Reference (E, N);
-            end if;
+         if Ekind (E) = E_Variable then
+            Record_Possible_Part_Of_Reference (E, N);
          end if;
 
          --  A Ghost entity must appear in a specific context