[Ada] Protected and task units in SPARK

This patch implements the following rules defined in chapter 9 of the SPARK
Reference Manual.

   1. A type is said to yield synchronized objects if it is
      * a task type; or
      * a protected type; or
      * a synchronized interface type; or
      * an array type whose element type yields synchronized objects; or
      * a record type or type extension whose discriminants, if any, lack
        default values, which has at least one nondiscriminant component
        (possibly inherited), and all of whose nondiscriminant component
        types yield synchronized objects; or
      * a descendant of the type Ada.Synchronous_Task_Control.Suspension_Object

      An object is said to be synchronized if it is
      * of a type which yields synchronized objects; or
      * an atomic object whose Async_Writers aspect is True; or
      * a variable which is "constant after elaboration"; or
      * a constant

   3. If a variable or a package which declares a state abstraction is
      declared immediately within the same declarative region as a
      single_task_declaration or a single_protected_declaration, then the
      Part_Of aspect of the variable or state abstraction may denote the task
      or protected object. This indicates that the object or state abstraction
      is not part of the visible state or private state of its enclosing
      package.

   4. A protected type shall define full default initialization. A variable
      whose Part_Of aspect specifies a task unit or protected unit shall be of
      a type which defines full default initialization, or shall be declared
      with an initial value expression, or shall be imported.

   5. A type which does not yield synchronized objects shall not have a
      component type which yields synchronized objects.

   6. A constituent of a synchronized state abstraction shall be a synchronized
      object or a synchronized state abstraction.

The patch also offers support for the following rule which is checked by the
flow analyzed.

   7. A global_item occurring in a Global aspect specification of a task
      unit or of a protected operation shall not denote an object or state
      abstraction which is not synchronized unless the Part_Of aspect of the
      object or state abstraction denotes the task or protected unit.

The patch also changes the implementation of pragmas Depend and Global when
they apply to a single protected or task type. The pragmas are now stored in
the contract of the anonymous object created for the single concurrent type.

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

--  lr3.ads

package LR3 with SPARK_Mode is
   protected Prot_Typ is
      entry Ent;
   end Prot_Typ;

   task Task_Typ;

   Var_1 : Integer := 1 with Part_Of => Prot_Typ;                    --  OK
   Var_2 : Integer := 2 with Part_Of => Task_Typ;                    --  OK
   Var_3 : Integer := 3;
   pragma Part_Of (Prot_Typ);                                        --  OK
   Var_4 : Integer := 4;
   pragma Part_Of (Task_Typ);                                        --  OK

   package Nested_1
     with Abstract_State => ((State_1 with Part_Of => Prot_Typ),     --  OK
                             (State_2 with Part_Of => Task_Typ))     --  OK
   is end Nested_1;

   package Nested_2 is
      pragma Abstract_State (((State_1 with Part_Of => Prot_Typ),    --  OK
                              (State_2 with Part_Of => Task_Typ)));  --  OK
   end Nested_2;

private
   Var_5 : Integer := 5 with Part_Of => Prot_Typ;                    --  OK
   Var_6 : Integer := 6 with Part_Of => Task_Typ;                    --  OK
   Var_7 : Integer := 7;
   pragma Part_Of (Prot_Typ);                                        --  OK
   Var_8 : Integer := 8;
   pragma Part_Of (Task_Typ);                                        --  OK

   package Nested_3
     with Abstract_State => ((State_1 with Part_Of => Prot_Typ),     --  OK
                             (State_2 with Part_Of => Task_Typ))     --  OK
   is end Nested_3;

   package Nested_4 is
      pragma Abstract_State (((State_1 with Part_Of => Prot_Typ),    --  OK
                              (State_2 with Part_Of => Task_Typ)));  --  OK
   end Nested_4;
end LR3;

--  lr3a.ads

