Side-effects in component declarations are prohibited in SPARK (both in
the constraints of component type definitions and in the default
expressions), but GNAT requires them to be removed when processing
records with per-object constraints.
This patch allows removal of side-effects in component declaration just
like it was allowed in top-level full type and subtype declarations.
This fixes a crash in processing of record aggregates with per-object
constraints in the frontend; side effects, if any, will be removed later
in the backend anyway.
The fix only affects GNATprove; the modified routine is not used by
GNAT.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* exp_util.adb (Possible_Side_Effect_In_SPARK): Handle component
declaration just like full type and subtype declarations.diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -11485,7 +11485,8 @@ package body Exp_Util is
return not Inside_A_Generic
and then Full_Analysis
and then Nkind (Enclosing_Declaration (Exp)) in
- N_Full_Type_Declaration
+ N_Component_Declaration
+ | N_Full_Type_Declaration
| N_Iterator_Specification
| N_Loop_Parameter_Specification
| N_Object_Renaming_Declaration
