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

Pierre-Marie de Rodat derodat@adacore.com
Tue Jun 15 10:20:52 GMT 2021

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

Tested on x86_64-pc-linux-gnu, committed on trunk


	* exp_util.adb (Possible_Side_Effect_In_SPARK): Handle component
	declaration just like full type and subtype declarations.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 591 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20210615/b7e64014/attachment-0001.bin>

More information about the Gcc-patches mailing list