package LR3a with SPARK_Mode is
   Str : constant String := "Error";

   protected type Prot_Typ_1 is
      entry Ent;
   end Prot_Typ_1;

   protected Prot_Typ_2 is
      entry Ent;
   end Prot_Typ_2;

   task type Task_Typ_1;

   task Task_Typ_2;

   --  The following designate non-synchronized entities or protected/task
   --  types.

   Var_1 : Integer := 1 with Part_Of => Str;                         --  Error
   Var_2 : Integer := 2 with Part_Of => Prot_Typ_1;                  --  Error
   Var_3 : Integer := 3 with Part_Of => Task_Typ_1;                  --  Error
   Var_4 : Integer := 4;
   pragma Part_Of (Str);                                             --  Error
   Var_5 : Integer := 5;
   pragma Part_Of (Prot_Typ_1);                                      --  Error
   Var_6 : Integer := 6;
   pragma Part_Of (Task_Typ_1);                                      --  Error

   package Nested_1
     with Abstract_State =>
            ((State_1 with Part_Of => Str),                          --  Error
             (State_2 with Part_Of => Prot_Typ_1),                   --  Error
             (State_3 with Part_Of => Task_Typ_1))                   --  Error
   is end Nested_1;

   package Nested_2 is
      pragma Abstract_State
               (((State_1 with Part_Of => Str),                      --  Error
                 (State_2 with Part_Of => Prot_Typ_1),               --  Error
                 (State_3 with Part_Of => Task_Typ_1)));             --  Error
   end Nested_2;

   --  Constants cannot be part of synchronized units

   Con_1 : constant Integer := 1 with Part_Of => Prot_Typ_2;         --  Error
   Con_2 : constant Integer := 2 with Part_Of => Task_Typ_2;         --  Error
   Con_3 : constant Integer := 3;
   pragma Part_Of (Prot_Typ_2);                                      --  Error
   Con_4 : constant Integer := 4;
   pragma Part_Of (Task_Typ_2);                                      --  Error

   --  The evaluation of Part_Of occurs at the end of the visible declarations

   Var_7 : Integer := 7 with Part_Of => Prot_Typ_3;                  --  Error?
   Var_8 : Integer := 8 with Part_Of => Task_Typ_3;                  --  Error?
   Var_9 : Integer := 9;
   pragma Part_Of (Prot_Typ_3);                                      --  Error?
   Var_10 : Integer := 10;
   pragma Part_Of (Task_Typ_3);                                      --  Error?

   package Nested_3
     with Abstract_State =>
            ((State_1 with Part_Of => Prot_Typ_3),                   --  Error
             (State_2 with Part_Of => Task_Typ_3))                   --  Error
   is end Nested_3;

   package Nested_4 is
      pragma Abstract_State
               (((State_1 with Part_Of => Prot_Typ_3),               --  Error
                 (State_2 with Part_Of => Task_Typ_3)));             --  Error
   end Nested_4;

   --  The following are not in the same declarative region

   package Outer is
      package Inner is
         Var_11 : Integer := 11 with Part_Of => Prot_Typ_2;          --  Error
         Var_12 : Integer := 12 with Part_Of => Task_Typ_2;          --  Error
         Var_13 : Integer := 13;
         pragma Part_Of (Prot_Typ_2);                                --  Error
         Var_14 : Integer := 14;
         pragma Part_Of (Task_Typ_2);                                --  Error

         package Nested_5
           with Abstract_State =>
                  ((State_1 with Part_Of => Prot_Typ_2),             --  Error
                   (State_2 with Part_Of => Task_Typ_2))             --  Error
         is end Nested_5;

         package Nested_6 is
            pragma Abstract_State
                     (((State_1 with Part_Of => Prot_Typ_2),         --  Error
                       (State_2 with Part_Of => Task_Typ_2)));       --  Error
         end Nested_6;
      end Inner;
   end Outer;

private
   protected Prot_Typ_3 is
      entry Ent;
   end Prot_Typ_3;

   task Task_Typ_3;
end LR3a;

--  lr3b.ads

package LR3b
  with SPARK_Mode,
       Abstract_State => (State with External)
is
   procedure Force_Body;

private
   protected Prot_Typ_1 with Part_Of => State is                     --  OK
      entry Ent;
   end Prot_Typ_1;

   protected Prot_Typ_2 is
      pragma Part_Of (State);                                        --  OK
      entry Ent;
   end Prot_Typ_2;

   task Task_Typ_1 with Part_Of => State;                            --  OK

   task Task_Typ_2;
   pragma Part_Of (State);                                           --  OK

   Var_1 : Integer := 1 with Part_Of => Prot_Typ_1;
   Var_2 : Integer := 2 with Part_Of => Task_Typ_1;
   Var_3 : Integer := 3;
   pragma Part_Of (Prot_Typ_2);                                      --  OK
   Var_4 : Integer := 4;
   pragma Part_Of (Task_Typ_2);                                      --  OK
