* [COMMITTED] ada: Accept and analyze new aspect Exceptional_Cases
@ 2023-05-23 8:09 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-05-23 8:09 UTC (permalink / raw)
To: gcc-patches; +Cc: Piotr Trojanek
From: Piotr Trojanek <trojanek@adacore.com>
Add new aspect Exceptional_Cases, which is intended for SPARK and
describes in which cases an exception will be raised, and optionally
supply a postcondition that shall be verified in this case.
The implementation is heavily modeled after Subprogram_Variant, which in
turn was heavily modeled after Contract_Cases. Currently the aspect is
only analysed; the code infrastructure required to expand it is prepared
but empty. This is enough for the aspect to be verified by GNATprove.
gcc/ada/
* aspects.ads
(Aspect_Id): Add aspect identifier.
(Aspect_Argument): New aspect accepts an expression.
(Is_Representation_Aspect): New aspect is not a representation
aspect.
(Aspect_Names): Associate name with the new aspect identifier.
(Aspect_Delay): New aspect is never delayed.
* contracts.adb
(Add_Contract_Item): Store new aspect among contract items.
(Analyze_Entry_Or_Subprogram_Contract): Likewise.
(Analyze_Subprogram_Body_Stub_Contract): Likewise.
(Process_Contract_Cases): Expand new aspect, if present.
* contracts.ads
(Analyze_Entry_Or_Subprogram_Body_Contract): Mention new aspect in
spec.
(Analyze_Entry_Or_Subprogram_Contract): Likewise.
* einfo-utils.adb
(Get_Pragma): Allow new aspect to be picked by the backend.
* einfo-utils.ads
(Get_Pragma): Mention new aspect in spec.
* exp_prag.adb
(Expand_Pragma_Exceptional_Cases): Dummy expansion routine.
* exp_prag.ads
(Expand_Pragma_Exceptional_Cases): Add spec for expansion routine.
* inline.adb
(Remove_Aspects_And_Pragmas): Remove aspect from bodies to inline.
* par-prag.adb
(Par.Prag): Accept pragma in the parser, so it will be checked
later.
* sem_ch12.adb
(Implementation of Generic Contracts): Mention new aspect in
comment.
* sem_ch13.adb
(Analyze_Aspect_Specifications): Transform new aspect info a
corresponding pragma.
* sem_prag.adb
(Analyze_Exceptional_Cases_In_Decl_Part): Analyze aspect
expression; heavily inspired by the existing code for analysis of
Subprogram_Variant and exception handlers.
(Analyze_Pragma): Analyze pragma corresponding to the new aspect.
(Is_Non_Significant_Pragma_Reference): Add new pragma to the
table.
* sem_prag.ads
(Assertion_Expression_Pragma): New pragma acts as an assertion
expression, even though it is not currently expanded.
(Analyze_Exceptional_Cases_In_Decl_Part): Add spec.
* sem_util.adb
(Is_Subprogram_Contract_Annotation): Mark new annotation is a
subprogram contract, so the subprogram with it won't be inlined.
* sem_util.ads
(Is_Subprogram_Contract_Annotation): Mention new aspect in
comment.
* sinfo.ads
(Contract_Test_Cases): Mention new aspect in comment.
* snames.ads-tmpl: Add entries for the new name and pragma.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/aspects.ads | 5 +
gcc/ada/contracts.adb | 18 +-
gcc/ada/contracts.ads | 2 +
gcc/ada/einfo-utils.adb | 1 +
gcc/ada/einfo-utils.ads | 1 +
gcc/ada/exp_prag.adb | 41 ++++
gcc/ada/exp_prag.ads | 4 +
gcc/ada/inline.adb | 2 +
gcc/ada/par-prag.adb | 1 +
gcc/ada/sem_ch12.adb | 3 +-
gcc/ada/sem_ch13.adb | 28 ++-
gcc/ada/sem_prag.adb | 429 ++++++++++++++++++++++++++++++++++++++++
gcc/ada/sem_prag.ads | 8 +
gcc/ada/sem_util.adb | 1 +
gcc/ada/sem_util.ads | 1 +
gcc/ada/sinfo.ads | 4 +-
gcc/ada/snames.ads-tmpl | 2 +
17 files changed, 538 insertions(+), 13 deletions(-)
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 36957d466e6..6670b64ca49 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -96,6 +96,7 @@ package Aspects is
Aspect_Dynamic_Predicate,
Aspect_Effective_Reads, -- GNAT
Aspect_Effective_Writes, -- GNAT
+ Aspect_Exceptional_Cases, -- GNAT
Aspect_Extensions_Visible, -- GNAT
Aspect_External_Name,
Aspect_External_Tag,
@@ -389,6 +390,7 @@ package Aspects is
Aspect_Dynamic_Predicate => Expression,
Aspect_Effective_Reads => Optional_Expression,
Aspect_Effective_Writes => Optional_Expression,
+ Aspect_Exceptional_Cases => Expression,
Aspect_Extensions_Visible => Optional_Expression,
Aspect_External_Name => Expression,
Aspect_External_Tag => Expression,
@@ -496,6 +498,7 @@ package Aspects is
Aspect_Dynamic_Predicate => False,
Aspect_Effective_Reads => False,
Aspect_Effective_Writes => False,
+ Aspect_Exceptional_Cases => False,
Aspect_Exclusive_Functions => False,
Aspect_Extensions_Visible => False,
Aspect_External_Name => False,
@@ -653,6 +656,7 @@ package Aspects is
Aspect_Effective_Reads => Name_Effective_Reads,
Aspect_Effective_Writes => Name_Effective_Writes,
Aspect_Elaborate_Body => Name_Elaborate_Body,
+ Aspect_Exceptional_Cases => Name_Exceptional_Cases,
Aspect_Exclusive_Functions => Name_Exclusive_Functions,
Aspect_Export => Name_Export,
Aspect_Extensions_Visible => Name_Extensions_Visible,
@@ -981,6 +985,7 @@ package Aspects is
Aspect_Disable_Controlled => Never_Delay,
Aspect_Effective_Reads => Never_Delay,
Aspect_Effective_Writes => Never_Delay,
+ Aspect_Exceptional_Cases => Never_Delay,
Aspect_Export => Never_Delay,
Aspect_Extensions_Visible => Never_Delay,
Aspect_Ghost => Never_Delay,
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index b0a0ab20228..c85df0fccc8 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -104,8 +104,9 @@ package body Contracts is
procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
-- Expand the contracts of a subprogram body and its correspoding spec (if
-- any). This routine processes all [refined] pre- and postconditions as
- -- well as Contract_Cases, Subprogram_Variant, invariants and predicates.
- -- Body_Id denotes the entity of the subprogram body.
+ -- well as Contract_Cases, Exceptional_Cases, Subprogram_Variant,
+ -- invariants and predicates. Body_Id denotes the entity of the
+ -- subprogram body.
procedure Preanalyze_Condition
(Subp : Entity_Id;
@@ -253,6 +254,7 @@ package body Contracts is
Add_Classification;
elsif Prag_Nam in Name_Contract_Cases
+ | Name_Exceptional_Cases
| Name_Subprogram_Variant
| Name_Test_Case
then
@@ -629,8 +631,9 @@ package body Contracts is
end if;
-- Deal with preconditions, [refined] postconditions, Contract_Cases,
- -- Subprogram_Variant, invariants and predicates associated with body
- -- and its spec. Do not expand the contract of subprogram body stubs.
+ -- Exceptional_Cases, Subprogram_Variant, invariants and predicates
+ -- associated with body and its spec. Do not expand the contract of
+ -- subprogram body stubs.
if Nkind (Body_Decl) = N_Subprogram_Body then
Expand_Subprogram_Contract (Body_Id);
@@ -766,6 +769,9 @@ package body Contracts is
Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
end if;
+ elsif Prag_Nam = Name_Exceptional_Cases then
+ Analyze_Exceptional_Cases_In_Decl_Part (Prag);
+
elsif Prag_Nam = Name_Subprogram_Variant then
Analyze_Subprogram_Variant_In_Decl_Part (Prag);
@@ -1493,6 +1499,7 @@ package body Contracts is
-- The stub acts as its own spec, the applicable pragmas are:
-- Contract_Cases
-- Depends
+ -- Exceptional_Cases
-- Global
-- Postcondition
-- Precondition
@@ -2830,6 +2837,9 @@ package body Contracts is
Decls => Decls,
Stmts => Stmts);
+ elsif Pragma_Name (Prag) = Name_Exceptional_Cases then
+ Expand_Pragma_Exceptional_Cases (Prag);
+
elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
Expand_Pragma_Subprogram_Variant
(Prag => Prag,
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index 0a03d19d431..a53565fe003 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -81,6 +81,7 @@ package Contracts is
--
-- Contract_Cases (stand alone subprogram body)
-- Depends (stand alone subprogram body)
+ -- Exceptional_Cases (stand alone subprogram body)
-- Global (stand alone subprogram body)
-- Postcondition (stand alone subprogram body)
-- Precondition (stand alone subprogram body)
@@ -99,6 +100,7 @@ package Contracts is
--
-- Contract_Cases
-- Depends
+ -- Exceptional_Cases
-- Global
-- Postcondition
-- Precondition
diff --git a/gcc/ada/einfo-utils.adb b/gcc/ada/einfo-utils.adb
index 5916188fa84..fa28a9e0100 100644
--- a/gcc/ada/einfo-utils.adb
+++ b/gcc/ada/einfo-utils.adb
@@ -1018,6 +1018,7 @@ package body Einfo.Utils is
Is_CTC : constant Boolean :=
Id = Pragma_Contract_Cases or else
+ Id = Pragma_Exceptional_Cases or else
Id = Pragma_Subprogram_Variant or else
Id = Pragma_Test_Case;
diff --git a/gcc/ada/einfo-utils.ads b/gcc/ada/einfo-utils.ads
index 174994647bc..e8055020a67 100644
--- a/gcc/ada/einfo-utils.ads
+++ b/gcc/ada/einfo-utils.ads
@@ -447,6 +447,7 @@ package Einfo.Utils is
-- Depends
-- Effective_Reads
-- Effective_Writes
+ -- Exceptional_Cases
-- Global
-- Initial_Condition
-- Initializes
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index c6b3bed5425..e660196c0f1 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -1978,6 +1978,47 @@ package body Exp_Prag is
In_Assertion_Expr := In_Assertion_Expr - 1;
end Expand_Pragma_Contract_Cases;
+ -------------------------------------
+ -- Expand_Pragma_Exceptional_Cases --
+ -------------------------------------
+
+ -- Aspect Exceptional_Cases shoule be expanded in the following manner:
+
+ -- Original declaration
+
+ -- procedure P (...) with
+ -- Exceptional_Cases =>
+ -- (Exp_1 => True,
+ -- Exp_2 => Post_4);
+
+ -- Expanded body
+
+ -- procedure P (...) is
+ -- begin
+ -- -- normal body of of P
+ -- declare
+ -- ...
+ -- end;
+ --
+ -- exception
+ -- when Exp1 =>
+ -- pragma Assert (True);
+ -- raise;
+ -- when E : Exp2 =>
+ -- pragma Assert (Post_4);
+ -- raise;
+ -- when others =>
+ -- pragma Assert (False);
+ -- raise;
+ -- end P;
+
+ procedure Expand_Pragma_Exceptional_Cases (Prag : Node_Id) is
+ begin
+ -- Currently we don't expand this pragma
+
+ Rewrite (Prag, Make_Null_Statement (Sloc (Prag)));
+ end Expand_Pragma_Exceptional_Cases;
+
---------------------------------------
-- Expand_Pragma_Import_Or_Interface --
---------------------------------------
diff --git a/gcc/ada/exp_prag.ads b/gcc/ada/exp_prag.ads
index 27c537c46ca..9f810dab227 100644
--- a/gcc/ada/exp_prag.ads
+++ b/gcc/ada/exp_prag.ads
@@ -42,6 +42,10 @@ package Exp_Prag is
-- Subp_Id's body. All generated code is added to list Stmts. If Stmts is
-- No_List on entry, a new list is created.
+ procedure Expand_Pragma_Exceptional_Cases (Prag : Node_Id);
+ -- Given pragma Exceptional_Cases Prag, create the circuitry needed to
+ -- catch exceptions and evaluate consequence expressions.
+
procedure Expand_Pragma_Initial_Condition
(Pack_Id : Entity_Id;
N : Node_Id);
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index b2ff7c9e405..b7dafde9cf9 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -315,6 +315,7 @@ package body Inline is
-- Contract_Cases
-- Global
-- Depends
+ -- Exceptional_Cases
-- Postcondition
-- Precondition
-- Refined_Global
@@ -5165,6 +5166,7 @@ package body Inline is
and then Chars (Item_Id) in Name_Contract_Cases
| Name_Global
| Name_Depends
+ | Name_Exceptional_Cases
| Name_Postcondition
| Name_Precondition
| Name_Refined_Global
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 4a3517d2297..ac50c846bf9 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1371,6 +1371,7 @@ begin
| Pragma_Elaboration_Checks
| Pragma_Eliminate
| Pragma_Enable_Atomic_Synchronization
+ | Pragma_Exceptional_Cases
| Pragma_Export
| Pragma_Export_Function
| Pragma_Export_Object
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 91a1fad444c..b8cd16080fe 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -263,7 +263,8 @@ package body Sem_Ch12 is
-- package subprogram [body]
-- Abstract_State Contract_Cases
-- Initial_Condition Depends
- -- Initializes Extensions_Visible
+ -- Initializes Exceptional_Cases
+ -- Extensions_Visible
-- Global
-- package body Post
-- Refined_State Post_Class
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 983f877e001..d40c70f6ee4 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1410,6 +1410,7 @@ package body Sem_Ch13 is
-- Attach_Handler
-- Contract_Cases
-- Depends
+ -- Exceptional_Cases
-- Ghost
-- Global
-- Initial_Condition
@@ -1666,10 +1667,10 @@ package body Sem_Ch13 is
-- analyzed right now.
-- Note that there is a special handling for Pre, Post, Test_Case,
- -- Contract_Cases and Subprogram_Variant aspects. In these cases, we do
- -- not have to worry about delay issues, since the pragmas themselves
- -- deal with delay of visibility for the expression analysis. Thus, we
- -- just insert the pragma after the node N.
+ -- Contract_Cases, Exceptional_Cases and Subprogram_Variant aspects.
+ -- In these cases, we do not have to worry about delay issues, since the
+ -- pragmas themselves deal with delay of visibility for the expression
+ -- analysis. Thus, we just insert the pragma after the node N.
-- Loop through aspects
@@ -4287,8 +4288,9 @@ package body Sem_Ch13 is
-- Case 4: Aspects requiring special handling
- -- Pre/Post/Test_Case/Contract_Cases/Subprogram_Variant whose
- -- corresponding pragmas take care of the delay.
+ -- Pre/Post/Test_Case/Contract_Cases/Exceptional_Cases and
+ -- Subprogram_Variant whose corresponding pragmas take care
+ -- of the delay.
-- Pre/Post
@@ -4520,6 +4522,19 @@ package body Sem_Ch13 is
Insert_Pragma (Aitem);
goto Continue;
+ -- Exceptional_Cases
+
+ when Aspect_Exceptional_Cases =>
+ Aitem := Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Exceptional_Cases);
+
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
-- Subprogram_Variant
when Aspect_Subprogram_Variant =>
@@ -11280,6 +11295,7 @@ package body Sem_Ch13 is
| Aspect_Depends
| Aspect_Dimension
| Aspect_Dimension_System
+ | Aspect_Exceptional_Cases
| Aspect_Effective_Reads
| Aspect_Effective_Writes
| Aspect_Extensions_Visible
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d80f78f4865..963c6dea238 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2104,6 +2104,298 @@ package body Sem_Prag is
Set_Is_Analyzed_Pragma (N);
end Analyze_Depends_In_Decl_Part;
+ --------------------------------------------
+ -- Analyze_Exceptional_Cases_In_Decl_Part --
+ --------------------------------------------
+
+ -- WARNING: This routine manages Ghost regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- Ghost mode.
+
+ procedure Analyze_Exceptional_Cases_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
+
+ procedure Analyze_Exceptional_Contract (Exceptional_Contract : Node_Id);
+ -- Verify the legality of a single exceptional contract
+
+ procedure Check_Duplication (Id : Node_Id; Contracts : List_Id);
+ -- Iterate through the identifiers in each contract to find duplicates
+
+ ----------------------------------
+ -- Analyze_Exceptional_Contract --
+ ----------------------------------
+
+ procedure Analyze_Exceptional_Contract (Exceptional_Contract : Node_Id)
+ is
+ Exception_Choice : Node_Id;
+ Consequence : Node_Id;
+ Errors : Nat;
+
+ begin
+ if Nkind (Exceptional_Contract) /= N_Component_Association then
+ Error_Msg_N
+ ("wrong syntax in exceptional contract", Exceptional_Contract);
+ return;
+ end if;
+
+ Exception_Choice := First (Choices (Exceptional_Contract));
+ Consequence := Expression (Exceptional_Contract);
+
+ while Present (Exception_Choice) loop
+ if Nkind (Exception_Choice) = N_Others_Choice then
+ if Present (Next (Exception_Choice))
+ or else Present (Next (Exceptional_Contract))
+ or else Present (Prev (Exception_Choice))
+ then
+ Error_Msg_N
+ ("OTHERS must appear alone and last", Exception_Choice);
+ end if;
+
+ else
+ Analyze (Exception_Choice);
+
+ if Is_Entity_Name (Exception_Choice)
+ and then Ekind (Entity (Exception_Choice)) = E_Exception
+ then
+ if Present (Renamed_Entity (Entity (Exception_Choice)))
+ and then Entity (Exception_Choice) = Standard_Numeric_Error
+ then
+ Check_Restriction
+ (No_Obsolescent_Features, Exception_Choice);
+
+ if Warn_On_Obsolescent_Feature then
+ Error_Msg_N
+ ("Numeric_Error is an obsolescent feature " &
+ "(RM J.6(1))?j?",
+ Exception_Choice);
+ Error_Msg_N
+ ("\use Constraint_Error instead?j?",
+ Exception_Choice);
+ end if;
+ end if;
+
+ Check_Duplication
+ (Exception_Choice, List_Containing (Exceptional_Contract));
+
+ -- Check for exception declared within generic formal
+ -- package (which is illegal, see RM 11.2(8)).
+
+ declare
+ Ent : Entity_Id := Entity (Exception_Choice);
+ Scop : Entity_Id;
+
+ begin
+ if Present (Renamed_Entity (Ent)) then
+ Ent := Renamed_Entity (Ent);
+ end if;
+
+ Scop := Scope (Ent);
+ while Scop /= Standard_Standard
+ and then Ekind (Scop) = E_Package
+ loop
+ if Nkind (Declaration_Node (Scop)) =
+ N_Package_Specification
+ and then
+ Nkind (Original_Node (Parent
+ (Declaration_Node (Scop)))) =
+ N_Formal_Package_Declaration
+ then
+ Error_Msg_NE
+ ("exception& is declared in generic formal "
+ & "package", Exception_Choice, Ent);
+ Error_Msg_N
+ ("\and therefore cannot appear in contract "
+ & "(RM 11.2(8))", Exception_Choice);
+ exit;
+
+ -- If the exception is declared in an inner instance,
+ -- nothing else to check.
+
+ elsif Is_Generic_Instance (Scop) then
+ exit;
+ end if;
+
+ Scop := Scope (Scop);
+ end loop;
+ end;
+ else
+ Error_Msg_N ("exception name expected", Exception_Choice);
+ end if;
+ end if;
+
+ Next (Exception_Choice);
+ end loop;
+
+ -- Now analyze the expressions of this contract
+
+ Errors := Serious_Errors_Detected;
+
+ -- Preanalyze_Assert_Expression, but without enforcing any of the two
+ -- acceptable types.
+
+ Preanalyze_Assert_Expression (Consequence, Any_Boolean);
+
+ -- Emit a clarification message when the consequence contains at
+ -- least one undefined reference, possibly due to contract freezing.
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Consequence)
+ then
+ Contract_Freeze_Error (Spec_Id, Freeze_Id);
+ end if;
+ end Analyze_Exceptional_Contract;
+
+ -----------------------
+ -- Check_Duplication --
+ -----------------------
+
+ procedure Check_Duplication (Id : Node_Id; Contracts : List_Id) is
+ Contract : Node_Id;
+ Id1 : Node_Id;
+ Id_Entity : Entity_Id := Entity (Id);
+
+ begin
+ if Present (Renamed_Entity (Id_Entity)) then
+ Id_Entity := Renamed_Entity (Id_Entity);
+ end if;
+
+ Contract := First (Contracts);
+ while Present (Contract) loop
+ Id1 := First (Choices (Contract));
+ while Present (Id1) loop
+
+ -- Only check against the exception choices which precede
+ -- Id in the contract, since the ones that follow Id have not
+ -- been analyzed yet and will be checked in a subsequent call.
+
+ if Id = Id1 then
+ return;
+
+ -- Duplication both simple and via a renaming across different
+ -- exceptional contracts is illegal.
+
+ elsif Nkind (Id1) /= N_Others_Choice
+ and then
+ (Id_Entity = Entity (Id1)
+ or else Id_Entity = Renamed_Entity (Entity (Id1)))
+ and then Contract /= Parent (Id)
+ then
+ Error_Msg_Sloc := Sloc (Id1);
+ Error_Msg_NE ("exception choice duplicates &#", Id, Id1);
+ end if;
+
+ Next (Id1);
+ end loop;
+
+ Next (Contract);
+ end loop;
+ end Check_Duplication;
+
+ -- Local variables
+
+ Exceptional_Contracts : constant Node_Id :=
+ Expression (Get_Argument (N, Spec_Id));
+
+ Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
+ Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
+ -- Save the Ghost-related attributes to restore on exit
+
+ Exceptional_Contract : Node_Id;
+ Restore_Scope : Boolean := False;
+
+ -- Start of processing for Analyze_Subprogram_Variant_In_Decl_Part
+
+ begin
+ -- Do not analyze the pragma multiple times
+
+ if Is_Analyzed_Pragma (N) then
+ return;
+ end if;
+
+ -- Set the Ghost mode in effect from the pragma. Due to the delayed
+ -- analysis of the pragma, the Ghost mode at point of declaration and
+ -- point of analysis may not necessarily be the same. Use the mode in
+ -- effect at the point of declaration.
+
+ Set_Ghost_Mode (N);
+
+ -- Single and multiple contracts must appear in aggregate form. If this
+ -- is not the case, then either the parser of the analysis of the pragma
+ -- failed to produce an aggregate, e.g. when the contract is "null" or a
+ -- "(null record)".
+
+ pragma Assert
+ (if Nkind (Exceptional_Contracts) = N_Aggregate
+ then Null_Record_Present (Exceptional_Contracts)
+ xor (Present (Component_Associations (Exceptional_Contracts))
+ or
+ Present (Expressions (Exceptional_Contracts)))
+ else Nkind (Exceptional_Contracts) = N_Null);
+
+ -- Only clauses of the following form are allowed:
+ --
+ -- exceptional_contract ::=
+ -- [choice_parameter_specification:]
+ -- exception_choice {'|' exception_choice} => consequence
+ --
+ -- where
+ --
+ -- consequence ::= Boolean_expression
+
+ if Nkind (Exceptional_Contracts) = N_Aggregate
+ and then Present (Component_Associations (Exceptional_Contracts))
+ and then No (Expressions (Exceptional_Contracts))
+ then
+
+ -- Check that the expression is a proper aggregate (no parentheses)
+
+ if Paren_Count (Exceptional_Contracts) /= 0 then
+ Error_Msg_F -- CODEFIX
+ ("redundant parentheses", Exceptional_Contracts);
+ end if;
+
+ -- Ensure that the formal parameters are visible when analyzing all
+ -- clauses. This falls out of the general rule of aspects pertaining
+ -- to subprogram declarations.
+
+ if not In_Open_Scopes (Spec_Id) then
+ Restore_Scope := True;
+ Push_Scope (Spec_Id);
+
+ if Is_Generic_Subprogram (Spec_Id) then
+ Install_Generic_Formals (Spec_Id);
+ else
+ Install_Formals (Spec_Id);
+ end if;
+ end if;
+
+ Exceptional_Contract :=
+ First (Component_Associations (Exceptional_Contracts));
+ while Present (Exceptional_Contract) loop
+ Analyze_Exceptional_Contract (Exceptional_Contract);
+ Next (Exceptional_Contract);
+ end loop;
+
+ if Restore_Scope then
+ End_Scope;
+ end if;
+
+ -- Otherwise the pragma is illegal
+
+ else
+ Error_Msg_N ("wrong syntax for exceptional cases", N);
+ end if;
+
+ Set_Is_Analyzed_Pragma (N);
+
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ end Analyze_Exceptional_Cases_In_Decl_Part;
+
--------------------------------------------
-- Analyze_External_Property_In_Decl_Part --
--------------------------------------------
@@ -16280,6 +16572,142 @@ package body Sem_Prag is
GNAT_Pragma;
Process_Disable_Enable_Atomic_Sync (Name_Unsuppress);
+ -----------------------
+ -- Exceptional_Cases --
+ -----------------------
+
+ -- pragma Exceptional_Cases ( EXCEPTIONAL_CONTRACT_LIST );
+
+ -- EXCEPTIONAL_CONTRACT_LIST ::=
+ -- ( EXCEPTIONAL_CONTRACT {, EXCEPTIONAL_CONTRACT })
+
+ -- EXCEPTIONAL_CONTRACT ::=
+ -- EXCEPTION_CHOICE {'|' EXCEPTION_CHOICE} => CONSEQUENCE
+ --
+ -- where
+ --
+ -- CONSEQUENCE ::= boolean_EXPRESSION
+
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expressions in:
+
+ -- Analyze_Exceptional_Cases_In_Decl_Part
+
+ -- * Expansion - The annotation is expanded during the expansion of
+ -- the related subprogram [body] contract as performed in:
+
+ -- Expand_Subprogram_Contract
+
+ -- * Template - The annotation utilizes the generic template of the
+ -- related subprogram [body] when it is:
+
+ -- aspect on subprogram declaration
+ -- aspect on stand-alone subprogram body
+ -- pragma on stand-alone subprogram body
+
+ -- The annotation must prepare its own template when it is:
+
+ -- pragma on subprogram declaration
+
+ -- * Globals - Capture of global references must occur after full
+ -- analysis.
+
+ -- * Instance - The annotation is instantiated automatically when
+ -- the related generic subprogram [body] is instantiated except for
+ -- the "pragma on subprogram declaration" case. In that scenario
+ -- the annotation must instantiate itself.
+
+ when Pragma_Exceptional_Cases => Exceptional_Cases : declare
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id;
+ Subp_Spec : Node_Id;
+
+ begin
+ GNAT_Pragma;
+ Check_No_Identifiers;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Exceptional_Cases
+ -- must be associated with a subprogram declaration or a body that
+ -- acts as a spec.
+
+ Subp_Decl :=
+ Find_Related_Declaration_Or_Body (N, Do_Checks => True);
+
+ -- Generic subprogram
+
+ if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ null;
+
+ -- Body acts as spec
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body
+ and then No (Corresponding_Spec (Subp_Decl))
+ then
+ null;
+
+ -- Body stub acts as spec
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
+ then
+ null;
+
+ -- Subprogram
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ Subp_Spec := Specification (Subp_Decl);
+
+ -- Pragma Exceptional_Cases is forbidden on null procedures,
+ -- as this may lead to potential ambiguities in behavior when
+ -- interface null procedures are involved. Also, it just
+ -- wouldn't make sense, because null procedures do not raise
+ -- exceptions.
+
+ if Nkind (Subp_Spec) = N_Procedure_Specification
+ and then Null_Present (Subp_Spec)
+ then
+ Error_Msg_N (Fix_Error
+ ("pragma % cannot apply to null procedure"), N);
+ return;
+ end if;
+
+ else
+ Pragma_Misplaced;
+ end if;
+
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
+
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Spec_Id);
+ Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
+
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Subprogram_Variant_In_Decl_Part.
+
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+
+ -- Fully analyze the pragma when it appears inside a subprogram
+ -- body because it cannot benefit from forward references.
+
+ if Nkind (Subp_Decl) in N_Subprogram_Body
+ | N_Subprogram_Body_Stub
+ then
+ -- The legality checks of pragma Subprogram_Variant are
+ -- affected by the SPARK mode in effect and the volatility
+ -- of the context. Analyze all pragmas in a specific order.
+
+ Analyze_If_Present (Pragma_SPARK_Mode);
+ Analyze_If_Present (Pragma_Volatile_Function);
+ Analyze_Subprogram_Variant_In_Decl_Part (N);
+ end if;
+ end Exceptional_Cases;
+
------------
-- Export --
------------
@@ -31580,6 +32008,7 @@ package body Sem_Prag is
Pragma_Elaboration_Checks => 0,
Pragma_Eliminate => 0,
Pragma_Enable_Atomic_Synchronization => 0,
+ Pragma_Exceptional_Cases => -1,
Pragma_Export => -1,
Pragma_Export_Function => -1,
Pragma_Export_Object => -1,
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index fa7e7073f5a..993ff7a986b 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -138,6 +138,7 @@ package Sem_Prag is
Pragma_Compile_Time_Error => True,
Pragma_Contract_Cases => True,
Pragma_Default_Initial_Condition => True,
+ Pragma_Exceptional_Cases => True,
Pragma_Initial_Condition => True,
Pragma_Invariant => True,
Pragma_Loop_Invariant => True,
@@ -247,6 +248,13 @@ package Sem_Prag is
-- Perform full analysis of delayed pragma Depends. This routine is also
-- capable of performing basic analysis of pragma Refined_Depends.
+ procedure Analyze_Exceptional_Cases_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of delayed pragma Exceptional_Cases. Freeze_Id is
+ -- the entity of [generic] package body or [generic] subprogram body which
+ -- caused "freezing" of the related contract where the pragma resides.
+
procedure Analyze_External_Property_In_Decl_Part
(N : Node_Id;
Expr_Val : out Boolean);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 9a0197cb45c..b28f2899894 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -20576,6 +20576,7 @@ package body Sem_Util is
return Nam = Name_Contract_Cases
or else Nam = Name_Depends
+ or else Nam = Name_Exceptional_Cases
or else Nam = Name_Extensions_Visible
or else Nam = Name_Global
or else Nam = Name_Post
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 253d1dadeee..4028d370823 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -2343,6 +2343,7 @@ package Sem_Util is
-- following subprogram contract annotations:
-- Contract_Cases
-- Depends
+ -- Exceptional_Cases
-- Extensions_Visible
-- Global
-- Post
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index b0ac6f900ed..e6a27e62cc1 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -7963,8 +7963,8 @@ package Sinfo is
-- operation) are also in this list.
-- Contract_Test_Cases contains a collection of pragmas that correspond
- -- to aspects/pragmas Contract_Cases, Test_Case and Subprogram_Variant.
- -- The ordering in the list is in LIFO fashion.
+ -- to aspects/pragmas Contract_Cases, Exceptional_Cases, Test_Case and
+ -- Subprogram_Variant. The ordering in the list is in LIFO fashion.
-- Classifications contains pragmas that either declare, categorize, or
-- establish dependencies between subprogram or package inputs and
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index cf2efbbbb63..9868d97b740 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -552,6 +552,7 @@ package Snames is
Name_Elaborate : constant Name_Id := N + $; -- Ada 83
Name_Elaborate_All : constant Name_Id := N + $;
Name_Elaborate_Body : constant Name_Id := N + $;
+ Name_Exceptional_Cases : constant Name_Id := N + $; -- GNAT
Name_Export : constant Name_Id := N + $;
Name_Export_Function : constant Name_Id := N + $; -- GNAT
Name_Export_Object : constant Name_Id := N + $; -- GNAT
@@ -1848,6 +1849,7 @@ package Snames is
Pragma_Elaborate,
Pragma_Elaborate_All,
Pragma_Elaborate_Body,
+ Pragma_Exceptional_Cases,
Pragma_Export,
Pragma_Export_Function,
Pragma_Export_Object,
--
2.40.0
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-05-23 8:09 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-05-23 8:09 [COMMITTED] ada: Accept and analyze new aspect Exceptional_Cases Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).