exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Use Component_Size of the innermost array instead of Esize of its component...

gcc/ada/

2017-12-15  Eric Botcazou  <ebotcazou@adacore.com>

	* exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Use Component_Size of
	the innermost array instead of Esize of its component type to exclude
	inappropriate array types, including packed array types.

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Input_Item): Allow concurrent types to appear
	within the input list of Initializes. Remove the uses of Input_OK.

2017-12-15  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch4.adb (Expand_N_In): Do not replace a membership test on a
	scalar type with a validity test when the membership appears in a
	predicate expression, to prevent a spurious error when predicate is
	specified static.
	* sem_ch13.adb (Build_Predicate_Functions): Add warning if a static
	predicate, after constant-folding, reduces to True and is this
	redundant.
	* par-ch4.adb: Typo fixes and minor reformattings.

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb (Ensure_Prior_Elaboration_Static): Mark the generated
	with clause as being implicit for an instantiation in order to
	circumvent an issue with 'W' and 'Z' line encodings in ALI files.

2017-12-15  Ed Schonberg  <schonberg@adacore.com>

	* sem_util.adb (Is_Potentially_Unevaluated): Detect further cases of
	misuse of 'Old that appear within an expression that is potentially
	unevaluated, when the prefix of the attribute does not statically
	designate an object (e.g. a function call).

2017-12-15  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Conformking_Types): Two incomplete types are conforming
	when one of them is used as a generic actual, but only within an
	instantiation.
	* einfo.ads: Clarify use of flag Used_As_Generic_Actual.

2017-12-15  Justin Squirek  <squirek@adacore.com>

	* sem_attr.adb (Resolve_Attribute): Modify check for aliased view on
	prefix to use the prefix's original node to avoid looking at expanded
	conversions for certain array types.

2017-12-15  Ed Schonberg  <schonberg@adacore.com>

	* sem_res.adb (Resolve_Membership_Op): Add warning on a membership
	operation on a scalar type for which there is a user-defined equality
	operator.

2017-12-15  Yannick Moy  <moy@adacore.com>

	* doc/gnat_rm/implementation_defined_pragmas.rst: Add Ghost assertion
	policy.

gcc/testsuite/

2017-12-15  Justin Squirek  <squirek@adacore.com>

	* gnat.dg/aliasing4.adb: New testcase.

2017-12-15  Ed Schonberg  <schonberg@adacore.com>

	* gnat.dg/incomplete6.adb, gnat.dg/incomplete6.ads: New testcase.

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* gnat.dg/initializes.ads, gnat.dg/initializes.adb: New testcase.

2017-12-15  Eric Botcazou  <ebotcazou@adacore.com>

	* gnat.dg/component_size.adb: New testcase.

From-SVN: r255695

15 files changed, 183 insertions, 56 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 528a5e6..fb3e7f4 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,62 @@
+2017-12-15  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Use Component_Size of
+	the innermost array instead of Esize of its component type to exclude
+	inappropriate array types, including packed array types.
+
+2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Input_Item): Allow concurrent types to appear
+	within the input list of Initializes. Remove the uses of Input_OK.
+
+2017-12-15  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch4.adb (Expand_N_In): Do not replace a membership test on a
+	scalar type with a validity test when the membership appears in a
+	predicate expression, to prevent a spurious error when predicate is
+	specified static.
+	* sem_ch13.adb (Build_Predicate_Functions): Add warning if a static
+	predicate, after constant-folding, reduces to True and is this
+	redundant.
+	* par-ch4.adb: Typo fixes and minor reformattings.
+
+2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_elab.adb (Ensure_Prior_Elaboration_Static): Mark the generated
+	with clause as being implicit for an instantiation in order to
+	circumvent an issue with 'W' and 'Z' line encodings in ALI files.
+
+2017-12-15  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_util.adb (Is_Potentially_Unevaluated): Detect further cases of
+	misuse of 'Old that appear within an expression that is potentially
+	unevaluated, when the prefix of the attribute does not statically
+	designate an object (e.g. a function call).
+
+2017-12-15  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Conformking_Types): Two incomplete types are conforming
+	when one of them is used as a generic actual, but only within an
+	instantiation.
+	* einfo.ads: Clarify use of flag Used_As_Generic_Actual.
+
+2017-12-15  Justin Squirek  <squirek@adacore.com>
+
+	* sem_attr.adb (Resolve_Attribute): Modify check for aliased view on
+	prefix to use the prefix's original node to avoid looking at expanded
+	conversions for certain array types.
+
+2017-12-15  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_res.adb (Resolve_Membership_Op): Add warning on a membership
+	operation on a scalar type for which there is a user-defined equality
+	operator.
+
+2017-12-15  Yannick Moy  <moy@adacore.com>
+
+	* doc/gnat_rm/implementation_defined_pragmas.rst: Add Ghost assertion
+	policy.
+
 2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_prag.adb (Analyze_Initialization_Item): Remove the specialized
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
index 1281758..d6ded29 100644
--- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -419,6 +419,7 @@ Syntax::
                         Assume               |
                         Contract_Cases       |
                         Debug                |
