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;
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-01-11 Ed Schonberg <schonb...@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.
--- gcc/ada/exp_util.adb
+++ 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--- gcc/ada/sem_ch3.adb
+++ 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
