[multiple changes]

2017-10-09  Ed Schonberg  <schonberg@adacore.com>

	* exp_util.adb (Make_Predicate_Call): If the type of the expression to
	which the predicate check applies is tagged, convert the expression to
	that type. This is in most cases a no-op, but is relevant if the
	expression is clas-swide, because the predicate function being invoked
	is not a primitive of the type and cannot take a class-wide actual.

2017-10-09  Gary Dismukes  <dismukes@adacore.com>

	* exp_disp.adb: Minor reformatting.

2017-10-09  Arnaud Charlet  <charlet@adacore.com>

	* sem_warn.adb (Warn_On_Unreferenced_Entity): Fix typo.

2017-10-09  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb (Install_ABE_Check): Do not generate an ABE check for
	GNATprove.
	(Install_ABE_Failure): Do not generate an ABE failure for GNATprove.

2017-10-09  Bob Duff  <duff@adacore.com>

	* exp_ch6.adb: (Make_Build_In_Place_Call_In_Object_Declaration): Return
	immediately if the call has already been processed (by a previous call
	to Make_Build_In_Place_Call_In_Anonymous_Context).
	* sem_elab.adb: Minor typo fixes.

2017-10-09  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb (Replace_Type_Ref): In the expression for a dynamic
	predicate, do not replace an identifier that matches the type if the
	identifier is a selector in a selected component, because this
	indicates a reference to some homograph of the type itself, and  not to
	the current occurence in the predicate.

2017-10-09  Eric Botcazou  <ebotcazou@adacore.com>

	* repinfo.adb (List_Record_Layout): Tweak formatting.
	(Write_Val): Remove superfluous spaces in back-end layout mode.

2017-10-09  Piotr Trojanek  <trojanek@adacore.com>

	* sem_res.adb (Property_Error): Remove.
	(Resolve_Actuals): check for SPARK RM 7.1.3(10) rewritten to match the
	current wording of the rule.

2017-10-09  Justin Squirek  <squirek@adacore.com>

	* sem_ch3.adb (Analyze_Declarations): Add check for ghost packages
	before analyzing a given scope due to an expression function.
	(Uses_Unseen_Lib_Unit_Priv): Rename to Uses_Unseen_Priv.

From-SVN: r253563

10 files changed, 157 insertions, 96 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 85825d0..31b6dc0 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,57 @@
+2017-10-09  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_util.adb (Make_Predicate_Call): If the type of the expression to
+	which the predicate check applies is tagged, convert the expression to
+	that type. This is in most cases a no-op, but is relevant if the
+	expression is clas-swide, because the predicate function being invoked
+	is not a primitive of the type and cannot take a class-wide actual.
+
+2017-10-09  Gary Dismukes  <dismukes@adacore.com>
+
+	* exp_disp.adb: Minor reformatting.
+
+2017-10-09  Arnaud Charlet  <charlet@adacore.com>
+
+	* sem_warn.adb (Warn_On_Unreferenced_Entity): Fix typo.
+
+2017-10-09  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_elab.adb (Install_ABE_Check): Do not generate an ABE check for
+	GNATprove.
+	(Install_ABE_Failure): Do not generate an ABE failure for GNATprove.
+
+2017-10-09  Bob Duff  <duff@adacore.com>
+
+	* exp_ch6.adb: (Make_Build_In_Place_Call_In_Object_Declaration): Return
+	immediately if the call has already been processed (by a previous call
+	to Make_Build_In_Place_Call_In_Anonymous_Context).
+	* sem_elab.adb: Minor typo fixes.
+
+2017-10-09  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb (Replace_Type_Ref): In the expression for a dynamic
+	predicate, do not replace an identifier that matches the type if the
+	identifier is a selector in a selected component, because this
+	indicates a reference to some homograph of the type itself, and  not to
+	the current occurence in the predicate.
+
+2017-10-09  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* repinfo.adb (List_Record_Layout): Tweak formatting.
+	(Write_Val): Remove superfluous spaces in back-end layout mode.
+
+2017-10-09  Piotr Trojanek  <trojanek@adacore.com>
+
+	* sem_res.adb (Property_Error): Remove.
+	(Resolve_Actuals): check for SPARK RM 7.1.3(10) rewritten to match the
+	current wording of the rule.
+
+2017-10-09  Justin Squirek  <squirek@adacore.com>
+
+	* sem_ch3.adb (Analyze_Declarations): Add check for ghost packages
+	before analyzing a given scope due to an expression function.
+	(Uses_Unseen_Lib_Unit_Priv): Rename to Uses_Unseen_Priv.
+
 2017-10-09  Bob Duff  <duff@adacore.com>
 
 	* exp_ch6.adb (Make_Build_In_Place_Call_In_Object_Declaration): Use
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 5ac2717..c9ec0da 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -8248,12 +8248,20 @@ package body Exp_Ch6 is
       --  Caller_Known_Size (specific) tagged type, we treat it as
       --  indefinite, because the code for the Definite case below sets the
       --  initialization expression of the object to Empty, which would be
