[multiple changes]

2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry in table Canonical_Aspect for
	Initial_Condition.
	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
	Aspect_Names and Aspect_Delay for Initial_Condition.
	* einfo.adb (Get_Pragma): Include pragma Initial_Condition to
	categorization pragmas.
	* einfo.ads (Get_Pragma): Update comment on usage.
	* exp_ch7.adb (Expand_N_Package_Body): Add a runtime check to
	verify the assertion introduced by pragma Initial_Condition.
	(Expand_N_Package_Declaration): Add a runtime check to
	verify the assertion introduced by pragma Initial_Condition.
	(Expand_Pragma_Initial_Condition): New routine.
	* par-prag: Include pragma Initial_Condition to the list of
	pragmas that do not require special processing by the parser.
	* sem_ch3.adb (Analyze_Declarations): Analyze pragma
	Initial_Condition at the end of the visible declarations.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Initial_Condition.
	(Check_Aspect_At_Freeze_Point):
	Aspect Initial_Condition does not need inspection at freezing.
	* sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part):
	New routine.
	(Analyze_Pragma): Update all calls
	to Check_Declaration_Order. Add processing for pragma
	Initial_Condition. Initial_Condition is now a valid assertion
	kind.  Add an entry in table Sig_Flags for Initial_Condition.
	(Check_Declaration_Order): Reimplemented to handle arbitrary
	pragmas.
	(Is_Valid_Assertion_Kind): Add an entry for
	Initial_Condition.
	* sem_pag.ads (Analyze_Initial_Condition_In_Decl_Part):
	New routine.
	* sem_util.adb (Add_Contract_Item): Pragma Initial_Condition
	can now be associated with a package spec.
	* sem_util.ads (Add_Contract_Item): Update comment on usage.
	* sinfo.ads: Update the documentation of node N_Contract
	* snames.ads-tmpl: Add new predefined name Initial_Condition. Add
	new pragma id for Initial_Condition.

2013-10-14  Thomas Quinot  <quinot@adacore.com>

	* exp_pakd.adb: Minor reformatting.

From-SVN: r203551

gcc/ada/ChangeLog

+2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb: Add an entry in table Canonical_Aspect for
+	Initial_Condition.
+	* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
+	Aspect_Names and Aspect_Delay for Initial_Condition.
+	* einfo.adb (Get_Pragma): Include pragma Initial_Condition to
+	categorization pragmas.
+	* einfo.ads (Get_Pragma): Update comment on usage.
+	* exp_ch7.adb (Expand_N_Package_Body): Add a runtime check to
+	verify the assertion introduced by pragma Initial_Condition.
+	(Expand_N_Package_Declaration): Add a runtime check to
+	verify the assertion introduced by pragma Initial_Condition.
+	(Expand_Pragma_Initial_Condition): New routine.
+	* par-prag: Include pragma Initial_Condition to the list of
+	pragmas that do not require special processing by the parser.
+	* sem_ch3.adb (Analyze_Declarations): Analyze pragma
+	Initial_Condition at the end of the visible declarations.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
+	for aspect Initial_Condition.
+	(Check_Aspect_At_Freeze_Point):
+	Aspect Initial_Condition does not need inspection at freezing.
+	* sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part):
+	New routine.
+	(Analyze_Pragma): Update all calls
+	to Check_Declaration_Order. Add processing for pragma
+	Initial_Condition. Initial_Condition is now a valid assertion
+	kind.  Add an entry in table Sig_Flags for Initial_Condition.
+	(Check_Declaration_Order): Reimplemented to handle arbitrary
+	pragmas.
+	(Is_Valid_Assertion_Kind): Add an entry for
+	Initial_Condition.
+	* sem_pag.ads (Analyze_Initial_Condition_In_Decl_Part):
+	New routine.
+	* sem_util.adb (Add_Contract_Item): Pragma Initial_Condition
+	can now be associated with a package spec.
+	* sem_util.ads (Add_Contract_Item): Update comment on usage.
+	* sinfo.ads: Update the documentation of node N_Contract
+	* snames.ads-tmpl: Add new predefined name Initial_Condition. Add
+	new pragma id for Initial_Condition.
+
+2013-10-14  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_pakd.adb: Minor reformatting.
+
 2013-10-14  Robert Dewar  <dewar@adacore.com>
 
 	* exp_prag.adb: Minor reformatting.

gcc/ada/aspects.adb

@@ -440,6 +440,7 @@ package body Aspects is
     Aspect_Independent_Components       => Aspect_Independent_Components,
     Aspect_Inline                       => Aspect_Inline,
     Aspect_Inline_Always                => Aspect_Inline,
