From: Gary Dismukes <dismukes@adacore.com>
Date: Mon, 14 Dec 2020 20:31:52 +0000 (-0500)
Subject: [Ada] SPARK needs DIC expressions within partial DIC procedures for abstract types
X-Git-Tag: basepoints/gcc-13~8049
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=427c07a2fc7e9799552499795bbe60664ef142ac;p=thirdparty%2Fgcc.git

[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.
---

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 36af89ba276d..801db80a3847 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,