[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
This commit is contained in:
parent
94ce49419a
commit
5cb78fb862
|
@ -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.
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue