[multiple changes]

2016-04-18  Eric Botcazou  <ebotcazou@adacore.com>

	* layout.adb (Set_Elem_Alignment): Extend setting of alignment
	to subtypes that are not first subtypes.

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.ads (Collect_Inherited_Class_Wide_Conditions):
	Simplify interface.
	* sem_prag.adb (Collect_Inherited_Class_Wide_Conditions): Insert
	generated pragmas after subprogram declaration, rather than in
	the corresponding subprogram body.
	* sem_ch6.adb (New_Overloaded_Entity): In GNATProve
	mode, if the operation is overridding, call
	Collect_Inherited_Class_Wide_Conditions to generate the
	corresponding pragmas immediately after the corresponding
	subprogram declaration.

2016-04-18  Arnaud Charlet  <charlet@adacore.com>

	* spark_xrefs.ads (Xref_Index, Scope_Index, File_Index): restrict
	type to natural numbers.
	(Stype): document code characters for concurrent entities.

2016-04-18  Olivier Hainque  <hainque@adacore.com>

	* targparm.ads: Update the Frontend_Exceptions default internal
	value.
	(Frontend_Exceptions_On_Target): Change default value to True.

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch4.adb (Analyze_Selected_Component): Refine error
	detection when a selected component in the body of a synchronized
	type is a reference to an object of the same type declared
	elsewhere. The construct is legal if the prefix of the selected
	component includes an explicit dereference at any point.

From-SVN: r235118

8 files changed, 229 insertions, 116 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 1183396..0d7e257 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,41 @@
+2016-04-18  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* layout.adb (Set_Elem_Alignment): Extend setting of alignment
+	to subtypes that are not first subtypes.
+
+2016-04-18  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.ads (Collect_Inherited_Class_Wide_Conditions):
+	Simplify interface.
+	* sem_prag.adb (Collect_Inherited_Class_Wide_Conditions): Insert
+	generated pragmas after subprogram declaration, rather than in
+	the corresponding subprogram body.
+	* sem_ch6.adb (New_Overloaded_Entity): In GNATProve
+	mode, if the operation is overridding, call
+	Collect_Inherited_Class_Wide_Conditions to generate the
+	corresponding pragmas immediately after the corresponding
+	subprogram declaration.
+
+2016-04-18  Arnaud Charlet  <charlet@adacore.com>
+
+	* spark_xrefs.ads (Xref_Index, Scope_Index, File_Index): restrict
+	type to natural numbers.
+	(Stype): document code characters for concurrent entities.
+
+2016-04-18  Olivier Hainque  <hainque@adacore.com>
+
+	* targparm.ads: Update the Frontend_Exceptions default internal
+	value.
+	(Frontend_Exceptions_On_Target): Change default value to True.
+
+2016-04-18  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch4.adb (Analyze_Selected_Component): Refine error
+	detection when a selected component in the body of a synchronized
+	type is a reference to an object of the same type declared
+	elsewhere. The construct is legal if the prefix of the selected
+	component includes an explicit dereference at any point.
+
 2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_ch3.adb (Analyze_Object_Declaration): Do not consider
diff --git a/gcc/ada/layout.adb b/gcc/ada/layout.adb
index 97c653c0..15f94a4 100644
--- a/gcc/ada/layout.adb
+++ b/gcc/ada/layout.adb
@@ -3268,80 +3268,114 @@ package body Layout is
          elsif Alignment (E) = A then
             null;
 