end LR3b;

--  lr3b.adb

package body LR3b
  with SPARK_Mode,
       Refined_State =>
         (State => (Prot_Typ_1, Prot_Typ_2, Task_Typ_1, Task_Typ_2))
is
   procedure Force_Body is begin null; end Force_Body;

   protected body Prot_Typ_1 is
      entry Ent when True is begin null; end Ent;
   end Prot_Typ_1;

   protected body Prot_Typ_2 is
      entry Ent when True is begin null; end Ent;
   end Prot_Typ_2;

   task body Task_Typ_1 is begin null; end Task_Typ_1;
   task body Task_Typ_2 is begin null; end Task_Typ_2;
end LR3b;

--  lr3c.ads

package LR3c
  with SPARK_Mode,
       Abstract_State => State
is
   procedure Force_Body;

private
   protected Prot_Typ is                                             --  Error
      entry Ent;
   end Prot_Typ;

   task Task_Typ;                                                    --  Error

   Var_1 : Integer := 1 with Part_Of => Prot_Typ;
   Var_2 : Integer := 2 with Part_Of => Task_Typ;
   Var_3 : Integer := 3;
   pragma Part_Of (Prot_Typ);
   Var_4 : Integer := 4;
   pragma Part_Of (Task_Typ);
end LR3c;

--  lr3c.adb

package body LR3c
  with SPARK_Mode,
       Refined_State => (State => (Var_1, Var_2, Var_3, Var_4))      --  Error
is
   procedure Force_Body is begin null; end Force_Body;

   protected body Prot_Typ is
      entry Ent when True is begin null; end Ent;
   end Prot_Typ;

   task body Task_Typ is begin null; end Task_Typ;
end LR3c;

--  fdi.ads

--  Full default initialization

package FDI with SPARK_Mode is

   --  Array-of-scalar type with Default_Component_Value

   type Arr_Typ_1 is array (1 .. 5) of Natural
     with Default_Component_Value => 0;

   --  Array type whose element type defines full initialization

   type Arr_Typ_2 is array (1 .. 5) of Arr_Typ_1;

   --  Private type whose Default_Initial_Condition aspect is non-null

   type Priv_Typ is private with Default_Initial_Condition => True;

   --  Protected type

   protected type Prot_Typ is
      entry Ent;
   private
      Comp_1 : Integer := 1;
      Comp_2 : Arr_Typ_1;
      Comp_3 : Arr_Typ_2;
   end Prot_Typ;

   --  Record type

   type Rec_Typ (Discr : Boolean) is record
      Comp_1 : Integer := 1;

      case Discr is
         when True =>
            Comp_2 : Arr_Typ_1;
         when others =>
            Comp_3 : Arr_Typ_2;
      end case;
   end record;

   --  Scalar type with Default_Value

   type Nat is new Natural range 1 .. 5 with Default_Value => 3;

   --  Task types

   task type Task_Typ;

   --  Type extension

   type Root is tagged record
      Comp_1 : Integer := 1;
      Comp_2 : Arr_Typ_1;
      Comp_3 : Arr_Typ_2;
      Comp_4 : Rec_Typ (True);
      Comp_5 : Nat;
   end record;

   type Deriv_Typ_1 is new Root with null record;
   type Deriv_Typ_2 is new Root with record
      Comp_6 : Boolean := True;
   end record;

   type Deriv_Typ_3 is new Rec_Typ;

private
   type Priv_Typ is null record;
end FDI;

--  lr4.ads

with FDI; use FDI;