+                        Ghost                |
                         Invariant            |
                         Invariant'Class      |
                         Loop_Invariant       |
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index bb5b5e9..dd6652b 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -4583,7 +4583,9 @@ package Einfo is
 
 --    Used_As_Generic_Actual (Flag222)
 --       Defined in all entities, set if the entity is used as an argument to
---       a generic instantiation. Used to tune certain warning messages.
+--       a generic instantiation. Used to tune certain warning messages, and
+--       in checking type conformance within an instantiation that involves
+--       incomplete formal and actual types.
 
 --    Uses_Lock_Free (Flag188)
 --       Defined in protected type entities. Set to True when the Lock Free
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 8aca0d2..92c040e 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -4895,14 +4895,14 @@ package body Exp_Aggr is
 
       --    1. N consists of a single OTHERS choice, possibly recursively
 
-      --    2. The array type is not packed
+      --    2. The array type has no null ranges (the purpose of this is to
+      --       avoid a bogus warning for an out-of-range value).
 
       --    3. The array type has no atomic components
 
-      --    4. The array type has no null ranges (the purpose of this is to
-      --       avoid a bogus warning for an out-of-range value).
+      --    4. The component type is elementary
 
-      --    5. The component type is elementary
+      --    5. The component size is a multiple of Storage_Unit
 
       --    6. The component size is Storage_Unit or the value is of the form
       --       M * (1 + A**1 + A**2 + .. A**(K-1)) where A = 2**(Storage_Unit)
@@ -4918,6 +4918,7 @@ package body Exp_Aggr is
          Expr      : Node_Id := N;
          Low       : Node_Id;
          High      : Node_Id;
+         Csiz      : Uint;
          Remainder : Uint;
          Value     : Uint;
          Nunits    : Nat;
@@ -4933,14 +4934,6 @@ package body Exp_Aggr is
                return False;
             end if;
 
-            if Present (Packed_Array_Impl_Type (Ctyp)) then
-               return False;
-            end if;
-
-            if Has_Atomic_Components (Ctyp) then
-               return False;
-            end if;
-
             Index := First_Index (Ctyp);
             while Present (Index) loop
                Get_Index_Bounds (Index, Low, High);
@@ -4964,6 +4957,11 @@ package body Exp_Aggr is
                Expr := Expression (First (Component_Associations (Expr)));
             end loop;
 
+            if Has_Atomic_Components (Ctyp) then
+               return False;
+            end if;
+
+            Csiz := Component_Size (Ctyp);
             Ctyp := Component_Type (Ctyp);
 
             if Is_Atomic_Or_VFA (Ctyp) then
@@ -4978,20 +4976,19 @@ package body Exp_Aggr is
             return False;
          end if;
 
-         --  All elementary types are supported
+         --  Access types need to be dealt with specially
 
-         if not Is_Elementary_Type (Ctyp) then
-            return False;
-         end if;
+         if Is_Access_Type (Ctyp) then
 
