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.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@203551 138bc75d-0d04-0410-961f-82ee72b054a4

16 files changed, 544 insertions, 67 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index adb5e6d79e2..acb4f5881ab 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,48 @@
+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.
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index b9f1a56af6c..0d9d28c556d 100644
--- a/gcc/ada/aspects.adb
+++ b/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,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 2325d970383..877a1af3b79 100644
--- a/gcc/ada/aspects.ads
+++ b/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,
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 176a81fbc5d..8636d8511cd 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -6300,18 +6300,19 @@ package body Einfo is
 
    function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
       Is_CDG  : constant Boolean :=
-                  Id = Pragma_Abstract_State  or else
-                  Id = Pragma_Depends         or else
-                  Id = Pragma_Global          or else
-                  Id = Pragma_Initializes     or else
-                  Id = Pragma_Refined_Depends or else
-                  Id = Pragma_Refined_Global  or else
+                  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
                   Id = Pragma_Refined_State;
       Is_CTC : constant Boolean :=
-                  Id = Pragma_Contract_Cases  or else
+                  Id = Pragma_Contract_Cases    or else
                   Id = Pragma_Test_Case;
       Is_PPC : constant Boolean :=
-                  Id = Pragma_Precondition    or else
+                  Id = Pragma_Precondition      or else
                   Id = Pragma_Postcondition;
 
       In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 8bc4b79007f..0526d4406e8 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -7442,6 +7442,8 @@ package Einfo is
    --    Contract_Cases
    --    Depends
    --    Global
+   --    Initial_Condition
+   --    Initializes
    --    Precondition
    --    Postcondition
    --    Refined_Depends
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index fdaf213ff86..1b242cc46e9 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/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
+         --  Generate RACW subprogram bodies
 
+         if Has_RACW (Id) then
             Decls := Private_Declarations (Spec);
 
             if No (Decls) then
@@ -4072,11 +4085,19 @@ package body Exp_Ch7 is
             Analyze_List (Decls);
          end if;
 
+         --  Generate task activation call as last step of elaboration
+
          if Present (Activation_Chain_Entity (N)) then
+            Build_Task_Activation_Call (N);
+         end if;
 
-            --  Generate task activation call as last step of elaboration
+         --  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).
 
-            Build_Task_Activation_Call (N);
+         if Present (Get_Pragma (Id, Pragma_Initial_Condition)) then
+            Expand_Pragma_Initial_Condition (N);
          end if;
 
          Pop_Scope;
@@ -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 --
    -----------------------------
diff --git a/gcc/ada/exp_pakd.adb b/gcc/ada/exp_pakd.adb
index a6a1f0dc70b..45aafadefee 100644
--- a/gcc/ada/exp_pakd.adb
+++ b/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;
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index a965e12972c..53f4fe4652d 100644
--- a/gcc/ada/par-prag.adb
+++ b/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                         |
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index aacb84c729e..6744484da38 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/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        |
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index e81e61f215a..4440910ab69 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/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
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 95ac60088ad..4734581b0e5 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -911,9 +911,9 @@ package body Sem_Prag is
             --  as input. OUT parameters are valid inputs only when their type
             --  is unconstrained or tagged as their discriminants, array bouns
             --  or tags can be read. In general, states and variables are