package LR4 with SPARK_Mode is
   protected PT is
      entry Ent;
   end PT;

   task TT;

   Var_1  : Arr_Typ_1          with Part_Of => PT;                   --  OK
   Var_2  : Arr_Typ_2          with Part_Of => TT;                   --  OK
   Var_3  : Priv_Typ           with Part_Of => PT;                   --  OK
   Var_4  : Prot_Typ           with Part_Of => TT;                   --  OK
   Var_5  : Rec_Typ (False)    with Part_Of => PT;                   --  OK
   Var_6  : Nat                with Part_Of => TT;                   --  OK
   Var_7  : Task_Typ           with Part_Of => PT;                   --  OK
   Var_8  : Root               with Part_Of => TT;                   --  OK
   Var_9  : Deriv_Typ_1        with Part_Of => PT;                   --  OK
   Var_10 : Deriv_Typ_2        with Part_Of => TT;                   --  OK
   Var_11 : Deriv_Typ_3 (True) with Part_Of => PT;                   --  OK
   Var_12 : Natural := 12      with Part_Of => TT;                   --  OK
   Var_13 : Natural            with Part_Of => PT;                   --  OK
   pragma Import (C, Var_13, "__var_13");

   Var_14 : Arr_Typ_1;
   pragma Part_Of (PT);                                              --  OK
   Var_15 : Arr_Typ_2;
   pragma Part_Of (TT);                                              --  OK
   Var_16 : Priv_Typ;
   pragma Part_Of (PT);                                              --  OK
   Var_17 : Prot_Typ;
   pragma Part_Of (TT);                                              --  OK
   Var_18 : Rec_Typ (False);
   pragma Part_Of (PT);                                              --  OK
   Var_19 : Nat;
   pragma Part_Of (TT);                                              --  OK
   Var_20 : Task_Typ;
   pragma Part_Of (PT);                                              --  OK
   Var_21 : Root;
   pragma Part_Of (TT);                                              --  OK
   Var_22 : Deriv_Typ_1;
   pragma Part_Of (PT);                                              --  OK
   Var_23 : Deriv_Typ_2;
   pragma Part_Of (TT);                                              --  OK
   Var_24 : Deriv_Typ_3 (True);
   pragma Part_Of (PT);                                              --  OK
   Var_25 : Natural := 12;
   pragma Part_Of (TT);                                              --  OK
   Var_26 : Natural;
   pragma Part_Of (PT);                                              --  OK
   pragma Import (C, Var_26, "__var_26");
   Var_27 : Natural;
   pragma Import (C, Var_27, "__var_27");
   pragma Part_Of (TT);                                              --  OK
end LR4;

--  lr4a.ads

package LR4a with SPARK_Mode is
   protected PT is
      entry Ent;
   end PT;

   task TT;

   type Rec_Typ is record
      Comp : Integer;
   end record;

   Var_1 : Natural with Part_Of => PT;                               --  Error
   Var_2 : Rec_Typ with Part_Of => TT;                               --  Error
   Var_3 : Natural;
   pragma Part_Of (PT);                                              --  Error
   Var_4 : Natural;
   pragma Part_Of (TT);                                              --  Error
end LR4a;

--  yso.ads

--  Yields synchronized object

with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control;

package YSO with SPARK_Mode is

   --  Protected interface

   type Prot_Iface is protected interface;

   --  Protected type

   protected type Prot_Typ is
      entry Ent;
   end Prot_Typ;

   --  Synchronized interface

   type Sync_Iface is synchronized interface;

   --  Task interface

   type Task_Iface is task interface;

   --  Task type

   task type Task_Typ;

   --  Array type

   type Arr_Typ is array (1 .. 5) of Prot_Typ;

   --  Descendant of Suspension_Object

   type Sus_Obj is new Suspension_Object;

   --  Record type

   type Rec_Typ is record
      Comp_1 : Prot_Typ;
      Comp_2 : Task_Typ;
      Comp_3 : Arr_Typ;
      Comp_4 : Sus_Obj;
      Comp_5 : Suspension_Object;
   end record with Volatile;

   --  Type extension

   type Deriv_Typ is new Rec_Typ;
end YSO;

--  lr5.ads

with YSO; use YSO;

package LR5 with SPARK_Mode is
   type Rec_1 is record
      Comp_1 : Integer := 1;
      Comp_2 : Prot_Typ;                                             --  Error
   end record with Volatile;

   type Rec_2 is record
      Comp_1 : Integer := 1;
      Comp_2 : Task_Typ;                                             --  Error
   end record with Volatile;

   type Rec_3 is record
      Comp_1 : Integer := 1;
      Comp_2 : Arr_Typ;                                              --  Error
   end record with Volatile;

   type Rec_4 is record
      Comp_1 : Integer := 1;
      Comp_2 : Sus_Obj;                                              --  Error
   end record with Volatile;

   type Rec_5 is record
      Comp_1 : Integer := 1;
      Comp_2 : Rec_Typ;                                              --  Error
   end record with Volatile;

   type Rec_6 is record
      Comp_1 : Integer := 1;
      Comp_2 : Deriv_Typ;                                            --  Error
   end record with Volatile;
