[multiple changes]

2014-02-06  Robert Dewar  <dewar@adacore.com>

	* sprint.adb: Minor reformatting.

2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch4.adb (Process_Transient_Object): Add local variable
	Temp_Ins. When the transient object is initialized by an
	aggregate, the hook must capture the object after the last
	component assignment takes place.
	* exp_ch7.adb (Detect_Subprogram_Call): Expose the subprogram to
	routine Is_Subprogram_Call.
	(Is_Subprogram_Call): Inspect an
	aggregate that has been heavily expanded for subprogram calls.
	(Process_Transient_Objects): Add local variables Expr, Ptr_Id
	and Temp_Ins.  Remove the nested declare block and adjust the
	indentation. When the transient object is initialized by an
	aggregate, the hook must capture the object after the last
	component assignment takes place.

2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Global_Item): Detect illegal uses of
	external states with enabled properties that do not match the
	global mode.
	(Property_Error): New routine.
	* sem_res.adb (Property_Error): New routine.
	(Resolve_Actuals): Detect illegal uses of external variables with
	enabled properties in procedure calls that do not match the mode of
	the corresponding formal parameter.

2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_util.adb (Has_Enabled_Property): Rename
	formal parameter Prop_Nam to Property. Update the comment on usage
	and all occurrences in the body. Add local variable Prop_Nam. When
	inspecting a property with an expression, the property name
	appears as the first choice of the component association.

From-SVN: r207534

7 files changed, 281 insertions, 77 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8417198..0ee4e1e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,42 @@
+2014-02-06  Robert Dewar  <dewar@adacore.com>
+
+	* sprint.adb: Minor reformatting.
+
+2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch4.adb (Process_Transient_Object): Add local variable
+	Temp_Ins. When the transient object is initialized by an
+	aggregate, the hook must capture the object after the last
+	component assignment takes place.
+	* exp_ch7.adb (Detect_Subprogram_Call): Expose the subprogram to
+	routine Is_Subprogram_Call.
+	(Is_Subprogram_Call): Inspect an
+	aggregate that has been heavily expanded for subprogram calls.
+	(Process_Transient_Objects): Add local variables Expr, Ptr_Id
+	and Temp_Ins.  Remove the nested declare block and adjust the
+	indentation. When the transient object is initialized by an
+	aggregate, the hook must capture the object after the last
+	component assignment takes place.
+
+2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Global_Item): Detect illegal uses of
+	external states with enabled properties that do not match the
+	global mode.
+	(Property_Error): New routine.
+	* sem_res.adb (Property_Error): New routine.
+	(Resolve_Actuals): Detect illegal uses of external variables with
+	enabled properties in procedure calls that do not match the mode of
+	the corresponding formal parameter.
+
+2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_util.adb (Has_Enabled_Property): Rename
+	formal parameter Prop_Nam to Property. Update the comment on usage
+	and all occurrences in the body. Add local variable Prop_Nam. When
+	inspecting a property with an expression, the property name
+	appears as the first choice of the component association.
+
 2014-02-04  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch5.adb, einfo.ads, freeze.adb, sem_ch8.adb: Minor reformatting.
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 7232ec8..d0ee791 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -12386,6 +12386,7 @@ package body Exp_Ch4 is
       Fin_Stmts : List_Id;
       Ptr_Id    : Entity_Id;
       Temp_Id   : Entity_Id;
+      Temp_Ins  : Node_Id;
 
    --  Start of processing for Process_Transient_Object
 
@@ -12463,7 +12464,22 @@ package body Exp_Ch4 is
       --      <or>
       --    Temp := Obj_Id'Unrestricted_Access;
 
-      Insert_After_And_Analyze (Decl,
+      --  When the transient object is initialized by an aggregate, the hook
+      --  must capture the object after the last component assignment takes
+      --  place. Only then is the object fully initialized.
+
+      if Ekind (Obj_Id) = E_Variable
+        and then Present (Last_Aggregate_Assignment (Obj_Id))
+      then
+         Temp_Ins := Last_Aggregate_Assignment (Obj_Id);
+
+      --  Otherwise the hook seizes the related object immediately
+
+      else
+         Temp_Ins := Decl;
+      end if;
+
+      Insert_After_And_Analyze (Temp_Ins,
         Make_Assignment_Statement (Loc,
           Name       => New_Reference_To (Temp_Id, Loc),
           Expression => Expr));
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index ddf6d7e..5e90723 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -2454,11 +2454,22 @@ package body Exp_Ch7 is
              Expression => Make_Integer_Literal (Loc, Counter_Val));
 
          --  Insert the counter after all initialization has been done. The
