diff options
author | Yannick Moy <moy@adacore.com> | 2023-09-26 17:29:12 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-10-19 16:35:22 +0200 |
commit | 04d6c74564b7eb51660a00b35353aeab706b5a50 (patch) | |
tree | e019b8517a3df3e6404ad52a740db16c3013a209 /gcc/ada/sem_ch6.adb | |
parent | c1fbfe5acbf02674c9fb411ffcccec5c6ed9a5eb (diff) | |
download | gcc-04d6c74564b7eb51660a00b35353aeab706b5a50.zip gcc-04d6c74564b7eb51660a00b35353aeab706b5a50.tar.gz gcc-04d6c74564b7eb51660a00b35353aeab706b5a50.tar.bz2 |
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.
Diffstat (limited to 'gcc/ada/sem_ch6.adb')
-rw-r--r-- | gcc/ada/sem_ch6.adb | 103 |
1 files changed, 75 insertions, 28 deletions
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index a0dad86..29d51a9 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -2219,6 +2219,50 @@ package body Sem_Ch6 is end if; end Analyze_Return_Type; + -------------------------------------------- + -- Analyze_SPARK_Subprogram_Specification -- + -------------------------------------------- + + procedure Analyze_SPARK_Subprogram_Specification (N : Node_Id) is + Spec_Id : constant Entity_Id := Defining_Entity (N); + Formal : Entity_Id; + + begin + if not Comes_From_Source (Spec_Id) then + return; + end if; + + -- The following checks are relevant only when SPARK_Mode is On as + -- these are not standard Ada legality rules. + + if No (SPARK_Pragma (Spec_Id)) + or else Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) /= On + then + return; + end if; + + Formal := First_Formal (Spec_Id); + while Present (Formal) loop + if Ekind (Spec_Id) in E_Function | E_Generic_Function + and then not Is_Function_With_Side_Effects (Spec_Id) + then + -- A function cannot have a parameter of mode IN OUT or OUT + -- (SPARK RM 6.1). + + if Ekind (Formal) in E_In_Out_Parameter + | E_Out_Parameter + then + Error_Msg_Code := GEC_Out_Parameter_In_Function; + Error_Msg_N + ("function cannot have parameter of mode `OUT` or " + & "`IN OUT` in SPARK '[[]']", Formal); + end if; + end if; + + Next_Formal (Formal); + end loop; + end Analyze_SPARK_Subprogram_Specification; + ----------------------------- -- Analyze_Subprogram_Body -- ----------------------------- @@ -4577,6 +4621,29 @@ package body Sem_Ch6 is Analyze_Pragmas_In_Declarations (Body_Id); Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id); + -- Apply SPARK legality checks + + Analyze_SPARK_Subprogram_Specification (Specification (N)); + + -- A function with side-effects shall not be an expression function + -- (SPARK RM 6.1.11(6)). + + if Present (Spec_Id) + and then (Is_Expression_Function (Spec_Id) + or else Is_Expression_Function (Body_Id)) + and then Is_Function_With_Side_Effects (Spec_Id) + then + if From_Aspect_Specification + (Get_Pragma (Spec_Id, Pragma_Side_Effects)) + then + Error_Msg_N ("aspect Side_Effects not allowed" + & " on an expression function", N); + else + Error_Msg_N ("pragma Side_Effects not allowed" + & " on an expression function", N); + end if; + end if; + Set_Actual_Subtypes (N, Current_Scope); -- Add a declaration for the Protection object, renaming declarations @@ -5187,6 +5254,14 @@ package body Sem_Ch6 is Analyze_Aspect_Specifications (N, Designator); end if; + -- The legality of a function specification in SPARK depends on whether + -- the function is a function with or without side-effects. Analyze the + -- pragma in advance if present, before specific SPARK legality checks. + + Analyze_Pragmas_If_Present (N, Pragma_SPARK_Mode); + Analyze_Pragmas_If_Present (N, Pragma_Side_Effects); + Analyze_SPARK_Subprogram_Specification (Specification (N)); + if Scop /= Standard_Standard and then not Is_Child_Unit (Designator) then Set_Categorization_From_Scope (Designator, Scop); @@ -13071,34 +13146,6 @@ package body Sem_Ch6 is Null_Exclusion_Static_Checks (Param_Spec); end if; - -- The following checks are relevant only when SPARK_Mode is on as - -- these are not standard Ada legality rules. - - if SPARK_Mode = On then - if Ekind (Scope (Formal)) in E_Function | E_Generic_Function then - - -- A function cannot have a parameter of mode IN OUT or OUT - -- (SPARK RM 6.1). - - if Ekind (Formal) in E_In_Out_Parameter | E_Out_Parameter then - Error_Msg_N - ("function cannot have parameter of mode `OUT` or " - & "`IN OUT`", Formal); - end if; - - -- A procedure cannot have an effectively volatile formal - -- parameter of mode IN because it behaves as a constant - -- (SPARK RM 7.1.3(4)). - - elsif Ekind (Scope (Formal)) = E_Procedure - and then Ekind (Formal) = E_In_Parameter - and then Is_Effectively_Volatile (Formal) - then - Error_Msg_N - ("formal parameter of mode `IN` cannot be volatile", Formal); - end if; - end if; - -- Deal with aspects on formal parameters. Only Unreferenced is -- supported for the time being. |