diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2023-02-08 00:54:06 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-25 09:44:14 +0200 |
commit | 7b67bfab289d7f50beed51ca72717be5a8154f3b (patch) | |
tree | 161df46da1c463430cad96fa6b9a05e6e47edc16 | |
parent | 53bd7622de70a4ca4a25cac953da3be2a24bc3c8 (diff) | |
download | gcc-7b67bfab289d7f50beed51ca72717be5a8154f3b.zip gcc-7b67bfab289d7f50beed51ca72717be5a8154f3b.tar.gz gcc-7b67bfab289d7f50beed51ca72717be5a8154f3b.tar.bz2 |
ada: Restrict use of formal parameters within exceptional cases
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.
-rw-r--r-- | gcc/ada/sem_attr.adb | 8 | ||||
-rw-r--r-- | gcc/ada/sem_res.adb | 61 |
2 files changed, 69 insertions, 0 deletions
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index bc4e3cf..0cfc2da2 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 3b7d821..4e49a0a 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. |