[Ada] Illegal protected calls in inherited pre/postconditions

AI12-0166 specifies that it is illegal for a pre/postcondition of a
protected operation to contain an internal call to a protected function.
This patch completes the implementation of this rule in the case the
condition is inherited from a classwide condition of an abstract operation
of an interface type.

Compiling inheritpo.adb must yield:

   inheritpo.ads:9:04: instantiation error at line 6
   inheritpo.ads:9:04: internal call to "F" cannot appear
      in inherited precondition of protected operation "P"
   inheritpo.ads:9:04: instantiation error at line 7
   inheritpo.ads:9:04: internal call to "F" cannot appear
      in inherited precondition of protected operation "P"

--
package InheritPO is

   type T is limited interface;
   function F (X : T) return Boolean is abstract;
   procedure P (X : in out T) is abstract with
     Pre'Class  => X.F,
     Post'Class => X.F;

   protected type PT is new T with
     overriding function F return Boolean;
     overriding procedure P;
   end PT;

end InheritPO;
----
package body InheritPO is
   protected body PT is
     function F return Boolean is begin return True; end;
     procedure P is begin null; end;
   end PT;
end InheritPO;

2018-01-11  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* sem_ch3.adb (Add_Internal_Interface_Entities): When checking the
	legality of an inherited operation that may require overriding, ignore
	primitive_wrappers that correspond to explicit operations that override
	an interface primitive.

	* exp_util.adb (Build_Class_Wide_Expression, Replace_Entity): If the
	operation to which the class-wide expression applies is a protected op.
	with a primitive_wrapper, verify that the updated inherited expression
	does not contain an internal call to a protected function.  This
	completes the implementation of AI12-0166.

From-SVN: r256491

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 550b760849704be74cddbb6a804c1c46f4e7ede9..1d1933368899dd3f3986942328d71c24827aa7c6 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,15 @@
+2018-01-11  Ed Schonberg  <schonberg@adacore.com>
+
+       * sem_ch3.adb (Add_Internal_Interface_Entities): When checking the
+       legality of an inherited operation that may require overriding, ignore
+       primitive_wrappers that correspond to explicit operations that override
+       an interface primitive.
+       * exp_util.adb (Build_Class_Wide_Expression, Replace_Entity): If the
+       operation to which the class-wide expression applies is a protected op.
+       with a primitive_wrapper, verify that the updated inherited expression
+       does not contain an internal call to a protected function.  This
+       completes the implementation of AI12-0166.
+
 2018-01-11  Hristian Kirtchev  <kirtchev@adacore.com>
 
        * ali.adb: Document the remaining letters available for ALI lines.

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 9ccaa78bc5ddcf98cb1f844de4c7d5b21b948662..058bfe4658b63e2ff860285ebc892f015c89c79d 100644 (file)
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1129,6 +1129,24 @@ package body Exp_Util is
             if Present (New_E) then
                Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
 
+               --  Implement rule in AI12-0166: a precondition for a
+               --  protected operation cannot include an internal call to
+               --  a protected function of the type. In the case of an
+               --  inherited condition for an overriding operation, both the
+               --  operation and the function are given by primitive wrappers.
+
+               if Ekind (New_E) = E_Function
+                 and then Is_Primitive_Wrapper (New_E)
+                 and then Is_Primitive_Wrapper (Subp)
+                 and then Scope (Subp) = Scope (New_E)
+               then
+                  Error_Msg_Node_2 := Wrapped_Entity (Subp);
+                  Error_Msg_NE
+                    ("internal call to& cannot appear in inherited "
+                     & "precondition of protected operation&",
+                       N, Wrapped_Entity (New_E));
+               end if;
+
                --  If the entity is an overridden primitive and we are not
                --  in GNATprove mode, we must build a wrapper for the current
                --  inherited operation. If the reference is the prefix of an

diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 715e6da741c0cf43335a93a52deafd33bdb5da9f..0e898223725d35ddb3165ed2c173995c26944f82 100644 (file)
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1732,6 +1732,9 @@ package body Sem_Ch3 is
                   --  nonconforming preconditions in both an ancestor and
                   --  a progenitor operation.
 
+                  --  If the operation is a primitive wrapper it is an explicit
+                  --  (overriding) operqtion and all is fine.
+
                   if Present (Anc)
                     and then Has_Non_Trivial_Precondition (Anc)
                     and then Has_Non_Trivial_Precondition (Iface_Prim)
@@ -1742,10 +1745,11 @@ package body Sem_Ch3 is
                            and then Nkind (Parent (Prim)) =
                                       N_Procedure_Specification
                            and then Null_Present (Parent (Prim)))
+                       or else Is_Primitive_Wrapper (Prim)
                      then
                         null;
 
-                     --  The inherited operation must be overridden
+                     --  The operation is inherited and must be overridden.
 
                      elsif not Comes_From_Source (Prim) then
                         Error_Msg_NE