[Ada] Aspects on stubs

This patch ensures that aspect specifications which appear on package,
protected, and task body stubs are properly analyzed.

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

--  pack.ads

package Pack
  with SPARK_Mode,
       Abstract_State => State
is
   -------------------------------------
   -- Refined_Depends, Refined_Global --
   -------------------------------------

   procedure Proc_1;
   procedure Proc_2
     with Global  => (In_Out => State),
          Depends => (State  => State);

   task Task_Obj_1;
   task Task_Obj_2
     with Global  => (In_Out => State),
          Depends => (State  => State);

   ------------------
   -- Refined_Post --
   ------------------

   function Func_1 (Formal : Integer) return Integer;
   function Func_2 (Formal : Integer) return Integer
     with Post => Func_2'Result > Formal;

   -------------------
   -- Refined_State --
   -------------------

   package Pack_1 is end Pack_1;
   package Pack_2 with Abstract_State => State_2 is end Pack_2;

   ----------------
   -- SPARK_Mode --
   ----------------

   package Pack_3 with SPARK_Mode => Off is end Pack_3;
   package Pack_4 with SPARK_Mode => Off is end Pack_4;
   package Pack_5 is end Pack_5;

   protected type Prot_Typ_1 with SPARK_Mode => Off is end Prot_Typ_1;
   protected type Prot_Typ_2 with SPARK_Mode => Off is end Prot_Typ_2;
   protected type Prot_Typ_3 is end Prot_Typ_3;

   procedure Proc_3 with SPARK_Mode => Off;
   procedure Proc_4 with SPARK_Mode => Off;
   procedure Proc_5;

   task type Task_Typ_1 with SPARK_Mode => Off;
   task type Task_Typ_2 with SPARK_Mode => Off;
   task type Task_Typ_3;
end Pack;

--  pack.adb

package body Pack
  with SPARK_Mode,
       Refined_State => (State => Constit)
is
   Constit : Integer := 0;

   -------------------------------------
   -- Refined_Depends, Refined_Global --
   -------------------------------------

   procedure Proc_1 is separate
     with Refined_Global  => (In_Out  => Constit),                   --  Error
          Refined_Depends => (Constit => Constit);                   --  Error

   procedure Proc_2 is separate
     with Refined_Global  => (In_Out  => Constit),                   --  OK
          Refined_Depends => (Constit => Constit);                   --  OK

   task body Task_Obj_1 is separate
     with Refined_Global  => (In_Out  => Constit),                   --  Error
          Refined_Depends => (Constit => Constit);                   --  Error

   task body Task_Obj_2 is separate
     with Refined_Global  => (In_Out  => Constit),                   --  OK
          Refined_Depends => (Constit => Constit);                   --  OK

   ------------------
   -- Refined_Post --
   ------------------

   function Func_1 (Formal : Integer) return Integer is separate
     with Refined_Post => Func_1'Result > Formal;                    --  OK

   function Func_2 (Formal : Integer) return Integer is separate
     with Refined_Post => Func_2'Result > Formal;                    --  OK

   -------------------
   -- Refined_State --
   -------------------

   package body Pack_1 is separate
     with Refined_State => (State_1 => Constit_1);                   --  Error

   package body Pack_2 is separate
     with Refined_State => (State_2 => Constit_2);                   --  Error

   ----------------
   -- SPARK_Mode --
   ----------------

   package body Pack_3 is separate with SPARK_Mode => On;            --  Error
   package body Pack_4 is separate;
   package body Pack_5 is separate with SPARK_Mode => Off;           --  Error

   protected body Prot_Typ_1 is separate with SPARK_Mode => On;      --  Error
   protected body Prot_Typ_2 is separate;
   protected body Prot_Typ_3 is separate with SPARK_Mode => Off;     --  Error

   procedure Proc_3 is separate with SPARK_Mode => On;               --  Error
   procedure Proc_4 is separate;
   procedure Proc_5 is separate with SPARK_Mode => Off;              --  Error

   task body Task_Typ_1 is separate with SPARK_Mode => On;           --  Error
   task body Task_Typ_2 is separate;
   task body Task_Typ_3 is separate with SPARK_Mode => Off;          --  Error
end Pack;

--  pack-func_1.adb

separate (Pack)

function Func_1 (Formal : Integer) return Integer
  with Refined_Post => Func_1'Result > Formal                        --  Error
is
begin
   return Formal * 10;
end Func_1;

