[multiple changes]
authorArnaud Charlet <charlet@gcc.gnu.org>
Wed, 22 Jun 2016 09:51:47 +0000 (11:51 +0200)
committerArnaud Charlet <charlet@gcc.gnu.org>
Wed, 22 Jun 2016 09:51:47 +0000 (11:51 +0200)
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

gcc/ada/ChangeLog
gcc/ada/exp_ch7.adb
gcc/ada/lib-xref-spark_specific.adb
gcc/ada/sem_ch6.adb

index 5703832c6f5651722a64c3e62a53254f4e4d9224..a8b4fcb2353612b0eeb8653d637e525d62c3f288 100644 (file)
@@ -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
index b962fcc78a095da3910c3ee9b26ce94bcb099f22..31522370058abe015bbd06dd73bd37b700f06ce2 100644 (file)
@@ -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
index 062e50c262289c883ed3010e5ffa17a6bf306f84..8bc660309ac714af3348911a621d6e863aab633c 100644 (file)
@@ -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
index ce5f55663be9c0a171f67b68fbb9b628d464b2cd..0a60d048d4cd0e4417abf104dd3d045150570bed 100644 (file)
@@ -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;