diff options
| author | Javier Miranda <miranda@adacore.com> | 2024-05-03 17:52:20 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2024-06-13 15:30:34 +0200 |
| commit | df898445c211cb417fad784d50a68bae0f20acbc (patch) | |
| tree | ad0bfa00064a29922a491b6a1e7eb2543223aa41 /gcc/ada/sem_disp.adb | |
| parent | 0662d7426835a69bf233c3f9a025b30e84563ff2 (diff) | |
| download | gcc-df898445c211cb417fad784d50a68bae0f20acbc.zip gcc-df898445c211cb417fad784d50a68bae0f20acbc.tar.gz gcc-df898445c211cb417fad784d50a68bae0f20acbc.tar.bz2 | |
ada: Missing postcondition runtime check in inherited primitive
When a derived tagged type implements more interface interface types
than its parent type, and a primitive inherited from its parent type
covers a primitive of these additional interface types that has
classwide postconditions, the code generated by the compiler does not
check the classwide postconditions inherited from the interface primitive.
gcc/ada/
* freeze.ads (Check_Condition_Entities): Complete documentation.
* freeze.adb (Check_Inherited_Conditions): Extend its functionality to
build two kind of wrappers: the existing LSP wrappers, and wrappers
required to handle postconditions of interface primitives implemented
by inherited primitives.
(Build_Inherited_Condition_Pragmas): Rename formal.
(Freeze_Record_Type): For derived tagged types, move call to
Check_Inherited_Conditions to subprogram Freeze_Entity_Checks;
done to improve the performance of Check_Inherited_Conditions since it
can rely on the internal entities that link interface primitives with
tagged type primitives that implement them.
(Check_Interface_Primitives_Strub_Mode): New subprogram.
* sem_ch13.adb (Freeze_Entity_Checks): Call Check_Inherited_Conditions.
Call Check_Inherited_Conditions with derived interface types to check
strub mode compatibility of their primitives.
* sem_disp.adb (Check_Dispatching_Operation): Adjust assertion to accept
wrappers of interface primitives that have classwide postconditions.
* exp_disp.adb (Write_DT): Adding text to identify wrappers.
Diffstat (limited to 'gcc/ada/sem_disp.adb')
| -rw-r--r-- | gcc/ada/sem_disp.adb | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index fd521a0..9c498ee 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -1388,10 +1388,13 @@ package body Sem_Disp is -- 3. Subprograms associated with stream attributes (built by -- New_Stream_Subprogram) or with the Put_Image attribute. - -- 4. Wrappers built for inherited operations with inherited class- - -- wide conditions, where the conditions include calls to other - -- overridden primitives. The wrappers include checks on these - -- modified conditions. (AI12-195). + -- 4. Wrappers built for inherited operations. We have two kinds: + -- * Wrappers built for inherited operations with inherited class- + -- wide conditions, where the conditions include calls to other + -- overridden primitives. The wrappers include checks on these + -- modified conditions (AI12-195). + -- * Wrappers built for inherited operations that implement + -- interface primitives that have class-wide postconditions. -- 5. Declarations built for subprograms without separate specs that -- are eligible for inlining in GNATprove (inside @@ -1419,7 +1422,7 @@ package body Sem_Disp is or else (Is_Wrapper (Subp) - and then Present (LSP_Subprogram (Subp))) + and then Is_Dispatch_Table_Wrapper (Subp)) or else GNATprove_Mode); |