--  pack-func_2.adb

separate (Pack)

function Func_2 (Formal : Integer) return Integer
  with Refined_Post => Func_2'Result > Formal                        --  Error
is
begin
   return Formal * 10;
end Func_2;

--  pack-pack_1.adb

separate (Pack)

package body Pack_1
  with SPARK_Mode,
       Refined_State => (State_1 => Constit_1)                       --  Error
is
   Constit_1 : Integer := 1;
end Pack_1;

--  pack-pack_2.adb

separate (Pack)

package body Pack_2
  with SPARK_Mode,
       Refined_State => (State_2 => Constit_2)                       --  OK
is
   Constit_2 : Integer := 2;
end Pack_2;

--  pack-pack_3.adb

separate (Pack)

package body Pack_3 is end Pack_3;

--  pack-pack_4.adb

separate (Pack)

package body Pack_4 with SPARK_Mode => On is end Pack_4;             --  OK

--  pack-pack_5.adb

separate (Pack)

package body Pack_5 with SPARK_Mode => On is end Pack_5;             --  OK

--  pack-proc_1.adb

separate (Pack)

procedure Proc_1
  with Refined_Global  => (In_Out  => Constit),                      --  Error
       Refined_Depends => (Constit => Constit)                       --  Error
is begin null; end Proc_1;

--  pack-proc_2.adb

separate (Pack)

procedure Proc_2
  with Refined_Global  => (In_Out  => Constit),                      --  Error
       Refined_Depends => (Constit => Constit)                       --  Error
is begin null; end Proc_2;

--  pack-proc_3.adb

separate (Pack)

procedure Proc_3 is begin null; end Proc_3;

--  pack-proc_4.adb

separate (Pack)

procedure Proc_4 with SPARK_Mode => On is begin null; end Proc_4;    --  OK

--  pack-proc_5.adb

separate (Pack)

procedure Proc_5 with SPARK_Mode => On is begin null; end Proc_5;    --  OK

--  pack-prot_typ_1.adb

separate (Pack)

protected body Prot_Typ_1 is end Prot_Typ_1;

--  pack-prot_typ_2.adb

separate (Pack)

protected body Prot_Typ_2 with SPARK_Mode => On is end Prot_Typ_2;   --  OK

--  pack-prot_typ_3.adb

separate (Pack)

protected body Prot_Typ_3 with SPARK_Mode => On is end Prot_Typ_3;   --  OK

--  pack-task_obj_1.adb

separate (Pack)

task body Task_Obj_1
  with Refined_Global  => (In_Out  => Constit),                      --  Error
       Refined_Depends => (Constit => Constit)                       --  Error
is begin null; end Task_Obj_1;

--  pack-task_obj_2.adb

separate (Pack)

task body Task_Obj_2
  with Refined_Global  => (In_Out  => Constit),                      --  Error
       Refined_Depends => (Constit => Constit)                       --  Error
is begin null; end Task_Obj_2;

--  pack-task_typ_1.adb

separate (Pack)

task body Task_Typ_1 is begin null; end Task_Typ_1;

--  pack-task_typ_2.adb

separate (Pack)

task body Task_Typ_2 with SPARK_Mode => On is                        --  OK
begin null; end Task_Typ_2;

--  pack-task_typ_3.adb

separate (Pack)

task body Task_Typ_3 with SPARK_Mode => On is                        --  OK
begin null; end Task_Typ_3;

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

$ gcc -c pack.adb
pack.adb:12:11: useless refinement, declaration of subprogram "Proc_1" lacks
  aspect or pragma Global
pack.adb:13:11: useless refinement, declaration of subprogram "Proc_1" lacks
  aspect or pragma Depends
pack.adb:20:11: useless refinement, declaration of task type "Task_Obj_1" lacks
  aspect or pragma Global
pack.adb:21:11: useless refinement, declaration of task type "Task_Obj_1" lacks
  aspect or pragma Depends
