[multiple changes]

2016-06-22  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Add_Invariant): Replace the
	current type instance with the _object parameter even in ASIS mode.
	(Build_Invariant_Procedure_Body): Do not insert the
	invariant procedure body into the tree for ASIS and GNATprove.
	(Build_Invariant_Procedure_Declaration): Do not insert the
	invariant procedure declaration into the tree for ASIS and
	GNATprove.
	* lib-xref-spark_specific.adb (Add_SPARK_Scope): Update comment.

2016-06-22  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Set_Actual_Subtypes): If the type of the actual
	has predicates, the actual subtype must be frozen properly
	because of the generated tests that may follow.  The predicate
	may be specified by an explicit aspect, or may be inherited in
	a derivation.

From-SVN: r237684

4 files changed, 53 insertions, 39 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5703832..a8b4fcb 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,22 @@
+2016-06-22  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch7.adb (Add_Invariant): Replace the
+	current type instance with the _object parameter even in ASIS mode.
+	(Build_Invariant_Procedure_Body): Do not insert the
+	invariant procedure body into the tree for ASIS and GNATprove.
+	(Build_Invariant_Procedure_Declaration): Do not insert the
+	invariant procedure declaration into the tree for ASIS and
+	GNATprove.
+	* lib-xref-spark_specific.adb (Add_SPARK_Scope): Update comment.
+
+2016-06-22  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb (Set_Actual_Subtypes): If the type of the actual
+	has predicates, the actual subtype must be frozen properly
+	because of the generated tests that may follow.  The predicate
+	may be specified by an explicit aspect, or may be inherited in
+	a derivation.
+
 2016-06-22  Ed Schonberg  <schonberg@adacore.com>
 
 	* exp_ch4.adb (In_Range_Chec)): New predicate, subsidiary of
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index b962fcc..3152237 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -4154,39 +4154,32 @@ package body Exp_Ch7 is
                   Set_Etype  (Selector_Name (N), Rep_Typ);
                end if;
 
-               --  Do not alter the tree for ASIS. As a result all references
-               --  to Ref_Typ remain as is, but they have sufficent semantic
-               --  information.
+               --  Perform the following substitution:
 
-               if not ASIS_Mode then
+               --    Ref_Typ  -->  _object
 
-                  --  Perform the following substitution:
+               Ref := Make_Identifier (Nloc, Chars (Obj_Id));
+               Set_Entity (Ref, Obj_Id);
+               Set_Etype  (Ref, Rep_Typ);
 
-                  --    Ref_Typ  -->  _object
+               --  When the pragma denotes a class-wide invariant, perform the
+               --  following substitution:
 
-                  Ref := Make_Identifier (Nloc, Chars (Obj_Id));
-                  Set_Entity (Ref, Obj_Id);
-                  Set_Etype  (Ref, Rep_Typ);
+               --    Rep_Typ  -->  Rep_Typ'Class (_object)
 
-                  --  When the pragma denotes a class-wide invariant, perform
-                  --  the following substitution:
-
-                  --    Rep_Typ  -->  Rep_Typ'Class (_object)
-
-                  if Class_Present (Prag) then
-                     Ref :=
-                       Make_Type_Conversion (Nloc,
-                         Subtype_Mark =>
-                           Make_Attribute_Reference (Nloc,
-                             Prefix         =>
-                               New_Occurrence_Of (Rep_Typ, Nloc),
-                             Attribute_Name => Name_Class),
-                         Expression   => Ref);
-                  end if;
-
-                  Rewrite (N, Ref);
-                  Set_Comes_From_Source (N, True);
+               if Class_Present (Prag) then
+                  Ref :=
+                    Make_Type_Conversion (Nloc,
+                      Subtype_Mark =>
+                        Make_Attribute_Reference (Nloc,
+                          Prefix         =>
+                            New_Occurrence_Of (Rep_Typ, Nloc),
+                          Attribute_Name => Name_Class),
+                      Expression   => Ref);
                end if;
+
+               Rewrite (N, Ref);
+               Set_Comes_From_Source (N, True);
             end Replace_Type_Ref;
 
             procedure Replace_Type_Refs is
@@ -4787,11 +4780,12 @@ package body Exp_Ch7 is
       Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
       Set_Corresponding_Spec (Proc_Body, Proc_Id);
 
-      --  The body should not be inserted into the tree when the context is a
-      --  generic unit because it is not part of the template. Note that the
-      --  body must still be generated in order to resolve the invariants.
+      --  The body should not be inserted into the tree when the context is
+      --  ASIS, GNATprove or a generic unit because it is not part of the
+      --  template. Note that the body must still be generated in order to
+      --  resolve the invariants.
 
-      if Inside_A_Generic then
+      if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
          null;
 
       --  Otherwise the body is part of the freezing actions of the type
@@ -4988,9 +4982,10 @@ package body Exp_Ch7 is
                     New_Occurrence_Of (Work_Typ, Loc)))));
 
       --  The declaration should not be inserted into the tree when the context
-      --  is a generic unit because it is not part of the template.
+      --  is ASIS, GNATprove or a generic unit because it is not part of the
+      --  template.
 
-      if Inside_A_Generic then
+      if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
          null;
 
       --  Otherwise insert the declaration
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 062e50c..8bc6603 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -934,10 +934,9 @@ package body SPARK_Specific is
             D2 := D1;
          end if;
 
-         --  Some files do not correspond to Ada units, and as such present no
-         --  interest for SPARK cross references. Skip these files, as printing
-         --  their name may require printing the full name with spaces, which
-         --  is not handled in the code doing I/O of SPARK cross references.
+         --  Skip dependencies with no entity node, e.g. configuration files
+         --  with pragmas (.adc) or target description (.atp), since they
+         --  present no interest for SPARK cross references.
 
          if Present (Cunit_Entity (Sdep_Table (D1))) then
             Add_SPARK_File
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index ce5f556..0a60d04 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -11308,9 +11308,10 @@ package body Sem_Ch6 is
                  Freeze_Entity (Defining_Identifier (Decl), N));
 
             --  Ditto if the type has a dynamic predicate, because the
-            --  generated function will mention the actual subtype.
+            --  generated function will mention the actual subtype. The
+            --  predicate may come from an explicit aspect of be inherited.
 
-            elsif Has_Dynamic_Predicate_Aspect (T) then
+            elsif Has_Predicates (T) then
                Insert_List_Before_And_Analyze (Decl,
                  Freeze_Entity (Defining_Identifier (Decl), N));
             end if;