-         --  Now we come to the difficult cases where we have inherited an
-         --  alignment and size, but overridden the size but not the alignment.
-
-         elsif Has_Size_Clause (E) or else Has_Object_Size_Clause (E) then
-
-            --  This is tricky, it might be thought that we should try to
-            --  inherit the alignment, since that's what the RM implies, but
-            --  that leads to complex rules and oddities. Consider for example:
-
-            --    type R is new Character;
-            --    for R'Size use 16;
-
-            --  It seems quite bogus in this case to inherit an alignment of 1
-            --  from the parent type Character. Furthermore, if that's what the
-            --  programmer really wanted for some odd reason, then he could
-            --  specify the alignment directly.
-
-            --  Furthermore we really don't want to inherit the alignment in
-            --  the case of a specified Object_Size for a subtype, since then
-            --  there would be no way of overriding to give a reasonable value
-            --  (we don't have an Object_Subtype attribute). Consider:
-
-            --    subtype R is Character;
-            --    for R'Object_Size use 16;
-
-            --  If we inherit the alignment of 1, then we have an inefficient
-            --  alignment for the subtype, which cannot be fixed.
-
-            --  So we make the decision that if Size (or Object_Size) is given
-            --  (and, in the case of a first subtype, the alignment is not set
-            --  with a specific alignment clause), we reset the alignment to
-            --  the appropriate value for the specified size. This is a nice
-            --  simple rule to implement and document.
-
-            --  There is one slight glitch, which is that a confirming size
-            --  clause can now change the alignment, which, if we really think
-            --  that confirming rep clauses should have no effect, is a no-no.
-
-            --    type R is new Character;
-            --    for R'Alignment use 2;
-            --    type S is new R;
-            --    for S'Size use Character'Size;
-
-            --  Now the alignment of S is changed to 1 instead of 2 as a result
-            --  of applying the above rule to the confirming rep clause for S.
-            --  Not clear this is worth worrying about. If we recorded whether
-            --  a size clause was confirming we could avoid this, but right now
-            --  we have no way of doing that or easily figuring it out, so we
-            --  don't bother.
-
-            --  Historical note: in versions of GNAT prior to Nov 6th, 2011, an
-            --  odd distinction was made between inherited alignments larger
-            --  than the computed alignment (where the larger alignment was
-            --  inherited) and inherited alignments smaller than the computed
-            --  alignment (where the smaller alignment was overridden). This
-            --  was a dubious fix to get around an ACATS problem which seems
-            --  to have disappeared anyway, and in any case, this peculiarity
-            --  was never documented.
+         else
+            --  Now we come to the difficult cases of subtypes for which we
+            --  have inherited an alignment different from the computed one.
+            --  We resort to the presence of alignment and size clauses to
+            --  guide our choices. Note that they can generally be present
+            --  only on the first subtype (except for Object_Size) and that
+            --  we need to look at the Rep_Item chain to correctly handle
+            --  derived types.
 
-            Init_Alignment (E, A);
+            declare
+               FST : constant Entity_Id := First_Subtype (E);
 
-         --  If no Size (or Object_Size) was specified, then we inherited the
-         --  object size, so we should inherit the alignment as well and not
-         --  modify it. This takes care of cases like:
+               function Has_Attribute_Clause
+                 (E  : Entity_Id;
+                  Id : Attribute_Id) return Boolean;
+               --  Wrapper around Get_Attribute_Definition_Clause which tests
+               --  for the presence of the specified attribute clause.
 
-         --    type R is new Integer;
-         --    for R'Alignment use 1;
-         --    subtype S is R;
+               --------------------------
+               -- Has_Attribute_Clause --
+               --------------------------
 
-         --  Here we have R with a default Object_Size of 32, and a specified
-         --  alignment of 1, and it seeems right for S to inherit both values.
+               function Has_Attribute_Clause
+                 (E  : Entity_Id;
+                  Id : Attribute_Id) return Boolean is
+               begin
+                  return Present (Get_Attribute_Definition_Clause (E, Id));
+               end Has_Attribute_Clause;
 
-         else
-            null;
+            begin
+               --  If the alignment comes from a clause, then we respect it.
+               --  Consider for example:
+
+               --    type R is new Character;
+               --    for R'Alignment use 1;
+               --    for R'Size use 16;
+               --    subtype S is R;
+
+               --  Here R has a specified size of 16 and a specified alignment
+               --  of 1, and it seems right for S to inherit both values.
+
+               if Has_Attribute_Clause (FST, Attribute_Alignment) then
+                  null;
+
+               --  Now we come to the cases where we have inherited alignment
+               --  and size, and overridden the size but not the alignment.
+
+               elsif Has_Attribute_Clause (FST, Attribute_Size)
+                 or else Has_Attribute_Clause (FST, Attribute_Object_Size)
+                 or else Has_Attribute_Clause (E, Attribute_Object_Size)
+               then
+                  --  This is tricky, it might be thought that we should try to
+                  --  inherit the alignment, since that's what the RM implies,
+                  --  but that leads to complex rules and oddities. Consider
+                  --  for example:
+
+                  --    type R is new Character;
+                  --    for R'Size use 16;
+
+                  --  It seems quite bogus in this case to inherit an alignment
+                  --  of 1 from the parent type Character. Furthermore, if that
+                  --  is what the programmer really wanted for some odd reason,
+                  --  then he could specify the alignment directly.
+
+                  --  Moreover we really don't want to inherit the alignment in
+                  --  the case of a specified Object_Size for a subtype, since
+                  --  there would be no way of overriding to give a reasonable
+                  --  value (as we don't have an Object_Alignment attribute).
+                  --  Consider for example:
+
+                  --    subtype R is Character;
+                  --    for R'Object_Size use 16;
+
+                  --  If we inherit the alignment of 1, then it will be very
+                  --  inefficient for the subtype and this cannot be fixed.
+
+                  --  So we make the decision that if Size (or Object_Size) is
+                  --  given and the alignment is not specified with a clause,
+                  --  we reset the alignment to the appropriate value for the
+                  --  specified size. This is a nice simple rule to implement
+                  --  and document.
+
+                  --  There is a theoretical glitch, which is that a confirming
+                  --  size clause could now change the alignment, which, if we
+                  --  really think that confirming rep clauses should have no
+                  --  effect, could be seen as a no-no. However that's already
+                  --  implemented by Alignment_Check_For_Size_Change so we do
+                  --  not change the philosophy here.
+
+                  --  Historical note: in versions prior to Nov 6th, 2011, an
+                  --  odd distinction was made between inherited alignments
+                  --  larger than the computed alignment (where the larger
+                  --  alignment was inherited) and inherited alignments smaller
+                  --  than the computed alignment (where the smaller alignment
+                  --  was overridden). This was a dubious fix to get around an
+                  --  ACATS problem which seems to have disappeared anyway, and
+                  --  in any case, this peculiarity was never documented.
+
+                  Init_Alignment (E, A);
+
+               --  If no Size (or Object_Size) was specified, then we have
+               --  inherited the object size, so we should also inherit the
+               --  alignment and not modify it.
+
+               else
+                  null;
+               end if;
+            end;
          end if;
       end;
    end Set_Elem_Alignment;
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index bdcf0e1..04b9dbd 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -4657,21 +4657,44 @@ package body Sem_Ch4 is
          end loop;
 
          --  If the scope is a current instance, the prefix cannot be an
-         --  expression of the same type (that would represent an attempt
-         --  to reach an internal operation of another synchronized object).
+         --  expression of the same type, unless the selector designates a
+         --  public operation (otherwise that would represent an attempt to
+         --  reach an internal entity of another synchronized object).
          --  This is legal if prefix is an access to such type and there is
-         --  a dereference.
+         --  a dereference, or is a component with a dereferenced prefix.
 
-         if In_Scope
-           and then not Is_Entity_Name (Name)
-           and then Nkind (Name) /= N_Explicit_Dereference
-         then
-            Error_Msg_NE
-              ("invalid reference to internal operation of some object of "
-               & "type &", N, Type_To_Use);
-            Set_Entity (Sel, Any_Id);
-            Set_Etype  (Sel, Any_Type);
-            return;
+         if In_Scope and then not Is_Entity_Name (Name) then
+            declare
+
+               function Has_Dereference (N : Node_Id) return Boolean;
+               --  Check whether prefix includes a dereference at any level.
+
+               ---------------------
+               -- Has_Dereference --
+               ---------------------
+
+               function Has_Dereference (N : Node_Id) return Boolean is
+               begin
+                  if Nkind (N) = N_Explicit_Dereference then
+                     return True;
+                  elsif
+                    Nkind_In (N, N_Selected_Component, N_Indexed_Component)
+                  then
+                     return Has_Dereference (Prefix (N));
+                  else
+                     return False;
+                  end if;
+               end Has_Dereference;
+
+            begin
+               if not Has_Dereference (Name) then
+                  Error_Msg_NE ("invalid reference to internal operation "
+                     & "of some object of type &", N, Type_To_Use);
+                  Set_Entity (Sel, Any_Id);
+                  Set_Etype  (Sel, Any_Type);
+                  return;
+               end if;
+            end;
          end if;
 
          --  If there is no visible entity with the given name or none of the
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 9563320..0e03ff6 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3761,15 +3761,7 @@ package body Sem_Ch6 is
       end if;
 
       --  When generating code, inherited pre/postconditions are handled when
-      --  expanding the corresponding contract. In GNATprove the annotations
-      --  must be processed when the body is analyzed.
-
-      if GNATprove_Mode
-        and then Present (Spec_Id)
-        and then Present (Overridden_Operation (Spec_Id))
-      then
-         Collect_Inherited_Class_Wide_Conditions (Spec_Id, N);
-      end if;
+      --  expanding the corresponding contract.
 
       --  Ada 2005 (AI-262): In library subprogram bodies, after the analysis
       --  of the specification we have to install the private withed units.
@@ -9946,6 +9938,13 @@ package body Sem_Ch6 is
                         Set_Convention (S, Convention (E));
                         Check_Dispatching_Operation (S, E);
 
+                        --  In GNATprove_Mode, create the pragmas corresponding
+                        --  to inherited class-wide conditions.
+
+                        if GNATprove_Mode then
+                           Collect_Inherited_Class_Wide_Conditions (S);
+                        end if;
+
                      else
                         Check_Dispatching_Operation (S, Empty);
                      end if;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 7be7172..173b14b 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -26759,17 +26759,18 @@ package body Sem_Prag is
    -- Collect_Inherited_Class_Wide_Conditions --
    ---------------------------------------------
 
-   procedure Collect_Inherited_Class_Wide_Conditions
-     (Subp : Entity_Id;
-      Bod  : Node_Id)
-   is
+   procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id) is
       Parent_Subp : constant Entity_Id := Overridden_Operation (Subp);
       Prags       : constant Node_Id   := Contract (Parent_Subp);
       Prag        : Node_Id;
+      New_Prag    : Node_Id;
+      Installed   : Boolean;
 
    begin
-      --  Iterate over the contract to find inherited class-wide pre- and
-      --  postconditions.
+      Installed := False;
+
+      --  Iterate over the contract of the overridden subprogram  to find
+      --  inherited class-wide pre- and postconditions.
 
       if Present (Prags) then
          Prag := Pre_Post_Conditions (Prags);
@@ -26777,17 +26778,29 @@ package body Sem_Prag is
          while Present (Prag) loop
             if Nam_In (Pragma_Name (Prag), Name_Precondition,
                                            Name_Postcondition)
+              and then Class_Present (Prag)
             then
-               if No (Declarations (Bod)) then
-                  Set_Declarations (Bod, Empty_List);
+               --  The generated pragma must be analyzed in the context of
+               --  the subprogram, to make its formals visible.
+
+               if not Installed then
+                  Installed := True;
+                  Push_Scope (Subp);
+                  Install_Formals (Subp);
                end if;
 
-               Append_To (Declarations (Bod),
-                 Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp));
+               New_Prag :=
+                 Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp);
+               Insert_After (Unit_Declaration_Node (Subp), New_Prag);
+               Preanalyze (New_Prag);
             end if;
 
             Prag := Next_Pragma (Prag);
          end loop;