-         --  However access types need to be dealt with specially
+            --  Component_Size is not set by Layout_Type if the component
+            --  type is an access type ???
 
-         if Is_Access_Type (Ctyp) then
+            Csiz := Esize (Ctyp);
 
             --  Fat pointers are rejected as they are not really elementary
             --  for the backend.
 
-            if Esize (Ctyp) /= System_Address_Size then
+            if Csiz /= System_Address_Size then
                return False;
             end if;
 
@@ -5002,15 +4999,26 @@ package body Exp_Aggr is
             if Nkind (Expr) /= N_Null and then not Is_Entity_Name (Expr) then
                return False;
             end if;
+
+         --  Scalar types are OK if their size is a multiple of Storage_Unit
+
+         elsif Is_Scalar_Type (Ctyp) then
+
+            if Csiz mod System_Storage_Unit /= 0 then
+               return False;
+            end if;
+
+         --  Composite types are rejected
+
+         else
+            return False;
          end if;
 
          --  The expression needs to be analyzed if True is returned
 
          Analyze_And_Resolve (Expr, Ctyp);
 
-         --  The back end uses the Esize as the precision of the type
-
-         Nunits := UI_To_Int (Esize (Ctyp)) / System_Storage_Unit;
+         Nunits := UI_To_Int (Csiz) / System_Storage_Unit;
 
          if Nunits = 1 then
             return True;
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index c3aa2d2..c5f64ae 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -6015,10 +6015,20 @@ package body Exp_Ch4 is
               --  have a test in the generic that makes sense with some types
               --  and not with other types.
 
-              and then not In_Instance
+              --  Similarly, do not rewrite membership as a validity check if
+              --  within the predicate function for the type.
+
             then
-               Substitute_Valid_Check;
-               goto Leave;
+               if In_Instance
+                 or else (Ekind (Current_Scope) = E_Function
+                           and then Is_Predicate_Function (Current_Scope))
+               then
+                  null;
+
+               else
+                  Substitute_Valid_Check;
+                  goto Leave;
+               end if;
             end if;
 
             --  If we have an explicit range, do a bit of optimization based on
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 0a2b151..0cec92a 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -21,7 +21,7 @@
 
 @copying
 @quotation
-GNAT Reference Manual , Nov 09, 2017
+GNAT Reference Manual , Dec 15, 2017
 
 AdaCore
 
@@ -1784,6 +1784,7 @@ ID_ASSERTION_KIND ::= Assertions           |
                       Assume               |
                       Contract_Cases       |
                       Debug                |
+                      Ghost                |
                       Invariant            |
                       Invariant'Class      |
                       Loop_Invariant       |
diff --git a/gcc/ada/par-ch4.adb b/gcc/ada/par-ch4.adb
index 4b5ef45..893011a 100644
--- a/gcc/ada/par-ch4.adb
+++ b/gcc/ada/par-ch4.adb
@@ -645,8 +645,8 @@ package body Ch4 is
          --      case of a name which can be extended in the normal manner.
          --      This case is handled by LP_State_Name or LP_State_Expr.
 
-         --      (Ada2020) : the expression can be a reduction_expression_
-         --      psarameter, i.e. a box or  < Simple_Expression >
+         --      (Ada 2020): the expression can be a reduction_expression_
+         --      parameter, i.e. a box or < Simple_Expression >.
 
          --      Note: if and case expressions (without an extra level of
          --      parentheses) are permitted in this context).
@@ -679,7 +679,7 @@ package body Ch4 is
          end if;
 
          --  Here we have an expression after all, which may be a reduction
-         --  expression with a binary operator
+         --  expression with a binary operator.
 
          if Token = Tok_Less then
             Scan; -- past <
@@ -2894,7 +2894,7 @@ package body Ch4 is
                Node1 := P_Name;
                return Node1;
 