+    Aspect_Initial_Condition            => Aspect_Initial_Condition,
     Aspect_Initializes                  => Aspect_Initializes,
     Aspect_Input                        => Aspect_Input,
     Aspect_Interrupt_Handler            => Aspect_Interrupt_Handler,

gcc/ada/aspects.ads

@@ -96,6 +96,7 @@ package Aspects is
       Aspect_External_Tag,
       Aspect_Global,                        -- GNAT
       Aspect_Implicit_Dereference,
+      Aspect_Initial_Condition,             -- GNAT
       Aspect_Initializes,                   -- GNAT
       Aspect_Input,
       Aspect_Interrupt_Priority,
@@ -310,6 +311,7 @@ package Aspects is
       Aspect_External_Tag            => Expression,
       Aspect_Global                  => Expression,
       Aspect_Implicit_Dereference    => Name,
+      Aspect_Initial_Condition       => Expression,
       Aspect_Initializes             => Expression,
       Aspect_Input                   => Name,
       Aspect_Interrupt_Priority      => Expression,
@@ -400,6 +402,7 @@ package Aspects is
       Aspect_Independent_Components       => Name_Independent_Components,
       Aspect_Inline                       => Name_Inline,
       Aspect_Inline_Always                => Name_Inline_Always,
+      Aspect_Initial_Condition            => Name_Initial_Condition,
       Aspect_Initializes                  => Name_Initializes,
       Aspect_Input                        => Name_Input,
       Aspect_Interrupt_Handler            => Name_Interrupt_Handler,
@@ -600,6 +603,7 @@ package Aspects is
       Aspect_Independent_Components       => Always_Delay,
       Aspect_Inline                       => Always_Delay,
       Aspect_Inline_Always                => Always_Delay,
+      Aspect_Initial_Condition            => Always_Delay,
       Aspect_Initializes                  => Always_Delay,
       Aspect_Input                        => Always_Delay,
       Aspect_Interrupt_Handler            => Always_Delay,

gcc/ada/einfo.adb

@@ -6303,6 +6303,7 @@ package body Einfo is
                   Id = Pragma_Abstract_State    or else
                   Id = Pragma_Depends           or else
                   Id = Pragma_Global            or else
+                  Id = Pragma_Initial_Condition or else
                   Id = Pragma_Initializes       or else
                   Id = Pragma_Refined_Depends   or else
                   Id = Pragma_Refined_Global    or else

gcc/ada/einfo.ads

@@ -7442,6 +7442,8 @@ package Einfo is
    --    Contract_Cases
    --    Depends
    --    Global
+   --    Initial_Condition
+   --    Initializes
    --    Precondition
    --    Postcondition
    --    Refined_Depends

gcc/ada/exp_ch7.adb

@@ -368,6 +368,11 @@ package body Exp_Ch7 is
    --  Given an arbitrary entity, traverse the scope chain looking for the
    --  first enclosing function. Return Empty if no function was found.
 