end LR5;

--  lr6.ads

with YSO; use YSO;

package LR6
  with SPARK_Mode,
       Abstract_State => (State with External, Synchronous)
is
   procedure Force_Body;

private
   protected PT_1 with Part_Of => State is
      entry Ent;
   end PT_1;

   protected PT_2 is
      pragma Part_Of (State);
      entry Ent;
   end PT_2;

   task TT_1 with Part_Of => State;

   task TT_2;
   pragma Part_Of (State);

   Obj_1 : Prot_Typ with Part_Of => State;
   Obj_2 : Task_Typ with Part_Of => State;
   Obj_3 : Prot_Typ;
   pragma Part_Of (State);
   Obj_4 : Task_Typ;
   pragma Part_Of (State);

   package Nested_1
     with Abstract_State =>
            (State_1 with External, Synchronous, Part_Of => State)
   is end Nested_1;

   package Nested_2 is
      pragma Abstract_State
               ((State_2 with External, Synchronous, Part_Of => State));
   end Nested_2;
end LR6;

--  lr6.adb

with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control;

package body LR6
  with SPARK_Mode,
       Refined_State =>
         (State =>
           (PT_1,
            PT_2,
            TT_1,
            TT_2,
            Obj_1,
            Obj_2,
            Obj_3,
            Obj_4,
            Nested_1.State_1,
            Nested_2.State_2,
            Obj_5,
            Obj_6,
            Obj_7,
            Obj_8,
            Obj_9,
            Obj_10,
            Obj_11,
            Obj_12,
            Obj_13,
            Obj_14,
            Nested_3.State_3,
            Nested_4.State_4))
is
   Obj_5  : Prot_Typ;
   Obj_6  : Task_Typ;
   Obj_7  : Arr_Typ;
   Obj_8  : Sus_Obj;
   Obj_9  : Suspension_Object;
   Obj_10 : Rec_Typ;
   Obj_11 : Deriv_Typ;
   Obj_12 : Integer := 12 with Atomic, Async_Writers => True;
   Obj_13 : Integer := 13 with Constant_After_Elaboration;
   Obj_14 : constant Integer := 14;

   package Nested_3
     with Abstract_State => (State_3 with External, Synchronous)
   is end Nested_3;

   package Nested_4 is
      pragma Abstract_State ((State_4 with External, Synchronous));
   end Nested_4;

   package body Nested_1
     with Refined_State => (State_1 => null)
   is end Nested_1;

   package body Nested_2
     with Refined_State => (State_2 => null)
   is end Nested_2;

   package body Nested_3
     with Refined_State => (State_3 => null)
   is end Nested_3;

   package body Nested_4
     with Refined_State => (State_4 => null)
   is end Nested_4;

   procedure Force_Body is begin null; end Force_Body;

   protected body PT_1 is
      entry Ent when True is begin null; end Ent;
   end PT_1;

   protected body PT_2 is
      entry Ent when True is begin null; end Ent;
   end PT_2;

   task body TT_1 is begin null; end TT_1;
   task body TT_2 is begin null; end TT_2;
end LR6;

--  lr6a.ads

package LR6a
  with SPARK_Mode,
       Abstract_State => (State with External, Synchronous)
is
   procedure Force_Body;

private
   Obj_1 : Integer := 1 with Part_Of => State;

   package Nested_1
     with Abstract_State => (State_1 with Part_Of => State)
   is end Nested_1;
end LR6a;

--  lr6a.adb

package body LR6a
  with SPARK_Mode,
       Refined_State =>
         (State =>
           (Obj_1,                                                   --  Error
            Nested_1.State_1,                                        --  Error
            Obj_2,                                                   --  Error
            Nested_2.State_2))                                       --  Error
is
   Obj_2 : Integer := 2;

   package Nested_2
     with Abstract_State => State_2
   is end Nested_2;

   procedure Force_Body is begin null; end Force_Body;

   package body Nested_1
     with Refined_State => (State_1 => null)
   is end Nested_1;

   package body Nested_2
     with Refined_State => (State_2 => null)
   is end Nested_2;