-            --  considered to have mode IN OUT unless they are moded by pragma
-            --  [Refined_]Global. In that case, the item must appear in an
-            --  input global list.
+            --  considered to have mode IN OUT unless they are classified by
+            --  pragma [Refined_]Global. In that case, the item must appear in
+            --  an input global list.
 
             if (Ekind (Item_Id) = E_Out_Parameter
                  and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
@@ -1964,6 +1964,194 @@ package body Sem_Prag is
       end if;
    end Analyze_Global_In_Decl_Part;
 
+   --------------------------------------------
+   -- Analyze_Initial_Condition_In_Decl_Part --
+   --------------------------------------------
+
+   procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
+      Pack_Id   : constant Entity_Id := Defining_Entity (Parent (Parent (N)));
+      Prag_Init : constant Node_Id   :=
+                    Get_Pragma (Pack_Id, Pragma_Initializes);
+      --  The related pragma Initializes
+
+      Vars : Elist_Id := No_Elist;
+      --  A list of all variables declared in pragma Initializes
+
+      procedure Collect_Variables;
+      --  Inspect the initialization list of pragma Initializes and collect the
+      --  entities of all variables declared within the related package.
+
+      function Match_Variable (N : Node_Id) return Traverse_Result;
+      --  Determine whether arbitrary node N denotes a variable declared in the
+      --  visible declarations of the related package.
+
+      procedure Report_Unused_Variables;
+      --  Emit errors for all variables found in list Vars
+
+      -----------------------
+      -- Collect_Variables --
+      -----------------------
+
+      procedure Collect_Variables is
+         procedure Collect_Variable (Item : Node_Id);
+         --  Determine whether Item denotes a variable that appears in the
+         --  related package and if it does, add it to list Vars.
+
+         ----------------------
+         -- Collect_Variable --
+         ----------------------
+
+         procedure Collect_Variable (Item : Node_Id) is
+            Item_Id : Entity_Id;
+
+         begin
+            if Is_Entity_Name (Item) and then Present (Entity (Item)) then
+               Item_Id := Entity (Item);
+
+               --  The item is a variable declared in the related package
+
+               if Ekind (Item_Id) = E_Variable
+                 and then Scope (Item_Id) = Pack_Id
+               then
+                  Add_Item (Item_Id, Vars);
+               end if;
+            end if;
+         end Collect_Variable;
+
+         --  Local variables
+
+         Inits : constant Node_Id :=
+                   Get_Pragma_Arg
+                     (First (Pragma_Argument_Associations (Prag_Init)));
+         Init  : Node_Id;
+
+      --  Start of processing for Collect_Variables
+
+      begin
+         --  Multiple initialization items appear as an aggregate
+
+         if Nkind (Inits) = N_Aggregate
+           and then Present (Expressions (Inits))
+         then
+            Init := First (Expressions (Inits));
+            while Present (Init) loop
+               Collect_Variable (Init);
+
+               Next (Init);
+            end loop;
+
+         --  Single initialization item
+
+         else
+            Collect_Variable (Inits);
+         end if;
+      end Collect_Variables;
+
+      --------------------
+      -- Match_Variable --
+      --------------------
+
+      function Match_Variable (N : Node_Id) return Traverse_Result is
+         Var_Id : Entity_Id;
+
+      begin
+         --  Find a variable declared within the related package and try to
+         --  remove it from the list of collected variables found in pragma
+         --  Initializes.
+
+         if Is_Entity_Name (N)
+           and then Present (Entity (N))
+         then
+            Var_Id := Entity (N);
+
+            if Ekind (Var_Id) = E_Variable
+              and then Scope (Var_Id) = Pack_Id
+            then
+               Remove (Vars, Var_Id);
+            end if;
+         end if;
+
+         return OK;
+      end Match_Variable;
+
+      procedure Match_Variables is new Traverse_Proc (Match_Variable);
+
+      -----------------------------
+      -- Report_Unused_Variables --
+      -----------------------------
+
+      procedure Report_Unused_Variables is
+         Posted   : Boolean := False;
+         Var_Elmt : Elmt_Id;
+         Var_Id   : Entity_Id;
+
+      begin
+         if Present (Vars) then
+            Var_Elmt := First_Elmt (Vars);
+            while Present (Var_Elmt) loop
+               Var_Id := Node (Var_Elmt);
+
+               if not Posted then
+                  Posted := True;
+                  Error_Msg_Name_1 := Name_Initial_Condition;
+                  Error_Msg_N
+                    ("expression of % must mention the following variables",
+                     N);
+               end if;
+
+               Error_Msg_Sloc := Sloc (Var_Id);
+               Error_Msg_NE ("\  & declared #", N, Var_Id);
+
+               Next_Elmt (Var_Elmt);
+            end loop;
+         end if;
+      end Report_Unused_Variables;
+
+      Expr   : constant Node_Id :=
+                 Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+      Errors : constant Nat     := Serious_Errors_Detected;
+
+   --  Start of processing for Analyze_Initial_Condition_In_Decl_Part
+
+   begin
+      Set_Analyzed (N);
+
+      --  Pragma Initial_Condition depends on the names enumerated in pragma
+      --  Initializes. Without those, the analysis cannot take place.
+
+      if No (Prag_Init) then
+         Error_Msg_Name_1 := Name_Initial_Condition;
+         Error_Msg_Name_2 := Name_Initializes;
+
+         Error_Msg_N ("% requires the presence of aspect or pragma %", N);
+         return;
+      end if;
+
+      --  The expression is preanalyzed because it has not been moved to its
+      --  final place yet. A direct analysis may generate sife effects and this
+      --  is not desired at this point.
+
+      Preanalyze_And_Resolve (Expr, Standard_Boolean);
+
+      --  Perform variable matching only when the expression is legal
+
+      if Serious_Errors_Detected = Errors then
+         Collect_Variables;
+
+         --  Verify that all variables mentioned in pragma Initializes are used
+         --  in the expression of pragma Initial_Condition.
+
+         Match_Variables (Expr);
+      end if;
+
+      --  Emit errors for all variables that should participate in the
+      --  expression of pragma Initial_Condition.
+
+      if Serious_Errors_Detected = Errors then
+         Report_Unused_Variables;
+      end if;
+   end Analyze_Initial_Condition_In_Decl_Part;
+
    --------------------------------------
    -- Analyze_Initializes_In_Decl_Part --
    --------------------------------------
@@ -2451,10 +2639,10 @@ package body Sem_Prag is
       --  UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part
       --  should be set when Comp comes from a record variant.
 
-      procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id);
-      --  Subsidiary routine to the analysis of pragmas Abstract_State and
-      --  Initializes. Determine whether pragma Abstract_State denoted by
-      --  States is defined earlier than pragma Initializes denoted by Inits.
+      procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id);
+      --  Subsidiary routine to the analysis of pragmas Abstract_State,
+      --  Initial_Condition and Initializes. Determine whether pragma First
+      --  appears before pragma Second. If this is not the case, emit an error.
 
       procedure Check_Duplicate_Pragma (E : Entity_Id);
       --  Check if a rep item of the same name as the current pragma is already