-         --  place of insertion depends on the context. When dealing with a
-         --  controlled function, the counter is inserted directly after the
-         --  declaration because such objects lack init calls.
+         --  place of insertion depends on the context. If an object is being
+         --  initialized via an aggregate, then the counter must be inserted
+         --  after the last aggregate assignment.
 
-         Find_Last_Init (Decl, Obj_Typ, Count_Ins, Body_Ins);
+         if Ekind (Obj_Id) = E_Variable
+           and then Present (Last_Aggregate_Assignment (Obj_Id))
+         then
+            Count_Ins := Last_Aggregate_Assignment (Obj_Id);
+            Body_Ins  := Empty;
+
+         --  In all other cases the counter is inserted after the last call to
+         --  either [Deep_]Initialize or the type specific init proc.
+
+         else
+            Find_Last_Init (Decl, Obj_Typ, Count_Ins, Body_Ins);
+         end if;
 
          Insert_After (Count_Ins, Inc_Decl);
          Analyze (Inc_Decl);
@@ -4419,17 +4430,25 @@ package body Exp_Ch7 is
          function Is_Subprogram_Call (N : Node_Id) return Traverse_Result;
          --  Determine whether an arbitrary node denotes a subprogram call
 
+         procedure Detect_Subprogram_Call is
+           new Traverse_Proc (Is_Subprogram_Call);
+
          ------------------------
          -- Is_Subprogram_Call --
          ------------------------
 
          function Is_Subprogram_Call (N : Node_Id) return Traverse_Result is
          begin
-            --  A regular procedure or function call
+            --  Aggregates are usually rewritten into component by component
+            --  assignments and replaced by a reference to a temporary in the
+            --  original tree. Peek in the aggregate to detect function calls.
 
-            if Nkind (N) in N_Subprogram_Call then
-               Must_Hook := True;
-               return Abandon;
+            if Nkind (N) = N_Identifier
+              and then Nkind_In (Original_Node (N), N_Aggregate,
+                                                    N_Extension_Aggregate)
+            then
+               Detect_Subprogram_Call (Original_Node (N));
+               return OK;
 
             --  Detect a call to a function that returns on the secondary stack
 
@@ -4439,6 +4458,12 @@ package body Exp_Ch7 is
                Must_Hook := True;
                return Abandon;
 
+            --  A regular procedure or function call
+
+            elsif Nkind (N) in N_Subprogram_Call then
+               Must_Hook := True;
+               return Abandon;
+
             --  Keep searching
 
             else
@@ -4446,13 +4471,11 @@ package body Exp_Ch7 is
             end if;
          end Is_Subprogram_Call;
 
-         procedure Detect_Subprogram_Call is
-           new Traverse_Proc (Is_Subprogram_Call);
-
          --  Local variables
 
          Built     : Boolean := False;
          Desig_Typ : Entity_Id;
+         Expr      : Node_Id;
          Fin_Block : Node_Id;
          Fin_Data  : Finalization_Exception_Data;
          Fin_Decls : List_Id;
@@ -4462,9 +4485,11 @@ package body Exp_Ch7 is
          Obj_Ref   : Node_Id;
          Obj_Typ   : Entity_Id;
          Prev_Fin  : Node_Id := Empty;
+         Ptr_Id    : Entity_Id;
          Stmt      : Node_Id;
          Stmts     : List_Id;
          Temp_Id   : Entity_Id;
+         Temp_Ins  : Node_Id;
 
       --  Start of processing for Process_Transient_Objects
 
@@ -4505,11 +4530,10 @@ package body Exp_Ch7 is
                --  time around.
 
                if not Built then
+                  Built     := True;
                   Fin_Decls := New_List;
 
                   Build_Object_Declarations (Fin_Data, Fin_Decls, Loc);
-
-                  Built := True;
                end if;
 
                --  Transient variables associated with subprogram calls need
@@ -4524,69 +4548,80 @@ package body Exp_Ch7 is
                --  "hooks" are picked up by the finalization machinery.
 
                if Must_Hook then
-                  declare
-                     Expr   : Node_Id;
-                     Ptr_Id : Entity_Id;
 
-                  begin
-                     --  Step 1: Create an access type which provides a
-                     --  reference to the transient object. Generate:
+                  --  Step 1: Create an access type which provides a reference
+                  --  to the transient object. Generate:
 
-                     --    Ann : access [all] <Desig_Typ>;
+                  --    Ann : access [all] <Desig_Typ>;
 
