freeze.adb (Check_Inherited_Conditions): Perform two passes over the primitive operat...

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index bcd9e52fa34c9afb816c39a0aed3e5fedf4b380c..6784eb24502e46ee84e31de4cd7faf98db63fbff 100644 (file)
--- 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 31c77394949251eb3d68d70eefed31fbb43b486f..b9d70c416c9dcf1fb13a8548105da90e8a97bc9f 100644 (file)
--- 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 a2392e68ee33870eddb1ce59d717c88dd25ea3c3..90d00fca9a1ea31156e30174966770a8a21ab872 100644 (file)
--- 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 064534f6ee34a1abd4db6373c03b8deb3c4e1b07..8613bba1831a64845fc99fe73bc26c528c4cd3a4 100644 (file)
--- 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;