-      --  illegal Ada, and would cause gigi to mis-allocate X.
+      --  illegal Ada, and would cause gigi to misallocate X.
+
+   --  Start of processing for Make_Build_In_Place_Call_In_Object_Declaration
 
    begin
+      --  If the call has already been processed to add build-in-place actuals
+      --  then return.
+
+      if Is_Expanded_Build_In_Place_Call (Func_Call) then
+         return;
+      end if;
+
       --  Mark the call as processed as a build-in-place call
 
-      pragma Assert (not Is_Expanded_Build_In_Place_Call (Func_Call));
       Set_Is_Expanded_Build_In_Place_Call (Func_Call);
 
       --  Create an access type designating the function's result subtype.
diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb
index 63c996e..69d2965 100644
--- a/gcc/ada/exp_disp.adb
+++ b/gcc/ada/exp_disp.adb
@@ -738,10 +738,10 @@ package body Exp_Disp is
                            Set_Etype (N, Etype (F));
 
                         --  Conversely, if this is a controlling argument
-                        --  (in a dispatching call in the condition)
-                        --  that is a dereference, the source is an access to
-                        --  classwide type, so preserve the dispatching nature
-                        --  of the call in the rewritten condition.
+                        --  (in a dispatching call in the condition) that is a
+                        --  dereference, the source is an access-to-class-wide
+                        --  type, so preserve the dispatching nature of the
+                        --  call in the rewritten condition.
 
                         elsif Nkind (Parent (N)) = N_Explicit_Dereference
                           and then Is_Controlling_Actual (Parent (N))
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index def2263..6fa8d21 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -9305,10 +9305,22 @@ package body Exp_Util is
 
       --  Case of calling normal predicate function
 
-      Call :=
-        Make_Function_Call (Loc,
-          Name                   => New_Occurrence_Of (Func_Id, Loc),
-          Parameter_Associations => New_List (Relocate_Node (Expr)));
+      --  If the type is tagged, the expression may be class-wide, in which
+      --  case it has to be converted to its root type, given that the
+      --  generated predicate function is not dispatching.
+
+      if Is_Tagged_Type (Typ) then
+         Call :=
+           Make_Function_Call (Loc,
+             Name                   => New_Occurrence_Of (Func_Id, Loc),
+             Parameter_Associations =>
+               New_List (Convert_To (Typ, Relocate_Node (Expr))));
+      else
+         Call :=
+           Make_Function_Call (Loc,
+             Name                   => New_Occurrence_Of (Func_Id, Loc),
+             Parameter_Associations => New_List (Relocate_Node (Expr)));
+      end if;
 
       Restore_Ghost_Mode (Saved_GM);
 
diff --git a/gcc/ada/repinfo.adb b/gcc/ada/repinfo.adb
index 630d592..464b1b2 100644
--- a/gcc/ada/repinfo.adb
+++ b/gcc/ada/repinfo.adb
@@ -1051,14 +1051,13 @@ package body Repinfo is
                  and then List_Representation_Info = 3
                then
                   Spaces (Max_Spos_Length - 2);
-                  Write_Str ("bit offset");
+                  Write_Str ("bit offset ");
 
                   if Starting_Position /= Uint_0
                     or else Starting_First_Bit /= Uint_0
                   then
-                     Write_Char (' ');
                      UI_Write (Starting_Position * SSU + Starting_First_Bit);
-                     Write_Str (" +");
+                     Write_Str (" + ");
                   end if;
 
                   Write_Val (Bofs, Paren => True);
@@ -1686,27 +1685,18 @@ package body Repinfo is
             Write_Str ("??");
 
          else