pack.adb:42:11: aspect "Refined_State" must apply to a package body
pack.adb:45:11: aspect "Refined_State" must apply to a package body
pack.adb:51:41: incorrect placement of aspect "Spark_Mode"
pack.adb:53:41: incorrect placement of aspect "Spark_Mode"
pack.adb:55:47: incorrect placement of aspect "Spark_Mode"
pack.adb:57:47: incorrect placement of aspect "Spark_Mode"
pack.adb:59:38: incorrect placement of aspect "Spark_Mode"
pack.adb:61:38: incorrect placement of aspect "Spark_Mode"
pack.adb:63:42: incorrect placement of aspect "Spark_Mode"
pack.adb:65:42: incorrect placement of aspect "Spark_Mode"
pack-proc_1.adb:4:08: aspect "Refined_Global" cannot apply to a subunit
pack-proc_1.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit
pack-proc_2.adb:4:08: aspect "Refined_Global" cannot apply to a subunit
pack-proc_2.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit
pack-task_obj_1.adb:4:08: aspect "Refined_Global" cannot apply to a subunit
pack-task_obj_1.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit
pack-task_obj_2.adb:4:08: aspect "Refined_Global" cannot apply to a subunit
pack-task_obj_2.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit
pack-func_1.adb:4:08: aspect "Refined_Post" cannot apply to a subunit
pack-func_2.adb:4:08: aspect "Refined_Post" cannot apply to a subunit
pack-pack_1.adb:3:14: body of package "Pack_1" has unused hidden states
pack-pack_1.adb:3:14: variable "Constit_1" defined at line 7
pack-pack_1.adb:5:08: useless refinement, package "Pack_1" does not define
  abstract states
pack-pack_1.adb:5:26: "State_1" is undefined
pack-pack_3.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2
pack-pack_3.adb:3:01: value Off was set for SPARK_Mode on "Pack_3" at
  pack.ads:38
pack-pack_4.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2
pack-pack_4.adb:3:01: value Off was set for SPARK_Mode on "Pack_4" at
  pack.ads:39
pack-pack_4.adb:3:26: incorrect use of SPARK_Mode
pack-pack_4.adb:3:26: value Off was set for SPARK_Mode on "Pack_4" at
  pack.ads:39
pack-prot_typ_2.adb:3:32: incorrect use of SPARK_Mode
pack-prot_typ_2.adb:3:32: value Off was set for SPARK_Mode on "Prot_Typ_2" at
  pack.ads:43
pack-proc_3.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2
pack-proc_3.adb:3:01: value Off was set for SPARK_Mode on "Proc_3" at
  pack.ads:46
pack-proc_4.adb:3:01: incorrect use of SPARK_Mode at pack.adb:2
pack-proc_4.adb:3:01: value Off was set for SPARK_Mode on "Proc_4" at
  pack.ads:47
pack-proc_4.adb:3:23: incorrect use of SPARK_Mode
pack-proc_4.adb:3:23: value Off was set for SPARK_Mode on "Proc_4" at
  pack.ads:47
pack-task_typ_2.adb:3:27: incorrect use of SPARK_Mode
pack-task_typ_2.adb:3:27: value Off was set for SPARK_Mode on "Task_Typ_2" at
  pack.ads:51

2018-05-21  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* sem_ch6.adb (Analyze_Generic_Subprogram_Body): Rename the call to
	Analyze_Aspect_Specifications_On_Body_Or_Stub.
	(Analyze_Subprogram_Body_Helper): Rename the calls to
	Analyze_Aspect_Specifications_On_Body_Or_Stub.
	* sem_ch9.adb (Analyze_Entry_Body): Rename the call to
	Analyze_Aspect_Specifications_On_Body_Or_Stub.
	* sem_ch10.adb: Add with and use clause for Sem_Ch13.
	(Analyze_Package_Body_Stub): Add constant Id. Decorate the package stub
	prior to analyzing its aspects.
	(Analyze_Protected_Body_Stub): Add constant Id. Decorate the package
	stub prior to analyzing its aspects. Save and restore the configuration
	switches.
	(Analyze_Task_Body_Stub): Add constant Id. Decorate the package stub
	prior to analyzing its aspects.
	* sem_ch13.adb (Analyze_Aspect_Specifications_On_Body_Or_Stub): Renamed
	to Analyze_Aspects_On_Subprogram_Body_Or_Stub.
	* sem_ch13.ads (Analyze_Aspect_Specifications_On_Body_Or_Stub): Renamed
	to Analyze_Aspects_On_Subprogram_Body_Or_Stub.
	* sem_prag.adb: Code reformatting.
	(Analyze_Refined_Depends_Global_Post): Consider task body stubs.

From-SVN: r260469

gcc/ada/ChangeLog