end LR6a;

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

$ gcc -c lr3.ads  -gnatc
$ gcc -c lr3a.ads
$ gcc -c lr3b.adb
$ gcc -c lr3c.adb
$ gcc -c lr4.ads  -gnatc
$ gcc -c lr4a.ads
$ gcc -c lr5.ads
$ gcc -c lr6.adb
$ gcc -c lr6a.adb
lr3a.ads:19:41: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:20:41: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:21:41: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:23:20: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:25:20: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:27:20: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:31:39: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:32:39: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:33:39: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:38:43: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:39:43: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:40:43: indicator Part_Of must denote abstract state, single protected
  type or single task type
lr3a.ads:45:39: consant "Con_1" cannot act as constituent of single protected
  type "Prot_Typ_2"
lr3a.ads:46:39: consant "Con_2" cannot act as constituent of single task type
  "Task_Typ_2"
lr3a.ads:48:04: consant "Con_3" cannot act as constituent of single protected
  type "Prot_Typ_2"
lr3a.ads:50:04: consant "Con_4" cannot act as constituent of single task type
  "Task_Typ_2"
lr3a.ads:63:39: "Prot_Typ_3" is undefined (more references follow)
lr3a.ads:64:39: "Task_Typ_3" is undefined (more references follow)
lr3a.ads:77:38: constituent "Var_11" must be declared immediately within the
  same region as single protected type "Prot_Typ_2"
lr3a.ads:78:38: constituent "Var_12" must be declared immediately within the
  same region as single task type "Task_Typ_2"
lr3a.ads:80:10: constituent "Var_13" must be declared immediately within the
  same region as single protected type "Prot_Typ_2"
lr3a.ads:82:10: constituent "Var_14" must be declared immediately within the
  same region as single task type "Task_Typ_2"
lr3a.ads:86:34: constituent "State_1" must be declared immediately within the
  same region as single protected type "Prot_Typ_2"
lr3a.ads:87:34: constituent "State_2" must be declared immediately within the
  same region as single task type "Task_Typ_2"
lr3a.ads:92:38: constituent "State_1" must be declared immediately within the
  same region as single protected type "Prot_Typ_2"
lr3a.ads:93:38: constituent "State_2" must be declared immediately within the
  same region as single task type "Task_Typ_2"
lr3c.adb:3:36: "Var_1" cannot act as constituent of state "State"
lr3c.adb:3:36: Part_Of indicator specifies encapsulator "Prot_Typ"
lr3c.adb:3:43: "Var_2" cannot act as constituent of state "State"
lr3c.adb:3:43: Part_Of indicator specifies encapsulator "Task_Typ"
lr3c.adb:3:50: "Var_3" cannot act as constituent of state "State"
lr3c.adb:3:50: Part_Of indicator specifies encapsulator "Prot_Typ"
lr3c.adb:3:57: "Var_4" cannot act as constituent of state "State"
lr3c.adb:3:57: Part_Of indicator specifies encapsulator "Task_Typ"
lr3c.ads:8:14: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
lr3c.ads:8:14: "Prot_Typ" is declared in the private part of package "Lr3c"
lr3c.ads:12:09: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
lr3c.ads:12:09: "Task_Typ" is declared in the private part of package "Lr3c"
lr4a.ads:12:04: "Var_1" requires full default initialization
lr4a.ads:12:04: object acts as constituent of single protected type "Pt"
lr4a.ads:13:04: "Var_2" requires full default initialization
lr4a.ads:13:04: object acts as constituent of single task type "Tt"
lr4a.ads:14:04: "Var_3" requires full default initialization
lr4a.ads:14:04: object acts as constituent of single protected type "Pt"
lr4a.ads:16:04: "Var_4" requires full default initialization
lr4a.ads:16:04: object acts as constituent of single task type "Tt"
lr5.ads:6:07: component "Comp_2" of non-synchronized type "REC_1" cannot be
  synchronized
lr5.ads:11:07: component "Comp_2" of non-synchronized type "REC_2" cannot be
  synchronized
lr5.ads:16:07: component "Comp_2" of non-synchronized type "REC_3" cannot be
  synchronized