-                     Ptr_Id := Make_Temporary (Loc, 'A');
+                  Ptr_Id := Make_Temporary (Loc, 'A');
 
-                     Insert_Action (Stmt,
-                       Make_Full_Type_Declaration (Loc,
-                         Defining_Identifier => Ptr_Id,
-                         Type_Definition     =>
-                           Make_Access_To_Object_Definition (Loc,
-                             All_Present        =>
-                               Ekind (Obj_Typ) = E_General_Access_Type,
-                             Subtype_Indication =>
-                               New_Reference_To (Desig_Typ, Loc))));
+                  Insert_Action (Stmt,
+                    Make_Full_Type_Declaration (Loc,
+                      Defining_Identifier => Ptr_Id,
+                      Type_Definition     =>
+                        Make_Access_To_Object_Definition (Loc,
+                          All_Present        =>
+                            Ekind (Obj_Typ) = E_General_Access_Type,
+                          Subtype_Indication =>
+                            New_Reference_To (Desig_Typ, Loc))));
 
-                     --  Step 2: Create a temporary which acts as a hook to
-                     --  the transient object. Generate:
+                  --  Step 2: Create a temporary which acts as a hook to the
+                  --  transient object. Generate:
 
-                     --    Temp : Ptr_Id := null;
+                  --    Temp : Ptr_Id := null;
 
-                     Temp_Id := Make_Temporary (Loc, 'T');
+                  Temp_Id := Make_Temporary (Loc, 'T');
 
-                     Insert_Action (Stmt,
-                       Make_Object_Declaration (Loc,
-                         Defining_Identifier => Temp_Id,
-                         Object_Definition   =>
-                           New_Reference_To (Ptr_Id, Loc)));
+                  Insert_Action (Stmt,
+                    Make_Object_Declaration (Loc,
+                      Defining_Identifier => Temp_Id,
+                      Object_Definition   =>
+                        New_Reference_To (Ptr_Id, Loc)));
 
-                     --  Mark the temporary as a transient hook. This signals
-                     --  the machinery in Build_Finalizer to recognize this
-                     --  special case.
+                  --  Mark the temporary as a transient hook. This signals the
+                  --  machinery in Build_Finalizer to recognize this special
+                  --  case.
 
-                     Set_Status_Flag_Or_Transient_Decl (Temp_Id, Stmt);
+                  Set_Status_Flag_Or_Transient_Decl (Temp_Id, Stmt);
 
-                     --  Step 3: Hook the transient object to the temporary
+                  --  Step 3: Hook the transient object to the temporary
 
-                     if Is_Access_Type (Obj_Typ) then
-                        Expr :=
-                          Convert_To (Ptr_Id, New_Reference_To (Obj_Id, Loc));
-                     else
-                        Expr :=
-                          Make_Attribute_Reference (Loc,
-                            Prefix         => New_Reference_To (Obj_Id, Loc),
-                            Attribute_Name => Name_Unrestricted_Access);
-                     end if;
+                  if Is_Access_Type (Obj_Typ) then
+                     Expr :=
+                       Convert_To (Ptr_Id, New_Reference_To (Obj_Id, Loc));
+                  else
+                     Expr :=
+                       Make_Attribute_Reference (Loc,
+                         Prefix         => New_Reference_To (Obj_Id, Loc),
+                         Attribute_Name => Name_Unrestricted_Access);
+                  end if;
 
-                     --  Generate:
-                     --    Temp := Ptr_Id (Obj_Id);
-                     --      <or>
-                     --    Temp := Obj_Id'Unrestricted_Access;
-
-                     Insert_After_And_Analyze (Stmt,
-                       Make_Assignment_Statement (Loc,
-                         Name       => New_Reference_To (Temp_Id, Loc),
-                         Expression => Expr));
-                  end;
+                  --  Generate:
+                  --    Temp := Ptr_Id (Obj_Id);
+                  --      <or>
+                  --    Temp := Obj_Id'Unrestricted_Access;
+
+                  --  When the transient object is initialized by an aggregate,
+                  --  the hook must capture the object after the last component
+                  --  assignment takes place. Only then is the object fully
+                  --  initialized.
+
+                  if Ekind (Obj_Id) = E_Variable
+                    and then Present (Last_Aggregate_Assignment (Obj_Id))
+                  then
+                     Temp_Ins := Last_Aggregate_Assignment (Obj_Id);
+
+                  --  Otherwise the hook seizes the related object immediately
+
+                  else
+                     Temp_Ins := Stmt;
+                  end if;
+
+                  Insert_After_And_Analyze (Temp_Ins,
+                    Make_Assignment_Statement (Loc,
+                      Name       => New_Reference_To (Temp_Id, Loc),
+                      Expression => Expr));
                end if;
 
                Stmts := New_List;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index dce9b8d..344bd27 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -1861,8 +1861,34 @@ package body Sem_Prag is
            (Item        : Node_Id;
             Global_Mode : Name_Id)
          is