-            --  Ada2020: reduction expression parameter
+            --  Ada 2020: reduction expression parameter
 
             when Tok_Less =>
                Scan; -- past <
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 91aa579..6db531a 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -11111,7 +11111,7 @@ package body Sem_Attr is
               and then not (Nkind (P) = N_Selected_Component
                              and then
                                Is_Overloadable (Entity (Selector_Name (P))))
-              and then not Is_Aliased_View (P)
+              and then not Is_Aliased_View (Original_Node (P))
               and then not In_Instance
               and then not In_Inlined_Body
               and then Comes_From_Source (N)
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index ebf1328..d2533b0 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -11919,6 +11919,12 @@ package body Sem_Ch13 is
       then
          return True;
 
+      elsif Is_Entity_Name (Expr)
+        and then Entity (Expr) = Standard_True
+      then
+         Error_Msg_N ("predicate is redundant (always True)?", Expr);
+         return True;
+
       --  That's an exhaustive list of tests, all other cases are not
       --  predicate-static, so we return False.
 
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 4791bf8..0a6c30a 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -4155,7 +4155,7 @@ package body Sem_Ch4 is
               and then Parent (Loop_Par) /= N
             then
                --  The parser cannot distinguish between a loop specification
-               --  and an iterator specification. If after pre-analysis the
+               --  and an iterator specification. If after preanalysis the
                --  proper form has been recognized, rewrite the expression to
                --  reflect the right kind. This is needed for proper ASIS
                --  navigation. If expansion is enabled, the transformation is
@@ -4378,7 +4378,7 @@ package body Sem_Ch4 is
               and then Parent (Loop_Par) /= N
             then
                --  The parser cannot distinguish between a loop specification
-               --  and an iterator specification. If after pre-analysis the
+               --  and an iterator specification. If after preanalysis the
                --  proper form has been recognized, rewrite the expression to
                --  reflect the right kind. This is needed for proper ASIS
                --  navigation. If expansion is enabled, the transformation is
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 1139a56..cb5b3e7 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -7666,10 +7666,12 @@ package body Sem_Ch6 is
          return True;
 
       --  In Ada 2012, incomplete types (including limited views) can appear
-      --  as actuals in instantiations.
+      --  as actuals in instantiations, where they are conformant to the
+      --  corresponding incomplete formal.
 
       elsif Is_Incomplete_Type (Type_1)
         and then Is_Incomplete_Type (Type_2)
+        and then In_Instance
         and then (Used_As_Generic_Actual (Type_1)
                    or else Used_As_Generic_Actual (Type_2))
       then
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 152def2..90746b4 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -3585,6 +3585,16 @@ package body Sem_Elab is
          Set_Implicit_With (Clause);
          Set_Library_Unit  (Clause, Unit_Cunit);
 
+         --  The following is a kludge to satisfy a GPRbuild requirement. In
+         --  general, internal with clauses should be encoded on a 'Z' line in
+         --  ALI files, but due to an old bug, they are encoded as source with
+         --  clauses on a 'W' line. As a result, these "semi-implicit" clauses
+         --  introduce spurious build dependencies in GPRbuild. The only way to
+         --  eliminate this effect is to mark the implicit clauses as generated
+         --  for an instantiation.
+
+         Set_Implicit_With_From_Instantiation (Clause);
+
          Append_To (Items, Clause);
       end if;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d98d9cf..6bf66ad 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2867,7 +2867,6 @@ package body Sem_Prag is
 
          procedure Analyze_Input_Item (Input : Node_Id) is
             Input_Id : Entity_Id;
-            Input_OK : Boolean := True;
 
          begin
             --  Null input list
@@ -2908,6 +2907,8 @@ package body Sem_Prag is
                                                  E_In_Parameter,
                                                  E_In_Out_Parameter,
                                                  E_Out_Parameter,
+                                                 E_Protected_Type,
+                                                 E_Task_Type,
                                                  E_Variable)
                   then
                      --  The input cannot denote states or objects declared
@@ -2933,11 +2934,11 @@ package body Sem_Prag is
                            null;
 
                         else