@@ -3433,7 +3621,7 @@ package body Sem_Prag is
       -- Check_Declaration_Order --
       -----------------------------
 
-      procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id) is
+      procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id) is
          procedure Check_Aspect_Specification_Order;
          --  Inspect the aspect specifications of the context to determine the
          --  proper order.
@@ -3443,33 +3631,34 @@ package body Sem_Prag is
          --------------------------------------
 
          procedure Check_Aspect_Specification_Order is
-            Asp_I : constant Node_Id := Corresponding_Aspect (Inits);
-            Asp_S : constant Node_Id := Corresponding_Aspect (States);
-            Asp   : Node_Id;
-
-            States_Seen : Boolean := False;
+            Asp_First  : constant Node_Id := Corresponding_Aspect (First);
+            Asp_Second : constant Node_Id := Corresponding_Aspect (Second);
+            Asp        : Node_Id;
 
          begin
             --  Both aspects must be part of the same aspect specification list
 
-            pragma Assert (List_Containing (Asp_I) = List_Containing (Asp_S));
+            pragma Assert
+              (List_Containing (Asp_First) = List_Containing (Asp_Second));
 
-            Asp := First (List_Containing (Asp_I));
+            --  Try to reach Second starting from First in a left to right
+            --  traversal of the aspect specifications.
+
+            Asp := Next (Asp_First);
             while Present (Asp) loop
-               if Get_Aspect_Id (Asp) = Aspect_Abstract_State then
-                  States_Seen := True;
 
-               elsif Get_Aspect_Id (Asp) = Aspect_Initializes then
-                  if not States_Seen then
-                     Error_Msg_N
-                       ("aspect % must come before aspect %", States);
-                  end if;
+               --  The order is ok, First is followed by Second
 
-                  exit;
+               if Asp = Asp_Second then
+                  return;
                end if;
 
                Next (Asp);
             end loop;
+
+            --  If we get here, then the aspects are out of order
+
+            Error_Msg_N ("aspect % cannot come after aspect %", First);
          end Check_Aspect_Specification_Order;
 
          --  Local variables
