freeze.adb (Check_Inherited_Conditions): Perform two passes over the primitive operations of the type...

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

	* freeze.adb (Check_Inherited_Conditions): Perform two passes over
	the primitive operations of the type: one over source overridings
	to build the primitives mapping, and one over inherited operations
	to check for the need to create wrappers, and to check legality
	of inherited condition in SPARK.
	* sem_prag.ads (Update_Primitive_Mapping): Make public, for use
	in freeze actions.
	* sem_prag.adb (Build_Pragma_Check_Equivalent): Refine error
	message in the case of an inherited condition in SPARK that
	includes a call to some other overriding primitive.

From-SVN: r237960

4 files changed, 67 insertions, 23 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index bcd9e52..6784eb2 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,16 @@
+2016-07-04  Ed Schonberg  <schonberg@adacore.com>
+
+	* freeze.adb (Check_Inherited_Conditions): Perform two passes over
+	the primitive operations of the type: one over source overridings
+	to build the primitives mapping, and one over inherited operations
+	to check for the need to create wrappers, and to check legality
+	of inherited condition in SPARK.
+	* sem_prag.ads (Update_Primitive_Mapping): Make public, for use
+	in freeze actions.
+	* sem_prag.adb (Build_Pragma_Check_Equivalent): Refine error
+	message in the case of an inherited condition in SPARK that
+	includes a call to some other overriding primitive.
+
 2016-07-04  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* exp_aggr.adb (Ctrl_Init_Expression): New routine.
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 31c7739..b9d70c4 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -1403,24 +1403,39 @@ package body Freeze is
       while Present (Op_Node) loop
          Prim := Node (Op_Node);
 
-         --  In SPARK mode this is where we can collect the inherited
-         --  conditions, because we do not create the Check pragmas that
-         --  normally convey the modified classwide conditions on overriding
-         --  operations.
-
-         if SPARK_Mode = On
-           and then Comes_From_Source (Prim)
-           and then Present (Overridden_Operation (Prim))
+         --  Map the overridden primitive to the overriding one. This
+         --  takes care of all overridings and is done only once.
+
+         if Present (Overridden_Operation (Prim))
+            and then Comes_From_Source (Prim)
          then
-            Collect_Inherited_Class_Wide_Conditions (Prim);
+            Update_Primitives_Mapping (Overridden_Operation (Prim), Prim);
+
+            --  In SPARK mode this is where we can collect the inherited
+            --  conditions, because we do not create the Check pragmas that
+            --  normally convey the the modified classwide conditions on
+            --  overriding operations.
+
+            if SPARK_Mode = On then
+               Collect_Inherited_Class_Wide_Conditions (Prim);
+            end if;
          end if;
 
-         --  In normal mode, we examine inherited operations to check whether
-         --  they require a wrapper to handle inherited conditions that call
-         --  other primitives.
-         --  Wrapper construction TBD.
+         Next_Elmt (Op_Node);
+      end loop;
+
+      --  In all cases, we examine inherited operations to check whether they
+      --  require a wrapper to handle inherited conditions that call other
+      --  primitives, so that LSP can be verified/enforced.
+
+      --  Wrapper construction TBD.
 
-         if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then
+      Op_Node := First_Elmt (Prim_Ops);
+      while Present (Op_Node) loop
+         Prim := Node (Op_Node);
+         if not Comes_From_Source (Prim)
+           and then Present (Alias (Prim))
+         then
             Par_Prim := Alias (Prim);
             A_Pre    := Find_Aspect (Par_Prim, Aspect_Pre);
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index a2392e6..90d00fc 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -322,13 +322,6 @@ package body Sem_Prag is
    --  pragma. Entity name for unit and its parents is taken from item in
    --  previous with_clause that mentions the unit.
 
-   procedure Update_Primitives_Mapping
-     (Inher_Id : Entity_Id;
-      Subp_Id  : Entity_Id);
-   --  Map primitive operations of the parent type to the corresponding
-   --  operations of the descendant. Note that the descendant type may
-   --  not be frozen yet, so we cannot use the dispatch table directly.
-
    Dummy : Integer := 0;
    pragma Volatile (Dummy);
    --  Dummy volatile integer used in bodies of ip/rv to prevent optimization
@@ -26380,13 +26373,25 @@ package body Sem_Prag is
                     ("cannot call abstract subprogram in inherited condition "
                       & "for&#", N, Current_Scope);
 
+               --  In SPARK mode, reject an inherited condition for an
+               --  inherited operation if it contains a call to an overriding
+               --  operation, because this implies that the pre/postcondition
+               --  of the inherited operation have changed silently.
+
                elsif SPARK_Mode = On
                  and then Warn_On_Suspicious_Contract
                  and then Present (Alias (Subp))
+                 and then Present (New_E)
+                 and then Comes_From_Source (New_E)
                then
+                  Error_Msg_N
+                    ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
+                      Parent (Subp));
+                  Error_Msg_Sloc := Sloc (New_E);
+                  Error_Msg_Node_2 := Subp;
                   Error_Msg_NE
-                    ("?inherited condition is modified, build a wrapper "
-                     & "for&", Parent (Subp), Subp);
+                    ("\overriding of&# forces overriding of&",
+                     Parent (Subp), New_E);
                end if;
             end if;
 
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 064534f..8613bba 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -528,4 +528,15 @@ package Sem_Prag is
    --
    --    Empty if there is no such argument
 
+   procedure Update_Primitives_Mapping
+     (Inher_Id : Entity_Id;
+      Subp_Id  : Entity_Id);
+
+   --  map primitive operations of the parent type to the corresponding
+   --  operations of the descendant. note that the descendant type may
+   --  not be frozen yet, so we cannot use the dispatch table directly.
+   --  This is called when elaborating a contract for a subprogram, and
+   --  when freezing a type extension to verify legality rules on inherited
+   --  conditions.
+
 end Sem_Prag;