-                           Input_OK := False;
                            Error_Msg_Name_1 := Chars (Pack_Id);
                            SPARK_Msg_NE
                              ("input item & cannot denote a visible object or "
                               & "state of package %", Input, Input_Id);
+                           return;
                         end if;
                      end if;
 
@@ -2945,26 +2946,25 @@ package body Sem_Prag is
                      --  (SPARK RM 7.1.5(5)).
 
                      if Contains (Inputs_Seen, Input_Id) then
-                        Input_OK := False;
                         SPARK_Msg_N ("duplicate input item", Input);
+                        return;
                      end if;
 
-                     --  Input is legal, add it to the list of processed inputs
+                     --  At this point it is known that the input is legal. Add
+                     --  it to the list of processed inputs.
 
-                     if Input_OK then
-                        Append_New_Elmt (Input_Id, Inputs_Seen);
+                     Append_New_Elmt (Input_Id, Inputs_Seen);
 
-                        if Ekind (Input_Id) = E_Abstract_State then
-                           Append_New_Elmt (Input_Id, States_Seen);
-                        end if;
+                     if Ekind (Input_Id) = E_Abstract_State then
+                        Append_New_Elmt (Input_Id, States_Seen);
+                     end if;
 
-                        if Ekind_In (Input_Id, E_Abstract_State,
-                                               E_Constant,
-                                               E_Variable)
-                          and then Present (Encapsulating_State (Input_Id))
-                        then
-                           Append_New_Elmt (Input_Id, Constits_Seen);
-                        end if;
+                     if Ekind_In (Input_Id, E_Abstract_State,
+                                            E_Constant,
+                                            E_Variable)
+                       and then Present (Encapsulating_State (Input_Id))
+                     then
+                        Append_New_Elmt (Input_Id, Constits_Seen);
                      end if;
 
                   --  The input references something that is not a state or an
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 969b8bd..23a95a4 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -9086,6 +9086,21 @@ package body Sem_Res is
                end loop;
             end;
          end if;
+
+         --  RM 4.5.2 (28.1/3) specifies that for types other than records or
+         --  limited types, evaluation of a membership test uses the predefined
+         --  equality for the type. This may be confusing to users, and the
+         --  following warning appears useful for the most common case.
+
+         if Is_Scalar_Type (Ltyp)
+           and then Present (Get_User_Defined_Eq (Ltyp))
+         then
+            Error_Msg_NE
+              ("membership test on& uses predefined equality?", N, Ltyp);
+            Error_Msg_N
+              ("\even if user-defined equality exists (RM 4.5.2 (28.1/3)?", N);
+         end if;
+
       end Resolve_Set_Membership;
 
    --  Start of processing for Resolve_Membership_Op
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 248a9b7..972bda5 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -15816,17 +15816,30 @@ package body Sem_Util is
 
    begin
       Expr := N;
-      Par  := Parent (N);
+      Par  := N;
 
       --  A postcondition whose expression is a short-circuit is broken down
       --  into individual aspects for better exception reporting. The original
       --  short-circuit expression is rewritten as the second operand, and an
       --  occurrence of 'Old in that operand is potentially unevaluated.
-      --  See Sem_ch13.adb for details of this transformation.
+      --  See sem_ch13.adb for details of this transformation. The reference
+      --  to 'Old may appear within an expression, so we must look for the
+      --  enclosing pragma argument in the tree that contains the reference.
 
-      if Nkind (Original_Node (Par)) = N_And_Then then
-         return True;
-      end if;
+      while Present (Par)
+        and then Nkind (Par) /= N_Pragma_Argument_Association
+      loop
+         if Nkind (Original_Node (Par)) = N_And_Then then
+            return True;
+         end if;
+
+         Par := Parent (Par);
+      end loop;
+
+      --  Other cases; 'Old appears within other expression (not the top-level
+      --  conjunct in a postcondition) with a potentially unevaluated operand.
+
+      Par := Parent (Expr);
 
       while not Nkind_In (Par, N_If_Expression,
                                N_Case_Expression,