aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_ch6.adb
diff options
context:
space:
mode:
Diffstat (limited to 'gcc/ada/sem_ch6.adb')
-rw-r--r--gcc/ada/sem_ch6.adb103
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.