[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 36af89ba276d48526a30ac7f2976b2208ba97fce..801db80a3847ef3f16788f65c3887cc6d194228b 100644 (file)
--- 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,