From: Piotr Trojanek <troja...@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(+) diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index bc4e3cf019e..0cfc2da29dd 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -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)). diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 3b7d821158c..4e49a0a1473 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -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. -- 2.40.0