@@ -3481,44 +3670,41 @@ package body Sem_Prag is
       begin
          --  Cannot check the order if one of the pragmas is missing
 
-         if No (States) or else No (Inits) then
+         if No (First) or else No (Second) then
             return;
          end if;
 
          --  Set up the error names in case the order is incorrect
 
-         Error_Msg_Name_1 := Name_Abstract_State;
-         Error_Msg_Name_2 := Name_Initializes;
+         Error_Msg_Name_1 := Pragma_Name (First);
+         Error_Msg_Name_2 := Pragma_Name (Second);
 
-         if From_Aspect_Specification (States) then
+         if From_Aspect_Specification (First) then
 
             --  Both pragmas are actually aspects, check their declaration
             --  order in the associated aspect specification list. Otherwise
-            --  States is an aspect and Inits a source pragma.
+            --  First is an aspect and Second a source pragma.
 
-            if From_Aspect_Specification (Inits) then
+            if From_Aspect_Specification (Second) then
                Check_Aspect_Specification_Order;
             end if;
 
          --  Abstract_States is a source pragma
 
          else
-            if From_Aspect_Specification (Inits) then
-               Error_Msg_N ("pragma % cannot come after aspect %", States);
+            if From_Aspect_Specification (Second) then
+               Error_Msg_N ("pragma % cannot come after aspect %", First);
 
-            --  Both pragmas are source constructs. Try to reach States from
-            --  Inits by traversing the declarations backwards.
+            --  Both pragmas are source constructs. Try to reach First from
+            --  Second by traversing the declarations backwards.
 
             else
-               Stmt := Prev (Inits);
+               Stmt := Prev (Second);
                while Present (Stmt) loop
 
-                  --  The order is ok, Abstract_States is first followed by
-                  --  Initializes.
+                  --  The order is ok, First is followed by Second
 
-                  if Nkind (Stmt) = N_Pragma
-                    and then Pragma_Name (Stmt) = Name_Abstract_State
-                  then
+                  if Stmt = First then
                      return;
                   end if;
 
@@ -3527,7 +3713,7 @@ package body Sem_Prag is
 
                --  If we get here, then the pragmas are out of order
 
-               Error_Msg_N ("pragma % cannot come after pragma %", States);
+               Error_Msg_N ("pragma % cannot come after pragma %", First);
             end if;
          end if;
       end Check_Declaration_Order;
@@ -9318,8 +9504,8 @@ package body Sem_Prag is
             --  Initializes.
 
             Check_Declaration_Order
-              (States => N,
-               Inits  => Get_Pragma (Pack_Id, Pragma_Initializes));
+              (First  => N,
+               Second => Get_Pragma (Pack_Id, Pragma_Initializes));
 
             State := Expression (Arg1);
 
@@ -9732,6 +9918,7 @@ package body Sem_Prag is
          --                        Assume               |
          --                        Contract_Cases       |
          --                        Debug                |
+         --                        Initial_Condition    |
          --                        Loop_Invariant       |
          --                        Loop_Variant         |
          --                        Postcondition        |
@@ -13380,6 +13567,80 @@ package body Sem_Prag is
             end if;
          end Independent_Components;
 