+2018-04-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_ch6.adb (Analyze_Generic_Subprogram_Body): Rename the call to
+	Analyze_Aspect_Specifications_On_Body_Or_Stub.
+	(Analyze_Subprogram_Body_Helper): Rename the calls to
+	Analyze_Aspect_Specifications_On_Body_Or_Stub.
+	* sem_ch9.adb (Analyze_Entry_Body): Rename the call to
+	Analyze_Aspect_Specifications_On_Body_Or_Stub.
+	* sem_ch10.adb: Add with and use clause for Sem_Ch13.
+	(Analyze_Package_Body_Stub): Add constant Id. Decorate the package stub
+	prior to analyzing its aspects.
+	(Analyze_Protected_Body_Stub): Add constant Id. Decorate the package
+	stub prior to analyzing its aspects. Save and restore the configuration
+	switches.
+	(Analyze_Task_Body_Stub): Add constant Id. Decorate the package stub
+	prior to analyzing its aspects.
+	* sem_ch13.adb (Analyze_Aspect_Specifications_On_Body_Or_Stub): Renamed
+	to Analyze_Aspects_On_Subprogram_Body_Or_Stub.
+	* sem_ch13.ads (Analyze_Aspect_Specifications_On_Body_Or_Stub): Renamed
+	to Analyze_Aspects_On_Subprogram_Body_Or_Stub.
+	* sem_prag.adb: Code reformatting.
+	(Analyze_Refined_Depends_Global_Post): Consider task body stubs.
+
 2018-04-04  Jerome Lambourg  <lambourg@adacore.com>
 
 	* gcc-interface/Makefile.in: Add g-soliop__qnx.ads to the runtime build

gcc/ada/sem_ch10.adb

@@ -55,6 +55,7 @@ with Sem_Ch3;   use Sem_Ch3;
 with Sem_Ch6;   use Sem_Ch6;
 with Sem_Ch7;   use Sem_Ch7;
 with Sem_Ch8;   use Sem_Ch8;
+with Sem_Ch13;  use Sem_Ch13;
 with Sem_Dist;  use Sem_Dist;
 with Sem_Prag;  use Sem_Prag;
 with Sem_Util;  use Sem_Util;
@@ -1594,7 +1595,7 @@ package body Sem_Ch10 is
    -------------------------------
 
    procedure Analyze_Package_Body_Stub (N : Node_Id) is
-      Id   : constant Entity_Id := Defining_Identifier (N);
+      Id   : constant Entity_Id := Defining_Entity (N);
       Nam  : Entity_Id;
       Opts : Config_Switches_Type;
 
@@ -1623,9 +1624,15 @@ package body Sem_Ch10 is
          --  generating code, the existence of the body will be confirmed
          --  when we load the proper body.
 
+         Set_Scope (Id, Current_Scope);
+         Set_Ekind (Id, E_Package_Body);
+         Set_Etype (Id, Standard_Void_Type);
+
+         if Has_Aspects (N) then
+            Analyze_Aspect_Specifications (N, Id);
+         end if;
+
          Set_Has_Completion (Nam);
-         Set_Scope (Defining_Entity (N), Current_Scope);
-         Set_Ekind (Defining_Entity (N), E_Package_Body);
          Set_Corresponding_Spec_Of_Stub (N, Nam);
          Generate_Reference (Nam, Id, 'b');
          Analyze_Proper_Body (N, Nam);
@@ -1951,7 +1958,9 @@ package body Sem_Ch10 is
    ----------------------------------
 
    procedure Analyze_Protected_Body_Stub (N : Node_Id) is
-      Nam : Entity_Id := Current_Entity_In_Scope (Defining_Identifier (N));
+      Id   : constant Entity_Id := Defining_Entity (N);
+      Nam  : Entity_Id          := Current_Entity_In_Scope (Id);
+      Opts : Config_Switches_Type;
 
    begin
       Check_Stub_Level (N);
@@ -1966,12 +1975,25 @@ package body Sem_Ch10 is
          Error_Msg_N ("missing specification for Protected body", N);
 
       else
-         Set_Scope (Defining_Entity (N), Current_Scope);
-         Set_Ekind (Defining_Entity (N), E_Protected_Body);
+         --  Retain and restore the configuration options of the enclosing
+         --  context as the proper body may introduce a set of its own.
+
+         Save_Opt_Config_Switches (Opts);
+
+         Set_Scope (Id, Current_Scope);
+         Set_Ekind (Id, E_Protected_Body);
+         Set_Etype (Id, Standard_Void_Type);
+
+         if Has_Aspects (N) then
+            Analyze_Aspect_Specifications (N, Id);
+         end if;
+
          Set_Has_Completion (Etype (Nam));
          Set_Corresponding_Spec_Of_Stub (N, Nam);
