ada: Support new SPARK aspect Side_Effects
commit04d6c74564b7eb51660a00b35353aeab706b5a50
authorYannick Moy <moy@adacore.com>
Tue, 26 Sep 2023 15:29:12 +0000 (26 17:29 +0200)
committerMarc Poulhiès <poulhies@adacore.com>
Thu, 19 Oct 2023 14:35:22 +0000 (19 16:35 +0200)
treee019b8517a3df3e6404ad52a740db16c3013a209
parentc1fbfe5acbf02674c9fb411ffcccec5c6ed9a5eb
ada: Support new SPARK aspect Side_Effects

SPARK RM 6.1.11 introduces a new aspect Side_Effects to denote
those functions which may have output parameters, write global
variables, raise exceptions and not terminate. This adds support
for this aspect and the corresponding pragma in the frontend.

Handling of this aspect in the frontend is very similar to
the handling of aspect Extensions_Visible: both are Boolean
aspects whose expression should be static, they can be specified
on the same entities, with the same rule of inheritance from
overridden to overriding primitives for tagged types.

There is no impact on code generation.

gcc/ada/

* aspects.ads: Add aspect Side_Effects.
* contracts.adb (Add_Pre_Post_Condition)
(Inherit_Subprogram_Contract): Add support for new contract.
* contracts.ads: Update comments.
* einfo-utils.adb (Get_Pragma): Add support.
* einfo-utils.ads (Prag): Update comment.
* errout.ads: Add explain codes.
* par-prag.adb (Prag): Add support.
* sem_ch13.adb (Analyze_Aspect_Specifications)
(Check_Aspect_At_Freeze_Point): Add support.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper)
(Analyze_Subprogram_Declaration): Call new analysis procedure to
check SPARK legality rules.
(Analyze_SPARK_Subprogram_Specification): New procedure to check
SPARK legality rules. Use an explain code for the error.
(Analyze_Subprogram_Specification): Move checks to new subprogram.
This code was effectively dead, as the kind for parameters was set
to E_Void at this point to detect early references.
* sem_ch6.ads (Analyze_Subprogram_Specification): Add new
procedure.
* sem_prag.adb (Analyze_Depends_In_Decl_Part)
(Analyze_Global_In_Decl_Part): Adapt legality check to apply only
to functions without side-effects.
(Analyze_If_Present): Extract functionality in new procedure
Analyze_If_Present_Internal.
(Analyze_If_Present_Internal): New procedure to analyze given
pragma kind.
(Analyze_Pragmas_If_Present): New procedure to analyze given
pragma kind associated with a declaration.
(Analyze_Pragma): Adapt support for Always_Terminates and
Exceptional_Cases. Add support for Side_Effects. Make sure to call
Analyze_If_Present to ensure pragma Side_Effects is analyzed prior
to analyzing pragmas Global and Depends. Use explain codes for the
errors.
* sem_prag.ads (Analyze_Pragmas_If_Present): Add new procedure.
* sem_util.adb (Is_Function_With_Side_Effects): New query function
to determine if a function is a function with side-effects.
* sem_util.ads (Is_Function_With_Side_Effects): Same.
* snames.ads-tmpl: Declare new names for pragma and aspect.
* doc/gnat_rm/implementation_defined_aspects.rst: Document new aspect.
* doc/gnat_rm/implementation_defined_pragmas.rst: Document new pragma.
* gnat_rm.texi: Regenerate.
18 files changed:
gcc/ada/aspects.ads
gcc/ada/contracts.adb
gcc/ada/contracts.ads
gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
gcc/ada/einfo-utils.adb
gcc/ada/einfo-utils.ads
gcc/ada/errout.ads
gcc/ada/gnat_rm.texi
gcc/ada/par-prag.adb
gcc/ada/sem_ch13.adb
gcc/ada/sem_ch6.adb
gcc/ada/sem_ch6.ads
gcc/ada/sem_prag.adb
gcc/ada/sem_prag.ads
gcc/ada/sem_util.adb
gcc/ada/sem_util.ads
gcc/ada/snames.ads-tmpl