+   procedure Expand_Pragma_Initial_Condition (N : Node_Id);
+   --  Subsidiary to the expansion of package specs and bodies. Generate a
+   --  runtime check needed to verify the assumption introduced by pragma
+   --  Initial_Condition. N denotes the package spec or body.
+
    function Make_Call
      (Loc        : Source_Ptr;
       Proc_Id    : Entity_Id;
@@ -3959,6 +3964,15 @@ package body Exp_Ch7 is
          end if;
 
          Build_Task_Activation_Call (N);
+
+         --  When the package is subject to pragma Initial_Condition, the
+         --  assertion expression must be verified at the end of the body
+         --  statements.
+
+         if Present (Get_Pragma (Spec_Ent, Pragma_Initial_Condition)) then
+            Expand_Pragma_Initial_Condition (N);
+         end if;
+
          Pop_Scope;
       end if;
 
@@ -4053,10 +4067,9 @@ package body Exp_Ch7 is
       if No_Body then
          Push_Scope (Id);
 
-         if Has_RACW (Id) then
-
          --  Generate RACW subprogram bodies
 
+         if Has_RACW (Id) then
             Decls := Private_Declarations (Spec);
 
             if No (Decls) then
@@ -4072,13 +4085,21 @@ package body Exp_Ch7 is
             Analyze_List (Decls);
          end if;
 
-         if Present (Activation_Chain_Entity (N)) then
-
          --  Generate task activation call as last step of elaboration
 
+         if Present (Activation_Chain_Entity (N)) then
             Build_Task_Activation_Call (N);
          end if;
 
+         --  When the package is subject to pragma Initial_Condition and lacks
+         --  a body, the assertion expression must be verified at the end of
+         --  the visible declarations. Otherwise the check is performed at the
+         --  end of the body statements (see Expand_N_Package_Body).
+
+         if Present (Get_Pragma (Id, Pragma_Initial_Condition)) then
+            Expand_Pragma_Initial_Condition (N);
+         end if;
+
          Pop_Scope;
       end if;
 
@@ -4114,6 +4135,88 @@ package body Exp_Ch7 is
       end if;
    end Expand_N_Package_Declaration;
 
+   -------------------------------------
+   -- Expand_Pragma_Initial_Condition --
+   -------------------------------------
+
+   procedure Expand_Pragma_Initial_Condition (N : Node_Id) is
+      Loc       : constant Source_Ptr := Sloc (N);
+      Check     : Node_Id;
+      Expr      : Node_Id;
+      Init_Cond : Node_Id;
+      List      : List_Id;
+      Pack_Id   : Entity_Id;
+
+   begin
+      if Nkind (N) = N_Package_Body then
+         Pack_Id := Corresponding_Spec (N);
+
+         if Present (Handled_Statement_Sequence (N)) then
+            List := Statements (Handled_Statement_Sequence (N));
+
+         --  The package body lacks statements, create an empty list
+
+         else
+            List := New_List;
+
+            Set_Handled_Statement_Sequence (N,
+              Make_Handled_Sequence_Of_Statements (Loc, Statements => List));
+         end if;
+
+      elsif Nkind (N) = N_Package_Declaration then
+         Pack_Id := Defining_Entity (N);
+
+         if Present (Visible_Declarations (Specification (N))) then
+            List := Visible_Declarations (Specification (N));
+
+         --  The package lacks visible declarations, create an empty list
+
+         else
+            List := New_List;
+
+            Set_Visible_Declarations (Specification (N), List);
+         end if;
+
+      --  This routine should not be used on anything other than packages
+
+      else
+         raise Program_Error;
+      end if;
+
+      Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
+
+      --  The caller should check whether the package is subject to pragma
+      --  Initial_Condition.
+
+      pragma Assert (Present (Init_Cond));
+
+      Expr :=
+        Get_Pragma_Arg (First (Pragma_Argument_Associations (Init_Cond)));
+
+      --  The assertion expression was found to be illegal, do not generate the
+      --  runtime check as it will repeat the illegality.
+
+      if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
+         return;
+      end if;
+
+      --  Generate:
+      --    pragma Check (Initial_Condition, <Expr>);
+
+      Check :=
+        Make_Pragma (Loc,
+          Chars                        => Name_Check,
+          Pragma_Argument_Associations => New_List (
+            Make_Pragma_Argument_Association (Loc,
+              Expression => Make_Identifier (Loc, Name_Initial_Condition)),
+
+            Make_Pragma_Argument_Association (Loc,
+              Expression => New_Copy_Tree (Expr))));
+
+      Append_To (List, Check);
+      Analyze (Check);
+   end Expand_Pragma_Initial_Condition;
+
    -----------------------------
    -- Find_Node_To_Be_Wrapped --
    -----------------------------

gcc/ada/exp_pakd.adb

@@ -1326,8 +1326,8 @@ package body Exp_Pakd is
       --  The expression for the shift value that is required
 
       Shift_Used : Boolean := False;
-      --  Set True if Shift has been used in the generated code at least
-      --  once, so that it must be duplicated if used again
+      --  Set True if Shift has been used in the generated code at least once,
+      --  so that it must be duplicated if used again.
 
       New_Lhs : Node_Id;
       New_Rhs : Node_Id;

gcc/ada/par-prag.adb

@@ -1185,6 +1185,7 @@ begin
            Pragma_Import_Valued_Procedure        |
            Pragma_Independent                    |
            Pragma_Independent_Components         |
+           Pragma_Initial_Condition              |
            Pragma_Initialize_Scalars             |
            Pragma_Initializes                    |
            Pragma_Inline                         |

gcc/ada/sem_ch13.adb

@@ -2053,6 +2053,45 @@ package body Sem_Ch13 is
                   Insert_Delayed_Pragma (Aitem);
                   goto Continue;
 
+               --  Initial_Condition
+
+               --  Aspect Initial_Condition covers the visible declarations of
+               --  a package and all hidden states through functions. As such,
+               --  it must be evaluated at the end of the said declarations.
+
+               when Aspect_Initial_Condition => Initial_Condition : declare
+                  Decls : List_Id;
+
+               begin
+                  if Nkind_In (N, N_Generic_Package_Declaration,
+                                  N_Package_Declaration)
+                  then
+                     Decls := Visible_Declarations (Specification (N));
+
+                     Make_Aitem_Pragma
+                       (Pragma_Argument_Associations => New_List (
+                          Make_Pragma_Argument_Association (Loc,
+                            Expression => Relocate_Node (Expr))),
+                        Pragma_Name                  =>
+                          Name_Initial_Condition);
+                     Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+
+                     if No (Decls) then
+                        Decls := New_List;
+                        Set_Visible_Declarations (N, Decls);
+                     end if;
+
+                     Prepend_To (Decls, Aitem);
+
+                  else
+                     Error_Msg_NE
+                       ("aspect & must apply to a package declaration",
+                        Aspect, Id);
+                  end if;
+
+                  goto Continue;
+               end Initial_Condition;
+
                --  Initializes
 
                --  Aspect Initializes coverts the visible declarations of a
@@ -7849,6 +7888,7 @@ package body Sem_Ch13 is
               Aspect_Dimension            |
               Aspect_Dimension_System     |
               Aspect_Implicit_Dereference |
+              Aspect_Initial_Condition    |
               Aspect_Initializes          |
               Aspect_Post                 |
               Aspect_Postcondition        |

gcc/ada/sem_ch3.adb

@@ -2224,9 +2224,9 @@ package body Sem_Ch3 is
       if Present (L) then
          Context := Parent (L);
 
-         --  Analyze aspect/pragma Initializes of a package at the end of the
-         --  visible declarations as the aspect/pragma has visibility over the
-         --  said region.
+         --  Analyze pragmas Initializes and Initial_Condition of a package at
+         --  the end of the visible declarations as the pragmas have visibility
+         --  over the said region.
 
          if Nkind (Context) = N_Package_Specification
            and then L = Visible_Declarations (Context)
@@ -2238,6 +2238,12 @@ package body Sem_Ch3 is
                Analyze_Initializes_In_Decl_Part (Prag);
             end if;
 
+            Prag := Get_Pragma (Spec_Id, Pragma_Initial_Condition);
+
+            if Present (Prag) then
+               Analyze_Initial_Condition_In_Decl_Part (Prag);
+            end if;
+
          --  Analyze the state refinements within a package body now, after
          --  all hidden states have been encountered and freely visible.
          --  Refinements must be processed before pragmas Refined_Depends and

gcc/ada/sem_prag.ads

@@ -64,6 +64,9 @@ package Sem_Prag is
    --  Perform full analysis of delayed pragma Global. This routine is also
    --  capable of performing basic analysis of pragma Refind_Global.
 
+   procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id);
+   --  Perform full analysis of delayed pragma Initial_Condition
+
    procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
    --  Perform full analysis of delayed pragma Initializes
 

