[Ada] Illegal protected calls in inherited pre/postconditions
Pierre-Marie de Rodat
derodat@adacore.com
Thu Jan 11 09:06:00 GMT 2018
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 <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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 2497 bytes
Desc: not available
URL: <http://gcc.gnu.org/pipermail/gcc-patches/attachments/20180111/f54e63eb/attachment.bin>
More information about the Gcc-patches
mailing list