diff options
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. |