[Ada] References to task and protected types in aspects/pragmas

This patch implements the following rules from SPARK RM 6.1.4:

   For purposes of the rules concerning the Global, Depends, Refined_Global,
   and Refined_Depends aspects, when any of these aspects are specified for a
   task unit the task unit's body is considered to be the body of a procedure
   and the current instance of the task unit is considered to be a formal
   parameter (of that notional procedure) of mode IN OUT.

   Similarly, for purposes of the rules concerning the Global, Refined_Global,
   Depends, and Refined_Depends aspects as they apply to protected operations,
   the current instance of the enclosing protected unit is considered to be a
   formal parameter (of mode IN for a protected function, of mode IN OUT
   otherwise) and a protected entry is considered to be a protected procedure.

The patch also introduces the concept of a body "freezing" the contract of its
initial declaration.

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

--  synchronized_contracts.ads

package Synchronized_Contracts
  with SPARK_Mode,
       Abstract_State => State
is
   Var : Integer := 1;

   protected type Prot_Typ_1 is
      entry Prot_Ent (Formal : out Integer)
        with Global  => (Input => (State, Var)),
             Depends => ((Prot_Typ_1, Formal) => (State, Var, Prot_Typ_1));
   end Prot_Typ_1;

   protected Prot_Typ_2 is
      entry Prot_Ent (Formal : out Integer);
      pragma Global  ((Input => State));
      pragma Depends ((Formal => State));
   end Prot_Typ_2;

   task type Task_Typ_1
     with Global  => (Input => State, Output => Var),
          Depends => ((Var, Task_Typ_1) => (State, Task_Typ_1));

   task Task_Typ_2;
   pragma Global  ((Output => (State, Var)));
   pragma Depends (((State, Var) => null));
end Synchronized_Contracts;

--  synchronized_contracts.adb

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

   protected body Prot_Typ_1 is
      entry Prot_Ent (Formal : out Integer) when True is
         pragma Refined_Global  ((Input => (Constit, Var)));
         pragma Refined_Depends (((Prot_Typ_1, Formal) =>
                                     (Constit, Var, Prot_Typ_1)));
      begin
         Formal := Constit + Var;
      end Prot_Ent;
   end Prot_Typ_1;

   protected body Prot_Typ_2 is
      entry Prot_Ent (Formal : out Integer)
        with Refined_Global  => (Input => Constit),
             Refined_Depends => (Formal => Constit)
        when True is
      begin
         Formal := Constit + 1;
      end Prot_Ent;
   end Prot_Typ_2;

   task body Task_Typ_1 is
      pragma Refined_Global  ((Input => Constit, Output => Var));
      pragma Refined_Depends (((Var, Task_Typ_1) => (Constit, Task_Typ_1)));
   begin
      null;
   end Task_Typ_1;

   task body Task_Typ_2
     with Refined_Global  => (Output => (Constit, Var)),
          Refined_Depends => ((Constit, Var) => null)
   is
   begin
      null;
   end Task_Typ_2;
end Synchronized_Contracts;

-----------------
-- Compilation --
-----------------

$ gcc -c synchronized_contracts.adb

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

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* atree.ads, atree.adb (Ekind_In): New 10 and 11 parameter versions.
	* contracts.ads, contracts.adb (Analyze_Initial_Declaration_Contract):
	New routine.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
	Analyze the contract of the initial declaration.
	(Analyze_Subprogram_Body_Helper): Analyze the contract of the
	initial declaration.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Analyze the contract
	of the initial declaration.
	* sem_ch9.adb (Analyze_Entry_Body): Analyze the contract of
	the initial declaration.
	(Analyze_Protected_Body): Analyze
	the contract of the initial declaration.
	(Analyze_Task_Body): Analyze the contract of the initial declaration.
	* sem_prag.adb (Add_Entity_To_Name_Buffer): Use "type" rather
	than "unit" as it makes the error messages sound better.
	(Add_Item_To_Name_Buffer): Update comment on usage. The routine
	now supports discriminants and current instances of concurrent
	types.
	(Analyze_Depends_In_Decl_Part): Install the discriminants
	of a task type.
	(Analyze_Global_In_Decl_Part): Install the discriminants of a task type.
	(Analyze_Global_Item): Add processing for current instances of
	concurrent types and include discriminants as valid global items.
	(Analyze_Input_Output): Discriminants and current instances of
	concurrent types are now valid items. Update various error messages.
	(Check_Usage): Current instances of protected and task types behaves
	as formal parameters.
	(Collect_Subprogram_Inputs_Outputs): There is
	no longer need to manually analyze [Refined_]Global thanks to
	freezing of initial declaration contracts.  Add processing for
	the current instance of a concurrent type.
	(Find_Role): Add categorizations for discriminants, protected and task
	types.
	(Is_CCT_Instance): New routine.
	(Match_Items): Update the comment on usage. Update internal comments.
	* sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update the
	comment on usage.
	* sem_util.adb (Entity_Of): Ensure that the entity is an object
	when traversing a potential renaming chain.
	(Fix_Msg): Use "type" rather than "unit" as it makes the error messages
	sound better.
	* sem_util.ads (Fix_Msg): Update the comment on usage.

[Ada] References to task and protected types in aspects/pragmas

Commit Message

Patch