[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

1 files changed, 6 insertions, 6 deletions

diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 538fa9d..c0118b4 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/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 --