gcc/ada/sem_util.adb

@@ -229,10 +229,14 @@ package body Sem_Util is
       --  Contract items related to [generic] packages. The applicable pragmas
       --  are:
       --    Abstract_States
+      --    Initial_Condition
       --    Initializes
 
       if Ekind_In (Id, E_Generic_Package, E_Package) then
-         if Nam_In (Nam, Name_Abstract_State, Name_Initializes) then
+         if Nam_In (Nam, Name_Abstract_State,
+                         Name_Initial_Condition,
+                         Name_Initializes)
+         then
             Set_Next_Pragma (Prag, Classifications (Items));
             Set_Classifications (Items, Prag);
 

gcc/ada/sem_util.ads

@@ -50,6 +50,7 @@ package Sem_Util is
    --    Contract_Cases
    --    Depends
    --    Global
+   --    Initial_Condition
    --    Initializes
    --    Postcondition
    --    Precondition

gcc/ada/sinfo.ads

@@ -7198,6 +7198,7 @@ package Sinfo is
       --    Abstract_States
       --    Depends
       --    Global
+      --    Initial_Condition
       --    Initializes
       --    Refined_Depends
       --    Refined_Global

gcc/ada/snames.ads-tmpl

@@ -509,6 +509,7 @@ package Snames is
    Name_Import_Valued_Procedure        : constant Name_Id := N + $; -- GNAT
    Name_Independent                    : constant Name_Id := N + $; -- Ada 12
    Name_Independent_Components         : constant Name_Id := N + $; -- Ada 12
+   Name_Initial_Condition              : constant Name_Id := N + $; -- GNAT
    Name_Initializes                    : constant Name_Id := N + $; -- GNAT
    Name_Inline                         : constant Name_Id := N + $;
    Name_Inline_Always                  : constant Name_Id := N + $; -- GNAT
@@ -1829,6 +1830,7 @@ package Snames is
       Pragma_Import_Valued_Procedure,
       Pragma_Independent,
       Pragma_Independent_Components,
+      Pragma_Initial_Condition,
       Pragma_Initializes,
       Pragma_Inline,
       Pragma_Inline_Always,