[COMMITTED] ada: Restrict use of formal parameters within exceptional cases
Checks
Commit Message
From: Piotr Trojanek <trojanek@adacore.com>
Restrict references to formal parameters within the new SPARK aspect
Exceptional_Cases and allow occurrences of 'Old in this aspect.
gcc/ada/
* sem_attr.adb
(Analyze_Attribute_Old_Result): Allow uses of 'Old and 'Result within
the new aspect.
* sem_res.adb
(Within_Exceptional_Cases_Consequence): New utility routine.
(Resolve_Entity_Name): Restrict use of formal parameters within the
new aspect.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_attr.adb | 8 ++++++
gcc/ada/sem_res.adb | 61 ++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 69 insertions(+)
@@ -1423,6 +1423,14 @@ package body Sem_Attr is
elsif Prag_Nam = Name_Contract_Cases then
Check_Placement_In_Contract_Cases (Prag);
+ -- Attributes 'Old and 'Result are allowed to appear in
+ -- consequence of aspect or pragma Exceptional_Cases. We already
+ -- examined the exception_choice part of contract syntax, so we
+ -- can accept all remaining occurrences within the pragma.
+
+ elsif Prag_Nam = Name_Exceptional_Cases then
+ null;
+
-- Attribute 'Result is allowed to appear in aspect or pragma
-- [Refined_]Depends (SPARK RM 6.1.5(11)).
@@ -7832,6 +7832,11 @@ package body Sem_Res is
-- Determine whether Expr is part of an N_Attribute_Reference
-- expression.
+ function Within_Exceptional_Cases_Consequence
+ (Expr : Node_Id)
+ return Boolean;
+ -- Determine whether Expr is part of an Exceptional_Cases consequence
+
----------------------------------------
-- Is_Assignment_Or_Object_Expression --
----------------------------------------
@@ -7896,6 +7901,39 @@ package body Sem_Res is
return False;
end Is_Attribute_Expression;
+ ------------------------------------------
+ -- Within_Exceptional_Cases_Consequence --
+ ------------------------------------------
+
+ function Within_Exceptional_Cases_Consequence
+ (Expr : Node_Id)
+ return Boolean
+ is
+ Context : Node_Id := Parent (Expr);
+ begin
+ while Present (Context) loop
+ if Nkind (Context) = N_Pragma then
+
+ -- In Exceptional_Cases references to formal parameters are
+ -- only allowed within consequences, so it is enough to
+ -- recognize the pragma itself.
+
+ if Get_Pragma_Id (Context) = Pragma_Exceptional_Cases then
+ return True;
+ end if;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Context) then
+ return False;
+ end if;
+
+ Context := Parent (Context);
+ end loop;
+
+ return False;
+ end Within_Exceptional_Cases_Consequence;
+
-- Local variables
E : constant Entity_Id := Entity (N);
@@ -8040,6 +8078,29 @@ package body Sem_Res is
& "(SPARK RM 7.1.3(10))", N);
end if;
+ -- Parameters of modes OUT or IN OUT of the subprogram shall not
+ -- occur in the consequences of an exceptional contract unless
+ -- they either are of a by-reference type or occur in the prefix
+ -- of a reference to the 'Old attribute.
+
+ if Ekind (E) in E_Out_Parameter | E_In_Out_Parameter
+ and then Within_Exceptional_Cases_Consequence (N)
+ and then not Is_Attribute_Old (Parent (N))
+ and then not Is_By_Reference_Type (Etype (E))
+ then
+ if Ekind (E) = E_Out_Parameter then
+ Error_Msg_N
+ ("formal parameter of mode `OUT` cannot appear " &
+ "in consequence of Exceptional_Cases", N);
+ else
+ Error_Msg_N
+ ("formal parameter of mode `IN OUT` cannot appear " &
+ "in consequence of Exceptional_Cases", N);
+ end if;
+ Error_Msg_N
+ ("\only parameters of by-reference types are allowed", N);
+ end if;
+
-- Check for possible elaboration issues with respect to reads of
-- variables. The act of renaming the variable is not considered a
-- read as it simply establishes an alias.