+            procedure Property_Error
+              (State_Id : Entity_Id;
+               Prop_Nam : Name_Id);
+            --  Emit an error concerning state State_Id with enabled property
+            --  Async_Readers, Effective_Reads or Effective_Writes that is not
+            --  marked as In_Out or Output item.
+
+            --------------------
+            -- Property_Error --
+            --------------------
+
+            procedure Property_Error
+              (State_Id : Entity_Id;
+               Prop_Nam : Name_Id)
+            is
+            begin
+               Error_Msg_Name_1 := Prop_Nam;
+               Error_Msg_NE
+                 ("external state & with enabled property % must have mode "
+                  & "In_Out or Output (SPARK RM 7.1.2(7))", Item, State_Id);
+            end Property_Error;
+
+            --  Local variables
+
             Item_Id : Entity_Id;
 
+         --  Start of processing for Analyze_Global_Item
+
          begin
             --  Detect one of the following cases
 
@@ -1941,6 +1967,30 @@ package body Sem_Prag is
                         Ref      => Item);
                   end if;
 
+                  --  Detect an external state with an enabled property that
+                  --  does not match the mode of the state.
+
+                  if Global_Mode = Name_Input then
+                     if Async_Readers_Enabled (Item_Id) then
+                        Property_Error (Item_Id, Name_Async_Readers);
+
+                     elsif Effective_Reads_Enabled (Item_Id) then
+                        Property_Error (Item_Id, Name_Effective_Reads);
+
+                     elsif Effective_Writes_Enabled (Item_Id) then
+                        Property_Error (Item_Id, Name_Effective_Writes);
+                     end if;
+
+                  elsif Global_Mode = Name_Output
+                    and then Async_Writers_Enabled (Item_Id)
+                  then
+                     Error_Msg_Name_1 := Name_Async_Writers;
+                     Error_Msg_NE
+                       ("external state & with enabled property % must have "
+                        & "mode Input or In_Out (SPARK RM 7.1.2(7))",
+                        Item, Item_Id);
+                  end if;
+
                --  Variable related checks
 
                else
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 7cb47f2..c7a7e08 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3020,8 +3020,9 @@ package body Sem_Res is
    procedure Resolve_Actuals (N : Node_Id; Nam : Entity_Id) is
       Loc    : constant Source_Ptr := Sloc (N);
       A      : Node_Id;
-      F      : Entity_Id;
+      A_Id   : Entity_Id;
       A_Typ  : Entity_Id;
+      F      : Entity_Id;
       F_Typ  : Entity_Id;
       Prev   : Node_Id := Empty;
       Orig_A : Node_Id;
@@ -3043,6 +3044,14 @@ package body Sem_Res is
       --  an instance of the default expression. The insertion is always
       --  a named association.
 
+      procedure Property_Error
+        (Var      : Node_Id;
+         Var_Id   : Entity_Id;
+         Prop_Nam : Name_Id);
+      --  Emit an error concerning variable Var with entity Var_Id that has
+      --  enabled property Prop_Nam when it acts as an actual parameter in a
+      --  call and the corresponding formal parameter is of mode IN.
+
       function Same_Ancestor (T1, T2 : Entity_Id) return Boolean;
       --  Check whether T1 and T2, or their full views, are derived from a
       --  common type. Used to enforce the restrictions on array conversions
@@ -3374,6 +3383,23 @@ package body Sem_Res is
          Prev := Actval;
       end Insert_Default;
 
+      --------------------
+      -- Property_Error --
+      --------------------
+
+      procedure Property_Error
+        (Var      : Node_Id;
+         Var_Id   : Entity_Id;
+         Prop_Nam : Name_Id)
+      is
+      begin
+         Error_Msg_Name_1 := Prop_Nam;
+         Error_Msg_NE
+           ("external variable & with enabled property % cannot appear as "
+            & "actual in procedure call (SPARK RM 7.1.3(11))", Var, Var_Id);
+         Error_Msg_N ("\\corresponding formal parameter has mode In", Var);
+      end Property_Error;
+
       -------------------
       -- Same_Ancestor --
       -------------------