-            if Back_End_Layout then
-               Write_Char (' ');
-
-               if Paren then
-                  Write_Char ('(');
-                  List_GCC_Expression (Val);
-                  Write_Char (')');
-               else
-                  List_GCC_Expression (Val);
-               end if;
-
-               Write_Char (' ');
+            if Paren then
+               Write_Char ('(');
+            end if;
 
+            if Back_End_Layout then
+               List_GCC_Expression (Val);
             else
-               if Paren then
-                  Write_Char ('(');
-                  Write_Name_Decoded (Chars (Get_Dynamic_SO_Entity (Val)));
-                  Write_Char (')');
-               else
-                  Write_Name_Decoded (Chars (Get_Dynamic_SO_Entity (Val)));
-               end if;
+               Write_Name_Decoded (Chars (Get_Dynamic_SO_Entity (Val)));
+            end if;
+
+            if Paren then
+               Write_Char (')');
             end if;
          end if;
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 79b22cd..5220e5d 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -4415,15 +4415,6 @@ package body Sem_Ch13 is
 
             if Present (Default_Element) then
                Analyze (Default_Element);
-
-               if Is_Entity_Name (Default_Element)
-                 and then not Covers (Entity (Default_Element), Ret_Type)
-                 and then False
-               then
-                  Illegal_Indexing
-                    ("wrong return type for indexing function");
-                  return;
-               end if;
             end if;
 
             --  For variable_indexing the return type must be a reference type
@@ -12670,10 +12661,18 @@ package body Sem_Ch13 is
 
                return Skip;
 
-            --  Otherwise do the replacement and we are done with this node
+            --  Otherwise do the replacement if this is not a qualified
+            --  reference to a homograph of the type itself. Note that the
+            --  current instance could not appear in such a context, e.g.
+            --  the prefix of a type conversion.
 
             else
-               Replace_Type_Reference (N);
+               if Nkind (Parent (N)) /= N_Selected_Component
+                 or else N /= Selector_Name (Parent (N))
+               then
+                  Replace_Type_Reference (N);
+               end if;
+
                return Skip;
             end if;
 
@@ -12682,7 +12681,7 @@ package body Sem_Ch13 is
 
          elsif Nkind (N) = N_Selected_Component then
 
-            --  If selector name is not our type, keeping going (we might still
+            --  If selector name is not our type, keep going (we might still
             --  have an occurrence of the type in the prefix).
 
             if Nkind (Selector_Name (N)) /= N_Identifier
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 769b7e9..7f54daa 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2233,9 +2233,11 @@ package body Sem_Ch3 is
       --  Utility to resolve the expressions of aspects at the end of a list of
       --  declarations.
 
-      function Uses_Unseen_Lib_Unit_Priv (Pkg : Entity_Id) return Boolean;
-      --  Check if an inner package has entities within it that rely on library
-      --  level private types where the full view has not been seen.
+      function Uses_Unseen_Priv (Pkg : Entity_Id) return Boolean;
+      --  Check if a nested package has entities within it that rely on library
+      --  level private types where the full view has not been seen for the
+      --  purposes of checking if it is acceptable to freeze an expression
+      --  function at the point of declaration.
 
       -----------------
       -- Adjust_Decl --
@@ -2540,11 +2542,11 @@ package body Sem_Ch3 is
          end loop;
       end Resolve_Aspects;
 
-      -------------------------------
-      -- Uses_Unseen_Lib_Unit_Priv --
-      -------------------------------
+      ----------------------
+      -- Uses_Unseen_Priv --
+      ----------------------
 
-      function Uses_Unseen_Lib_Unit_Priv (Pkg : Entity_Id) return Boolean is
+      function Uses_Unseen_Priv (Pkg : Entity_Id) return Boolean is
          Curr : Entity_Id;
 
       begin
@@ -2572,7 +2574,7 @@ package body Sem_Ch3 is
          end if;
 
          return False;
-      end Uses_Unseen_Lib_Unit_Priv;
+      end Uses_Unseen_Priv;
 
       --  Local variables
 
@@ -2753,8 +2755,9 @@ package body Sem_Ch3 is
 
          elsif not Analyzed (Next_Decl) and then Is_Body (Next_Decl)
            and then ((Nkind (Next_Decl) /= N_Subprogram_Body
-                      or else not Was_Expression_Function (Next_Decl))
-                     or else not Uses_Unseen_Lib_Unit_Priv (Current_Scope))
+                       or else not Was_Expression_Function (Next_Decl))
+                      or else (not Is_Ignored_Ghost_Entity (Current_Scope)
+                                and then not Uses_Unseen_Priv (Current_Scope)))
          then
             --  When a controlled type is frozen, the expander generates stream
             --  and controlled-type support routines. If the freeze is caused
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 47e9c99..e1ef3f8 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -4199,9 +4199,15 @@ package body Sem_Elab is
       Scop_Id : Entity_Id;
 
    begin