lr5.ads:21:07: component "Comp_2" of non-synchronized type "REC_4" cannot be
  synchronized
lr5.ads:26:07: component "Comp_2" of non-synchronized type "REC_5" cannot be
  synchronized
lr5.ads:31:07: component "Comp_2" of non-synchronized type "REC_6" cannot be
  synchronized
lr6.adb:33:04: warning: variable "Obj_8" is read but never assigned
lr6.adb:34:04: warning: variable "Obj_9" is read but never assigned
lr6.adb:35:04: warning: variable "Obj_10" is read but never assigned
lr6.adb:36:04: warning: variable "Obj_11" is read but never assigned
lr6a.adb:4:11: external state "State" requires at least one external
  constituent or null refinement
lr6a.adb:5:13: constituent of synchronized state "State" must be synchronized
lr6a.adb:6:21: constituent of synchronized state "State" must be synchronized
lr6a.adb:7:13: constituent of synchronized state "State" must be synchronized
lr6a.adb:8:21: constituent of synchronized state "State" must be synchronized

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

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

	* aspects.adb (Move_Or_Merge_Aspects): Move all aspects related
	to a single concurrent type declaration to the declaration
	of the anonymous object if they qualify.
	(Relocate_Aspect): Update comment on usage.
	* aspects.ads Add new sectioon on aspect specifications on single
	concurrent types. Add new table Aspect_On_Anonymous_Object_OK.
	(Move_Or_Merge_Aspects): Udate the comment on usage.
	* atree.adb (Elist36): New routine.
	(Set_Elist36): New routine.
	* atree.ads (Elist36): New routine along with pragma Inline.
	(Set_Elist36): New routine along with pragma Inline.
	* atree.h: Elist36 is now an alias for Field36.
	* contracts.adb (Add_Contract_Item): Add processing
	for protected units and extra processing for variables.
	(Analyze_Object_Contract): Code cleanup. The processing of
	Part_Of now depends on wherer the object is a constant or
	a variable. Add processing for pragmas Depends and Global
	when they apply to a single concurrent object. Verify that a
	variable which is part of a single concurrent type has full
	default initialization. Set/restore the SPARK_Mode of a single
	concurrent object.
	(Analyze_Protected_Contract): New routine.
	* contracts.ads (Add_Contract_Item): Update the comment on usage.
	(Analyze_Object_Contract): Update the comment on usage.
	(Analyze_Protected_Contract): New routine.
	(Analyze_Task_Contract): Update the comment on usage.
	* einfo.adb Part_Of_Constituents now uses Elist10.
	(Anonymous_Object): New routine.
	(Contract): Code cleanup.
	(Has_Option): Remove the assumption that the only simple
	option is External.
	(Is_Synchronized_State): New routine.
	(Part_Of_Constituents): This attribute applies to
	variables and uses Elist10.
	(Set_Anonymous_Object): New routine.
	(Set_Contract): Code cleanup.
	(Set_Part_Of_Constituents): This attribute applies to variables and
	uses Elist10.
	(Set_SPARK_Aux_Pragma): Code cleanup.
	(Set_SPARK_Aux_Pragma_Inherited): Code cleanup.
	(Set_SPARK_Pragma): Code cleanup. This attribute applies to
	variables.
	(Set_SPARK_Pragma_Inherited): Code cleanup. This
	attribute applies to variables.
	(SPARK_Aux_Pragma): Code cleanup.
	(SPARK_Aux_Pragma_Inherited): Code cleanup.
	(SPARK_Pragma): Code cleanup. This attribute applies to variables.
	(SPARK_Pragma_Inherited): Code cleanup. This attribute applies
	to variables.
	(Write_Field9_Name): Remove the output for Part_Of_Constituents.
	(Write_Field10_Name): Add output for Part_Of_Constituents.
	(Write_Field30_Name): Add output for Anonymous_Object.
	(Write_Field34_Name): Output SPARK_Pragma
	for protected types and variables.
	* einfo.ads: New attributes Anonymous_Object and
	Is_Synchronized_State along with usage in entities. Update
	the documentation of attributes Contract Encapsulating_State
	Part_Of_Constituents SPARK_Aux_Pragma SPARK_Aux_Pragma_Inherited
	SPARK_Pragma SPARK_Pragma_Inherited (Anonymous_Object): New
	routine along with pragma Inline.
	(Is_Synchronized_State): New routine.
	(Set_Anonymous_Object): New routine along with pragma Inline.
	* freeze.adb (Freeze_Record_Type): Ensure that a non-synchronized
	record does not have synchronized components.
	* sem_ch3.adb (Analyze_Declarations): Code cleanup. Analyze the
	contract of protected units.
	* sem_ch9.adb Add with and use clauses for Sem_Prag. Code cleanup.
	(Analyze_Single_Protected_Declaration): Reimplemented.
	(Analyze_Single_Task_Declaration): Reimplemented.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Aspect Part_Of
	can now apply to a single concurrent type declaration. Rely on
	Insert_Pragma to place the pragma.  Update the error message on
	usage to reflect the new context.
	(Insert_Pragma): When inserting
	pragmas for a protected or task type, create a definition if
	the type lacks one.
	* sem_elab.adb (Check_A_Call): Code cleanup. Issue error message
	related to elaboration issues for SPARK when SPARK_Mode is "on"
	and the offending entity comes from source.
	* sem_prag.adb (Analyze_Abstract_State): Add new flag
	Synchronous_Seen. Update the analysis of simple options Externa,
	Ghost and Synchronous. Update various error messages to reflect
	the use of single concurrent types.
	(Analyze_Depends_Global): Pragmas Depends and Global can now apply to
	a single task type or a single concurrent object created for a task
	type.
	(Analyze_Depends_In_Decl_Part): Do not push a scope when the
	context is a single concurrent object.	(Analyze_Part_Of):
	Moved out of Analyze_Pragma. The routine has a new profile
	and comment on usage.
	(Analyze_Part_Of_In_Decl_Part): New routine.
	(Analyze_Part_Of_Option): Update the call to Analyze_Part_Of.
	(Analyze_Pragma): Pragma Abstract_State can
	now carry simple option Synchronous. Pragma Part_Of can now
	apply to a single concurrent type declaration. The analysis
	of pragma Part_Of is delayed when the context is a single
	concurrent object.
	(Analyze_Refined_Depends_In_Decl_Part): Use the anonymous object when
	the context is a single concurren type.
	(Analyze_Refined_Global_In_Decl_Part): Use the
	anonymous object when the context is a single concurren type.
	(Check_Ghost_Constituent): Removed.
	(Check_Matching_Constituent): Renamed to Match_Constituent.
	(Check_Matching_State): Renamed to Match_State.
	(Collect_Constituent): Update the comment
	on usage. Verify various legality rules related to ghost and
	synchronized entities.
	(Find_Related_Declaration_Or_Body): A single task declaration is no
	longer a valid context for a pragma.
	(Fix_Msg): Moved to Sem_Util.
	(Process_Overloadable): Add processing for single task objects.
	(Process_Visible_Part): Add processing for single concurrent
	types.
	(Relocate_Pragmas_To_Anonymous_Object): New routine.
	* sem_prag.ads Add new table Pragma_On_Anonymous_Object_OK.
	(Analyze_Part_Of_In_Decl_Part): New routine.
	(Relocate_Pragmas_To_Anonymous_Object): New routine.
	* sem_util.adb (Defining_Entity): Code cleanup.
	(Fix_Msg): Moved from Sem_Prag and augmented to handle
	mode replacements.
	(Has_Full_Default_Initialization): New routine.
	(Is_Descendant_Of_Suspension_Object): Moved out of
	Is_Effectively_Volatile.
	(Is_Single_Concurrent_Object): New routine.
	(Is_Single_Concurrent_Type): New routine.
	(Is_Single_Concurrent_Type_Declaration): New routine.
	(Is_Synchronized_Object): New routine.
	(Yields_Synchronized_Object): New routine.
	* sem_util.ads (Fix_Msg): Moved form Sem_Prag. Update the
	comment on usage.
	(Has_Full_Default_Initialization): New routine.
	(Is_Single_Concurrent_Object): New routine.
	(Is_Single_Concurrent_Type): New routine.
	(Is_Single_Concurrent_Type_Declaration): New routine.
	(Is_Synchronized_Object): New routine.
	(Yields_Synchronized_Object): New routine.
	* snames.ads-tmpl: Add name Synchronous.

[Ada] Protected and task units in SPARK

Commit Message

Patch