+         -----------------------
+         -- Initial_Condition --
+         -----------------------
+
+         --  pragma Initial_Condition (boolean_EXPRESSION);
+
+         when Pragma_Initial_Condition => Initial_Condition : declare
+            Context : constant Node_Id := Parent (Parent (N));
+            Pack_Id : Entity_Id;
+            Stmt    : Node_Id;
+
+         begin
+            GNAT_Pragma;
+            S14_Pragma;
+            Check_Arg_Count (1);
+
+            --  Ensure the proper placement of the pragma. Initial_Condition
+            --  must be associated with a package declaration.
+
+            if not Nkind_In (Context, N_Generic_Package_Declaration,
+                                      N_Package_Declaration)
+            then
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Stmt := Prev (N);
+            while Present (Stmt) loop
+
+               --  Skip prior pragmas, but check for duplicates
+
+               if Nkind (Stmt) = N_Pragma then
+                  if Pragma_Name (Stmt) = Pname then
+                     Error_Msg_Name_1 := Pname;
+                     Error_Msg_Sloc   := Sloc (Stmt);
+                     Error_Msg_N ("pragma % duplicates pragma declared #", N);
+                  end if;
+
+               --  Skip internally generated code
+
+               elsif not Comes_From_Source (Stmt) then
+                  null;
+
+               --  The pragma does not apply to a legal construct, issue an
+               --  error and stop the analysis.
+
+               else
+                  Pragma_Misplaced;
+                  return;
+               end if;
+
+               Stmt := Prev (Stmt);
+            end loop;
+
+            --  The pragma must be analyzed at the end of the visible
+            --  declarations of the related package. Save the pragma for later
+            --  (see Analyze_Initial_Condition_In_Decl_Part) by adding it to
+            --  the contract of the package.
+
+            Pack_Id := Defining_Entity (Context);
+            Add_Contract_Item (N, Pack_Id);
+
+            --  Verify the declaration order of pragma Initial_Condition with
+            --  respect to pragmas Abstract_State and Initializes.
+
+            Check_Declaration_Order
+              (First  => Get_Pragma (Pack_Id, Pragma_Abstract_State),
+               Second => N);
+
+            Check_Declaration_Order
+              (First  => Get_Pragma (Pack_Id, Pragma_Initializes),
+               Second => N);
+         end Initial_Condition;
+
          ------------------------
          -- Initialize_Scalars --
          ------------------------
@@ -13461,8 +13722,8 @@ package body Sem_Prag is
                elsif not Comes_From_Source (Stmt) then
                   null;
 
-                  --  The pragma does not apply to a legal construct, issue an
-                  --  error and stop the analysis.
+               --  The pragma does not apply to a legal construct, issue an
+               --  error and stop the analysis.
 
                else
                   Pragma_Misplaced;
@@ -13484,8 +13745,8 @@ package body Sem_Prag is
             --  Initializes.
 
             Check_Declaration_Order
-              (States => Get_Pragma (Pack_Id, Pragma_Abstract_State),
-               Inits  => N);
+              (First  => Get_Pragma (Pack_Id, Pragma_Abstract_State),
+               Second => N);
          end Initializes;
 
          ------------
@@ -16979,8 +17240,8 @@ package body Sem_Prag is
                elsif not Comes_From_Source (Stmt) then
                   null;
 
-                  --  The pragma does not apply to a legal construct, issue an
-                  --  error and stop the analysis.
+               --  The pragma does not apply to a legal construct, issue an
+               --  error and stop the analysis.
 
                else
                   Pragma_Misplaced;
@@ -22429,6 +22690,7 @@ package body Sem_Prag is
       Pragma_Import_Valued_Procedure        =>  0,
       Pragma_Independent                    =>  0,
       Pragma_Independent_Components         =>  0,
+      Pragma_Initial_Condition              => -1,
       Pragma_Initialize_Scalars             => -1,
       Pragma_Initializes                    => -1,
       Pragma_Inline                         =>  0,
@@ -22822,6 +23084,7 @@ package body Sem_Prag is
             Name_Assume               |
             Name_Contract_Cases       |
             Name_Debug                |
+            Name_Initial_Condition    |
             Name_Invariant            |
             Name_uInvariant           |
             Name_Loop_Invariant       |
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 3f7b3066059..9f88638e921 100644
--- a/gcc/ada/sem_prag.ads
+++ b/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
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 83decce62f0..add58bf5aeb 100644
--- a/gcc/ada/sem_util.adb
+++ b/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);
 
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 8eaa58014c8..bf9987cb7b8 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -50,6 +50,7 @@ package Sem_Util is
    --    Contract_Cases
    --    Depends
    --    Global
+   --    Initial_Condition
    --    Initializes
    --    Postcondition
    --    Precondition
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index ebe51f29d66..eecc2d49960 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -7198,6 +7198,7 @@ package Sinfo is
       --    Abstract_States
       --    Depends
       --    Global
+      --    Initial_Condition
       --    Initializes
       --    Refined_Depends
       --    Refined_Global
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 74702f819e9..577e9ecadf0 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/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,