-         Generate_Reference (Nam, Defining_Identifier (N), 'b');
+         Generate_Reference (Nam, Id, 'b');
          Analyze_Proper_Body (N, Etype (Nam));
+
+         Restore_Opt_Config_Switches (Opts);
       end if;
    end Analyze_Protected_Body_Stub;
 
@@ -2427,8 +2449,9 @@ package body Sem_Ch10 is
    ----------------------------
 
    procedure Analyze_Task_Body_Stub (N : Node_Id) is
+      Id  : constant Entity_Id  := Defining_Entity (N);
       Loc : constant Source_Ptr := Sloc (N);
-      Nam : Entity_Id := Current_Entity_In_Scope (Defining_Identifier (N));
+      Nam : Entity_Id           := Current_Entity_In_Scope (Id);
 
    begin
       Check_Stub_Level (N);
@@ -2443,9 +2466,15 @@ package body Sem_Ch10 is
          Error_Msg_N ("missing specification for task body", N);
 
       else
-         Set_Scope (Defining_Entity (N), Current_Scope);
-         Set_Ekind (Defining_Entity (N), E_Task_Body);
-         Generate_Reference (Nam, Defining_Identifier (N), 'b');
+         Set_Scope (Id, Current_Scope);
+         Set_Ekind (Id, E_Task_Body);
+         Set_Etype (Id, Standard_Void_Type);
+
+         if Has_Aspects (N) then
+            Analyze_Aspect_Specifications (N, Id);
+         end if;
+
+         Generate_Reference (Nam, Id, 'b');
          Set_Corresponding_Spec_Of_Stub (N, Nam);
 
          --  Check for duplicate stub, if so give message and terminate

gcc/ada/sem_ch13.adb

@@ -3865,11 +3865,11 @@ package body Sem_Ch13 is
       end if;
    end Analyze_Aspect_Specifications;
 
-   ---------------------------------------------------
-   -- Analyze_Aspect_Specifications_On_Body_Or_Stub --
-   ---------------------------------------------------
+   ------------------------------------------------
+   -- Analyze_Aspects_On_Subprogram_Body_Or_Stub --
+   ------------------------------------------------
 
-   procedure Analyze_Aspect_Specifications_On_Body_Or_Stub (N : Node_Id) is
+   procedure Analyze_Aspects_On_Subprogram_Body_Or_Stub (N : Node_Id) is
       Body_Id : constant Entity_Id := Defining_Entity (N);
 
       procedure Diagnose_Misplaced_Aspects (Spec_Id : Entity_Id);
@@ -3985,7 +3985,7 @@ package body Sem_Ch13 is
 
       Spec_Id : constant Entity_Id := Unique_Defining_Entity (N);
 
-   --  Start of processing for Analyze_Aspects_On_Body_Or_Stub
+   --  Start of processing for Analyze_Aspects_On_Subprogram_Body_Or_Stub
 
    begin
       --  Language-defined aspects cannot be associated with a subprogram body
@@ -3998,7 +3998,7 @@ package body Sem_Ch13 is
       else
          Analyze_Aspect_Specifications (N, Body_Id);
       end if;
-   end Analyze_Aspect_Specifications_On_Body_Or_Stub;
+   end Analyze_Aspects_On_Subprogram_Body_Or_Stub;
 
    -----------------------
    -- Analyze_At_Clause --

gcc/ada/sem_ch13.ads

@@ -42,7 +42,7 @@ package Sem_Ch13 is
    --  is the corresponding entity declared by the declaration node N. Callers
    --  should check that Has_Aspects (N) is True before calling this routine.
 
-   procedure Analyze_Aspect_Specifications_On_Body_Or_Stub (N : Node_Id);
+   procedure Analyze_Aspects_On_Subprogram_Body_Or_Stub (N : Node_Id);
    --  Analyze the aspect specifications of [generic] subprogram body or stub
    --  N. Callers should check that Has_Aspects (N) is True before calling the
    --  routine. This routine diagnoses misplaced aspects that should appear on

gcc/ada/sem_ch6.adb

@@ -1502,7 +1502,7 @@ package body Sem_Ch6 is
          --  subprogram body.
 
          if Has_Aspects (N) then
