https://gcc.gnu.org/g:cc113fac909df3e68a4f445ba307d65c7ba39ea2
commit r16-4132-gcc113fac909df3e68a4f445ba307d65c7ba39ea2 Author: Piotr Trojanek <[email protected]> Date: Tue Jul 15 15:18:26 2025 +0200 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: --- gcc/ada/exp_util.adb | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 78fb3167c82d..30b2461c4af6 100644 --- 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
