[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

1 files changed, 13 insertions, 7 deletions

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;