A recent change done as part of the implementation of AI12-0397 was to
suppress generation of DIC check expressions within DIC procedures
associated with abstract types (to avoid producing calls to abstract
subprograms, which are legal to give in a DIC aspect, but would cause
problems for gigi if they resulted in actual calls). However, SPARK
still needs access to the resolved expression of the DIC aspect, which
normally occurs within the partial DIC procedure of the type. This is
fixed by adding a test of GNATprove_Mode to avoid suppressing the
DIC check pragma when running SPARK tools.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* exp_util.adb (Add_Own_DIC): Relax the suppression of adding a
DIC Check pragma that's done for abstract types by still doing
it in the case where GNATprove_Mode is set.diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1860,7 +1860,7 @@ package body Exp_Util is
-- procedures can never be called in any case, so not generating the
-- check at all is OK).
- if not Is_Abstract_Type (DIC_Typ) then
+ if not Is_Abstract_Type (DIC_Typ) or else GNATprove_Mode then
Add_DIC_Check
(DIC_Prag => DIC_Prag,
DIC_Expr => Expr,
