diff options
| author | Gary Dismukes <dismukes@adacore.com> | 2020-12-14 15:31:52 -0500 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-04-29 04:00:46 -0400 |
| commit | 427c07a2fc7e9799552499795bbe60664ef142ac (patch) | |
| tree | 4b808b667515bf1231e75341e23c78242eb2b8fe /gcc | |
| parent | 40f0ef4fa378fc0506be622209927bd2f3c2d6f8 (diff) | |
| download | gcc-427c07a2fc7e9799552499795bbe60664ef142ac.zip gcc-427c07a2fc7e9799552499795bbe60664ef142ac.tar.gz gcc-427c07a2fc7e9799552499795bbe60664ef142ac.tar.bz2 | |
[Ada] SPARK needs DIC expressions within partial DIC procedures for abstract types
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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/exp_util.adb | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 36af89b..801db80 100644 --- 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, |