[Ada] Enable removal of side-effects in component declarations
Pierre-Marie de Rodat
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...
Size: 591 bytes
Desc: not available
More information about the Gcc-patches