diff mbox series

[Ada] Enable removal of side-effects in component declarations

Message ID 20210615102052.GA4298@adacore.com
State New
Headers show
Series [Ada] Enable removal of side-effects in component declarations | expand

Commit Message

Pierre-Marie de Rodat June 15, 2021, 10:20 a.m. UTC 
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 mbox series

Patch

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