+
+         if Installed then
+            End_Scope;
+         end if;
       end if;
    end Collect_Inherited_Class_Wide_Conditions;
 
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index a78478e..7afb6e6 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -311,12 +311,12 @@ package Sem_Prag is
    --  state, variable or package instantiation denoted by Item_Id requires the
    --  use of indicator/option Part_Of. If this is the case, emit an error.
 
-   procedure Collect_Inherited_Class_Wide_Conditions
-     (Subp : Entity_Id;
-      Bod  : Node_Id);
-   --  When analyzing an overriding subprogram, check whether the overridden
-   --  operations have class-wide pre/postconditions, and generate the
-   --  corresponding pragmas.
+   procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id);
+   --  In GNATprove mode, when analyzing an overriding subprogram, check
+   --  whether the overridden operations have class-wide pre/postconditions,
+   --  and generate the corresponding pragmas. The pragmas are inserted after
+   --  the subprogram declaration, together with those generated for other
+   --  aspects of the subprogram.
 
    procedure Collect_Subprogram_Inputs_Outputs
      (Subp_Id      : Entity_Id;
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index f6cc7c3..eb95f73 100644
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -209,9 +209,10 @@ package SPARK_Xrefs is
 
    --  The following table records SPARK cross-references
 
-   type Xref_Index is new Int;
+   type Xref_Index is new Nat;
    --  Used to index values in this table. Values start at 1 and are assigned
-   --  sequentially as entries are constructed.
+   --  sequentially as entries are constructed; value 0 is used temporarily
+   --  until a proper value is determined.
 
    type SPARK_Xref_Record is record
       Entity_Name : String_Ptr;
@@ -268,9 +269,11 @@ package SPARK_Xrefs is
    --  This table keeps track of the scopes and the corresponding starting and
    --  ending indexes (From, To) in the Xref table.
 
-   type Scope_Index is new Int;
+   type Scope_Index is new Nat;
    --  Used to index values in this table. Values start at 1 and are assigned
-   --  sequentially as entries are constructed.
+   --  sequentially as entries are constructed; value 0 indicates that no
+   --  entries have been constructed and is also used until a proper value is
+   --  determined.
 
    type SPARK_Scope_Record is record
       Scope_Name : String_Ptr;
@@ -296,8 +299,10 @@ package SPARK_Xrefs is
       Stype : Character;
       --  Indicates type of scope, using code used in ALI file:
       --    K = package
-      --    V = function
+      --    T = task
       --    U = procedure
+      --    V = function
+      --    Y = entry
 
       Col : Nat;
       --  Column number for the scope
@@ -329,9 +334,10 @@ package SPARK_Xrefs is
    --  This table keeps track of the units and the corresponding starting and
    --  ending indexes (From, To) in the Scope table.
 
-   type File_Index is new Int;
+   type File_Index is new Nat;
    --  Used to index values in this table. Values start at 1 and are assigned
-   --  sequentially as entries are constructed.
+   --  sequentially as entries are constructed; value 0 indicates that no
+   --  entries have been constructed.
 
    type SPARK_File_Record is record
       File_Name : String_Ptr;
diff --git a/gcc/ada/targparm.ads b/gcc/ada/targparm.ads
index af2177d..9964425 100644
--- a/gcc/ada/targparm.ads
+++ b/gcc/ada/targparm.ads
@@ -261,7 +261,7 @@ package Targparm is
    --    Back-End Setjmp/Longjmp Exceptions
 
    --      With this approach, the back end also handles the generation and
-   --      handling of exceptions, using setjmp/longjmp to setup receivers and
+   --      handling of exceptions, using setjmp/longjmp to set up receivers and
    --      propagate. AT-END actions on exceptional paths are also taken care
    --      of by the back end and the front end doesn't need to generate
    --      explicit exception handlers for these.
@@ -271,7 +271,7 @@ package Targparm is
    --      The following switches specify whether we're using a front-end or a
    --      back-end mechanism and whether this is a zero-cost or a sjlj scheme.
 
-   --      The per switch default values correspond to the default value of
+   --      The per-switch default values correspond to the default value of
    --      Opt.Exception_Mechanism.
 
    ZCX_By_Default_On_Target : Boolean := False;