-            Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
+            Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
          end if;
 
          Analyze_Declarations (Declarations (N));
@@ -4155,7 +4155,7 @@ package body Sem_Ch6 is
 
       if Nkind (N) = N_Subprogram_Body_Stub then
          if Has_Aspects (N) then
-            Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
+            Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
          end if;
 
          goto Leave;
@@ -4370,7 +4370,7 @@ package body Sem_Ch6 is
       --  Analyze any aspect specifications that appear on the subprogram body
 
       if Has_Aspects (N) then
-         Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
+         Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
       end if;
 
       Analyze_Declarations (Declarations (N));

gcc/ada/sem_ch9.adb

@@ -1246,7 +1246,7 @@ package body Sem_Ch9 is
       --  Analyze any aspect specifications that appear on the entry body
 
       if Has_Aspects (N) then
-         Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
+         Analyze_Aspects_On_Subprogram_Body_Or_Stub (N);
       end if;
 
       E := First_Entity (P_Type);

gcc/ada/sem_prag.adb

@@ -2010,8 +2010,9 @@ package body Sem_Prag is
      (N        : Node_Id;
       Expr_Val : out Boolean)
    is
-      Arg1     : constant Node_Id := First (Pragma_Argument_Associations (N));
-      Obj_Decl : constant Node_Id := Find_Related_Context (N);
+      Arg1     : constant Node_Id   :=
+                   First (Pragma_Argument_Associations (N));
+      Obj_Decl : constant Node_Id   := Find_Related_Context (N);
       Obj_Id   : constant Entity_Id := Defining_Entity (Obj_Decl);
       Expr     : Node_Id;
 
@@ -4709,27 +4710,12 @@ package body Sem_Prag is
 
          Body_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True);
 
-         --  Entry body
-
-         if Nkind (Body_Decl) = N_Entry_Body then
-            null;
-
-         --  Subprogram body
-
-         elsif Nkind (Body_Decl) = N_Subprogram_Body then
-            null;
-
-         --  Subprogram body stub
-
-         elsif Nkind (Body_Decl) = N_Subprogram_Body_Stub then
-            null;
-
-         --  Task body
-
-         elsif Nkind (Body_Decl) = N_Task_Body then
-            null;
-
-         else
+         if not Nkind_In (Body_Decl, N_Entry_Body,
+                                     N_Subprogram_Body,
+                                     N_Subprogram_Body_Stub,
+                                     N_Task_Body,
+                                     N_Task_Body_Stub)
+         then
             Pragma_Misplaced;
             return;
          end if;
@@ -11929,17 +11915,9 @@ package body Sem_Prag is
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Abstract states must
-            --  be associated with a package declaration.
-
-            if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                    N_Package_Declaration)
+            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
             then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construct
-
-            else
                Pragma_Misplaced;
                return;
             end if;
@@ -12858,12 +12836,7 @@ package body Sem_Prag is
 
             --  Object declaration
 
-            if Nkind (Obj_Decl) = N_Object_Declaration then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construact
-
-            else
+            if Nkind (Obj_Decl) /= N_Object_Declaration then
                Pragma_Misplaced;
                return;
             end if;
@@ -13903,14 +13876,7 @@ package body Sem_Prag is
 
             Obj_Decl := Find_Related_Context (N, Do_Checks => True);
 
-            --  Object declaration
-
-            if Nkind (Obj_Decl) = N_Object_Declaration then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construct
-
-            else
+            if Nkind (Obj_Decl) /= N_Object_Declaration then
                Pragma_Misplaced;
                return;
             end if;
@@ -17109,17 +17075,9 @@ package body Sem_Prag is
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Initial_Condition
-            --  must be associated with a package declaration.
-
-            if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                    N_Package_Declaration)
+            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
             then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal context
-
-            else
                Pragma_Misplaced;
                return;
             end if;
@@ -17223,17 +17181,9 @@ package body Sem_Prag is
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Initializes must be
-            --  associated with a package declaration.
-
-            if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                    N_Package_Declaration)
+            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
             then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construc
-
-            else
                Pragma_Misplaced;
                return;
             end if;
@@ -21442,15 +21392,7 @@ package body Sem_Prag is
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Refined states must
-            --  be associated with a package body.
-
-            if Nkind (Pack_Decl) = N_Package_Body then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construct
-
-            else
+            if Nkind (Pack_Decl) /= N_Package_Body then
                Pragma_Misplaced;
                return;
             end if;