ada: Add special-case for 'Constrained on stand-alone objects in SPARK

GNAT relies on standalone objects of indefinite, non-class-wide types getting a
constrained itypes; GNATprove relies on the same objects keeping their nominal,
unconstrained types. None of that can be simply changed, so instead we carry
this different handling to routine which provides the value of attribute
Constrained.

gcc/ada/ChangeLog:

	* exp_util.adb (Attribute_Constrained_Static_Value): Special case
	stand-alone objects for GNATprove.

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 78fb3167c82ddee86835ebe6f623b6cc391c4636..30b2461c4af6d2d538edaabcaf1107fac832f049 100644 (file)
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -638,6 +638,23 @@ package body Exp_Util is
                end if;
 
             else
+               --  For GNAT objects with indefinite nominal subtypes will have
+               --  an itype constrained by their initialization expression
+               --  (except for class-wide type). For GNATprove, those objects
+               --  will keep their nominal subtype unconstrained, while
+               --  actually those objects are constrained; see call from
+               --  Analyze_Object_Declaration to Expand_Subtype_From_Expr.
+
+               if Ekind (Ent) in E_Constant | E_Variable
+                  and then not Is_Definite_Subtype (Etype (Ent))
+                  and then not Is_Class_Wide_Type (Etype (Ent))
+                  and then No (Renamed_Object (Ent))
+               then
+                  pragma Assert
+                    (GNATprove_Mode
+                     and then Present (Expression (Parent (Ent))));
+                  return True;
+               end if;
 
                --  If the prefix is not a variable or is aliased, then
                --  definitely true; if it's a formal parameter without an