+      --  Nothing to do when compiling for GNATprove because raise statements
+      --  are not supported.
+
+      if GNATprove_Mode then
+         return;
+
       --  Nothing to do when the compilation will not produce an executable
 
-      if Serious_Errors_Detected > 0 then
+      elsif Serious_Errors_Detected > 0 then
          return;
 
       --  Nothing to do for a compilation unit because there is no executable
@@ -4325,9 +4331,15 @@ package body Sem_Elab is
    --  Start for processing for Install_ABE_Check
 
    begin
+      --  Nothing to do when compiling for GNATprove because raise statements
+      --  are not supported.
+
+      if GNATprove_Mode then
+         return;
+
       --  Nothing to do when the compilation will not produce an executable
 
-      if Serious_Errors_Detected > 0 then
+      elsif Serious_Errors_Detected > 0 then
          return;
 
       --  Nothing to do when the target is a protected subprogram because the
@@ -4381,9 +4393,15 @@ package body Sem_Elab is
       Scop_Id : Entity_Id;
 
    begin
+      --  Nothing to do when compiling for GNATprove because raise statements
+      --  are not supported.
+
+      if GNATprove_Mode then
+         return;
+
       --  Nothing to do when the compilation will not produce an executable
 
-      if Serious_Errors_Detected > 0 then
+      elsif Serious_Errors_Detected > 0 then
          return;
 
       --  Do not install an ABE check for a compilation unit because there is
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 0722e37..3ef0b7b 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3178,14 +3178,6 @@ 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
@@ -3634,23 +3626,6 @@ 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(10))", Var, Var_Id);
-         Error_Msg_N ("\\corresponding formal parameter has mode In", Var);
-      end Property_Error;
-
       -------------------
       -- Same_Ancestor --
       -------------------
@@ -4659,26 +4634,28 @@ package body Sem_Res is
                   Flag_Effectively_Volatile_Objects (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. Functions are not considered because they
-               --  cannot have effectively volatile formal parameters in the
-               --  first place.
+               --  An effectively volatile variable cannot act as an actual
+               --  parameter in a procedure call when the variable has enabled
+               --  property Effective_Reads and the corresponding formal is of
+               --  mode IN (SPARK RM 7.1.3(10)).
 
                if Ekind (Nam) = E_Procedure
                  and then Ekind (F) = E_In_Parameter
                  and then Is_Entity_Name (A)
-                 and then Present (Entity (A))
-                 and then Ekind (Entity (A)) = E_Variable
                then
                   A_Id := Entity (A);
 
-                  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);
+                  if Ekind (A_Id) = E_Variable
+                    and then Is_Effectively_Volatile (Etype (A_Id))
+                    and then Effective_Reads_Enabled (A_Id)
+                  then
+                     Error_Msg_NE
+                       ("effectively volatile variable & cannot appear as "
+                        & "actual in procedure call", A, A_Id);
+
+                     Error_Msg_Name_1 := Name_Effective_Reads;
+                     Error_Msg_N ("\\variable has enabled property %", A);
+                     Error_Msg_N ("\\corresponding formal has mode IN", A);
                   end if;
                end if;
             end if;
diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb
index aae5454..91f430a 100644
--- a/gcc/ada/sem_warn.adb
+++ b/gcc/ada/sem_warn.adb
@@ -4285,7 +4285,7 @@ package body Sem_Warn is
                   then
                      if not Has_Pragma_Unmodified_Check_Spec (E) then
                         Error_Msg_N -- CODEFIX
-                          ("?u?variable & is assigned but never read!", E);
+                          ("?m?variable & is assigned but never read!", E);
                      end if;
 
                      Set_Last_Assignment (E, Empty);