@@ -4288,6 +4314,41 @@ package body Sem_Res is
                     ("volatile object cannot act as actual in a call (SPARK "
                      & "RM 7.1.3(12))", A);
                end if;
+
+               --  Detect an external variable with an enabled property that
+               --  does not match the mode of the corresponding formal in a
+               --  procedure call.
+
+               --  why only procedure calls ???
+
+               if Ekind (Nam) = E_Procedure
+                 and then Is_Entity_Name (A)
+                 and then Present (Entity (A))
+                 and then Ekind (Entity (A)) = E_Variable
+               then
+                  A_Id := Entity (A);
+
+                  if Ekind (F) = E_In_Parameter then
+                     if Async_Readers_Enabled (A_Id) then
+                        Property_Error (A, A_Id, Name_Async_Readers);
+                     elsif Effective_Reads_Enabled (A_Id) then
+                        Property_Error (A, A_Id, Name_Effective_Reads);
+                     elsif Effective_Writes_Enabled (A_Id) then
+                        Property_Error (A, A_Id, Name_Effective_Writes);
+                     end if;
+
+                  elsif Ekind (F) = E_Out_Parameter
+                    and then Async_Writers_Enabled (A_Id)
+                  then
+                     Error_Msg_Name_1 := Name_Async_Writers;
+                     Error_Msg_NE
+                       ("external variable & with enabled property % cannot "
+                        & "appear as actual in procedure call (SPARK RM "
+                        & "7.1.3(11))", A, A_Id);
+                     Error_Msg_N
+                       ("\\corresponding formal parameter has mode Out", A);
+                  end if;
+               end if;
             end if;
 
             Next_Actual (A);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 12704a6..ba978e1 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -115,10 +115,10 @@ package body Sem_Util is
 
    function Has_Enabled_Property
      (State_Id : Node_Id;
-      Prop_Nam : Name_Id) return Boolean;
+      Property : Name_Id) return Boolean;
    --  Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
    --  Determine whether an abstract state denoted by its entity State_Id has
-   --  enabled property Prop_Name.
+   --  enabled property Property.
 
    function Has_Null_Extension (T : Entity_Id) return Boolean;
    --  T is a derived tagged type. Check whether the type extension is null.
@@ -7255,13 +7255,14 @@ package body Sem_Util is
 
    function Has_Enabled_Property
      (State_Id : Node_Id;
-      Prop_Nam : Name_Id) return Boolean
+      Property : Name_Id) return Boolean
    is
-      Decl    : constant Node_Id := Parent (State_Id);
-      Opt     : Node_Id;
-      Opt_Nam : Node_Id;
-      Prop    : Node_Id;
-      Props   : Node_Id;
+      Decl     : constant Node_Id := Parent (State_Id);
+      Opt      : Node_Id;
+      Opt_Nam  : Node_Id;
+      Prop     : Node_Id;
+      Prop_Nam : Node_Id;
+      Props    : Node_Id;
 
    begin
       --  The declaration of an external abstract state appears as an extension
@@ -7305,7 +7306,7 @@ package body Sem_Util is
 
                Prop := First (Expressions (Props));
                while Present (Prop) loop
-                  if Chars (Prop) = Prop_Nam then
+                  if Chars (Prop) = Property then
                      return True;
                   end if;
 
@@ -7316,7 +7317,9 @@ package body Sem_Util is
 
                Prop := First (Component_Associations (Props));
                while Present (Prop) loop
-                  if Chars (Prop) = Prop_Nam then
+                  Prop_Nam := First (Choices (Prop));
+
+                  if Chars (Prop_Nam) = Property then
                      return Is_True (Expr_Value (Expression (Prop)));
                   end if;
 
@@ -7326,7 +7329,7 @@ package body Sem_Util is
             --  Single property
 
             else
-               return Chars (Props) = Prop_Nam;
+               return Chars (Props) = Property;
             end if;
          end if;
 
diff --git a/gcc/ada/sprint.adb b/gcc/ada/sprint.adb
index e909474..49adb11 100644
--- a/gcc/ada/sprint.adb
+++ b/gcc/ada/sprint.adb
@@ -204,7 +204,7 @@ package body Sprint is
      (Node    : Node_Id;
       Default : Node_Id);
    --  Print the end label for a Handled_Sequence_Of_Statements in a body.
-   --  If there is not end label, use the defining identifier of the enclosing
+   --  If there is no end label, use the defining identifier of the enclosing
    --  construct. If the end label is present, treat it as a reference to the
    --  defining entity of the construct: this guarantees that it carries the
    --  proper sloc information for debugging purposes.