===================================================================
@@ -1499,7 +1499,17 @@
begin
CTC := Spec_CTC_List (Contract (S));
while Present (CTC) loop
- if String_Equal (Name, Get_Name_From_CTC_Pragma (CTC)) then
+
+ -- Omit pragma Contract_Cases because it does not introduce
+ -- a unique case name and it does not follow the syntax of
+ -- Contract_Case and Test_Case.
+
+ if Pragma_Name (CTC) = Name_Contract_Cases then
+ null;
+
+ elsif String_Equal
+ (Name, Get_Name_From_CTC_Pragma (CTC))
+ then
Error_Msg_Sloc := Sloc (CTC);
Error_Pragma ("name for pragma% is already used#");
end if;
@@ -7705,6 +7715,166 @@
when Pragma_Contract_Case =>
Check_Contract_Or_Test_Case;
+ --------------------
+ -- Contract_Cases --
+ --------------------
+
+ -- pragma Contract_Cases (POST_CASE_LIST);
+
+ -- POST_CASE_LIST ::= POST_CASE {, POST_CASE}
+
+ -- POST_CASE ::= CASE_GUARD => CONSEQUENCE
+
+ -- CASE_GUARD ::= boolean_EXPRESSION | others
+
+ -- CONSEQUENCE ::= boolean_EXPRESSION
+
+ when Pragma_Contract_Cases => Contract_Cases : declare
+ procedure Chain_Contract_Cases (Subp_Decl : Node_Id);
+ -- Chain pragma Contract_Cases to the contract of a subprogram.
+ -- Subp_Decl is the declaration of the subprogram.
+
+ --------------------------
+ -- Chain_Contract_Cases --
+ --------------------------
+
+ procedure Chain_Contract_Cases (Subp_Decl : Node_Id) is
+ Subp : constant Entity_Id :=
+ Defining_Unit_Name (Specification (Subp_Decl));
+ CTC : Node_Id;
+
+ begin
+ CTC := Spec_CTC_List (Contract (Subp));
+ while Present (CTC) loop
+ if Chars (Pragma_Identifier (CTC)) = Pname then
+ Error_Pragma ("pragma % already in use");
+ return;
+ end if;
+
+ CTC := Next_Pragma (CTC);
+ end loop;
+
+ -- Prepend pragma Contract_Cases to the contract
+
+ Set_Next_Pragma (N, Spec_CTC_List (Contract (Subp)));
+ Set_Spec_CTC_List (Contract (Subp), N);
+ end Chain_Contract_Cases;
+
+ -- Local variables
+
+ Case_Guard : Node_Id;
+ Decl : Node_Id;
+ Extra : Node_Id;
+ Others_Seen : Boolean := False;
+ Post_Case : Node_Id;
+ Subp_Decl : Node_Id;
+
+ -- Start of processing for Contract_Cases
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Completely ignore if disabled
+
+ if Check_Disabled (Pname) then
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
+ return;
+ end if;
+
+ -- Check the placement of the pragma
+
+ if not Is_List_Member (N) then
+ Pragma_Misplaced;
+ end if;
+
+ -- Pragma Contract_Cases must be associated with a subprogram
+
+ Decl := N;
+ while Present (Prev (Decl)) loop
+ Decl := Prev (Decl);
+
+ if Nkind (Decl) in N_Generic_Declaration then
+ Subp_Decl := Decl;
+ else
+ Subp_Decl := Original_Node (Decl);
+ end if;
+
+ -- Skip prior pragmas
+
+ if Nkind (Subp_Decl) = N_Pragma then
+ null;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Subp_Decl) then
+ null;
+
+ -- We have found the related subprogram
+
+ elsif Nkind_In (Subp_Decl, N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
+ exit;
+
+ else
+ Pragma_Misplaced;
+ end if;
+ end loop;
+
+ -- All post cases must appear as an aggregate
+
+ if Nkind (Expression (Arg1)) /= N_Aggregate then
+ Error_Pragma ("wrong syntax for pragma %");
+ return;
+ end if;
+
+ -- Verify the legality of individual post cases
+
+ Post_Case := First (Component_Associations (Expression (Arg1)));
+ while Present (Post_Case) loop
+ if Nkind (Post_Case) /= N_Component_Association then
+ Error_Pragma_Arg ("wrong syntax in post case", Post_Case);
+ return;
+ end if;
+
+ Case_Guard := First (Choices (Post_Case));
+
+ -- Each post case must have exactly on case guard
+
+ Extra := Next (Case_Guard);
+ if Present (Extra) then
+ Error_Pragma_Arg
+ ("post case may have only one case guard", Extra);
+ return;
+ end if;
+
+ -- Check the placement of "others" (if available)
+
+ if Nkind (Case_Guard) = N_Others_Choice then
+ if Others_Seen then
+ Error_Pragma_Arg
+ ("only one others choice allowed in pragma %",
+ Case_Guard);
+ return;
+ else
+ Others_Seen := True;
+ end if;
+
+ elsif Others_Seen then
+ Error_Pragma_Arg
+ ("others must be the last choice in pragma %", N);
+ return;
+ end if;
+
+ Next (Post_Case);
+ end loop;
+
+ Chain_Contract_Cases (Subp_Decl);
+ end Contract_Cases;
+
----------------
-- Controlled --
----------------
@@ -15468,6 +15638,7 @@
Pragma_Complex_Representation => 0,
Pragma_Component_Alignment => -1,
Pragma_Contract_Case => -1,
+ Pragma_Contract_Cases => -1,
Pragma_Controlled => 0,
Pragma_Convention => 0,
Pragma_Convention_Identifier => 0,
===================================================================
@@ -252,6 +252,7 @@
Aspect_Component_Size => Aspect_Component_Size,
Aspect_Constant_Indexing => Aspect_Constant_Indexing,
Aspect_Contract_Case => Aspect_Contract_Case,
+ Aspect_Contract_Cases => Aspect_Contract_Cases,
Aspect_Convention => Aspect_Convention,
Aspect_CPU => Aspect_CPU,
Aspect_Default_Component_Value => Aspect_Default_Component_Value,
===================================================================
@@ -81,6 +81,7 @@
Aspect_Component_Size,
Aspect_Constant_Indexing,
Aspect_Contract_Case, -- GNAT
+ Aspect_Contract_Cases, -- GNAT
Aspect_Convention,
Aspect_CPU,
Aspect_Default_Component_Value,
@@ -223,6 +224,7 @@
Aspect_Ada_2012 => True,
Aspect_Compiler_Unit => True,
Aspect_Contract_Case => True,
+ Aspect_Contract_Cases => True,
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Favor_Top_Level => True,
@@ -254,9 +256,10 @@
-- the same aspect attached to the same declaration are allowed.
No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
- (Aspect_Contract_Case => False,
- Aspect_Test_Case => False,
- others => True);
+ (Aspect_Contract_Case => False,
+ Aspect_Contract_Cases => False,
+ Aspect_Test_Case => False,
+ others => True);
-- The following array indicates type aspects that are inherited and apply
-- to the class-wide type as well.
@@ -309,6 +312,7 @@
Aspect_Component_Size => Expression,
Aspect_Constant_Indexing => Name,
Aspect_Contract_Case => Expression,
+ Aspect_Contract_Cases => Expression,
Aspect_Convention => Name,
Aspect_CPU => Expression,
Aspect_Default_Component_Value => Expression,
@@ -379,6 +383,7 @@
Aspect_Component_Size => Name_Component_Size,
Aspect_Constant_Indexing => Name_Constant_Indexing,
Aspect_Contract_Case => Name_Contract_Case,
+ Aspect_Contract_Cases => Name_Contract_Cases,
Aspect_Convention => Name_Convention,
Aspect_CPU => Name_CPU,
Aspect_Default_Iterator => Name_Default_Iterator,
===================================================================
@@ -11139,6 +11139,11 @@
-- under the same visibility conditions as for other invariant checks,
-- the type invariant must be applied to the returned value.
+ procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id);
+ -- Given pragma Contract_Cases CCs, create the circuitry needed to
+ -- evaluate case guards and trigger consequence expressions. Subp_Id
+ -- denotes the related subprogram.
+
function Grab_CC return Node_Id;
-- Prag contains an analyzed contract case pragma. This function copies
-- relevant components of the pragma, creates the corresponding Check
@@ -11206,6 +11211,459 @@
end if;
end Check_Access_Invariants;
+ ---------------------------
+ -- Expand_Contract_Cases --
+ ---------------------------
+
+ -- Pragma Contract_Cases is expanded in the following manner:
+
+ -- subprogram S is
+ -- Flag_1 : Boolean := False;
+ -- . . .
+ -- Flag_N : Boolean := False;
+ -- Flag_N+1 : Boolean := False; -- when "others" present
+ -- Count : Natural := 0;
+
+ -- <preconditions (if any)>
+
+ -- if Case_Guard_1 then
+ -- Flag_1 := True;
+ -- Count := Count + 1;
+ -- end if;
+ -- . . .
+ -- if Case_Guard_N then
+ -- Flag_N := True;
+ -- Count := Count + 1;
+ -- end if;
+
+ -- if Count = 0 then
+ -- raise Assertion_Error with "contract cases incomplete";
+ -- <or>
+ -- Flag_N+1 := True; -- when "others" present
+
+ -- elsif Count > 1 then
+ -- declare
+ -- Str0 : constant String :=
+ -- "contract cases overlap for subprogram ABC";
+ -- Str1 : constant String :=
+ -- (if Flag_1 then
+ -- Str0 & "case guard at xxx evaluates to True"
+ -- else Str0);
+ -- StrN : constant String :=
+ -- (if Flag_N then
+ -- StrN-1 & "case guard at xxx evaluates to True"
+ -- else StrN-1);
+ -- begin
+ -- raise Assertion_Error with StrN;
+ -- end;
+ -- end if;
+
+ -- procedure _Postconditions is
+ -- begin
+ -- <postconditions (if any)>
+
+ -- if Flag_1 and then not Consequence_1 then
+ -- raise Assertion_Error with "failed contract case at xxx";
+ -- end if;
+ -- . . .
+ -- if Flag_N[+1] and then not Consequence_N[+1] then
+ -- raise Assertion_Error with "failed contract case at xxx";
+ -- end if;
+ -- end _Postconditions;
+ -- begin
+ -- . . .
+ -- end S;
+
+ procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id) is
+ Loc : constant Source_Ptr := Sloc (CCs);
+
+ procedure Case_Guard_Error
+ (Decls : List_Id;
+ Flag : Entity_Id;
+ Error_Loc : Source_Ptr;
+ Msg : in out Entity_Id);
+ -- Given a declarative list Decls, status flag Flag, the location of
+ -- the error and a string Msg, construct the following check:
+ -- Msg : constant String :=
+ -- (if Flag then
+ -- Msg & "case guard at Error_Loc evaluates to True"
+ -- else Msg);
+ -- The resulting code is added to Decls
+
+ procedure Consequence_Error
+ (Checks : in out Node_Id;
+ Flag : Entity_Id;
+ Conseq : Node_Id);
+ -- Given an if statement Checks, status flag Flag and a consequence
+ -- Conseq, construct the following check:
+ -- [els]if Flag and then not Conseq then
+ -- raise Assertion_Error
+ -- with "failed contract case at Sloc (Conseq)";
+ -- [end if;]
+ -- The resulting code is added to Checks
+
+ function Declaration_Of (Id : Entity_Id) return Node_Id;
+ -- Given the entity Id of a boolean flag, generate:
+ -- Id : Boolean := False;
+
+ function Increment (Id : Entity_Id) return Node_Id;
+ -- Given the entity Id of a numerical variable, generate:
+ -- Id := Id + 1;
+
+ function Set (Id : Entity_Id) return Node_Id;
+ -- Given the entity Id of a boolean variable, generate:
+ -- Id := True;
+
+ ----------------------
+ -- Case_Guard_Error --
+ ----------------------
+
+ procedure Case_Guard_Error
+ (Decls : List_Id;
+ Flag : Entity_Id;
+ Error_Loc : Source_Ptr;
+ Msg : in out Entity_Id)
+ is
+ New_Line : constant Character := Character'Val (10);
+ New_Msg : constant Entity_Id := Make_Temporary (Loc, 'S');
+
+ begin
+ Start_String;
+ Store_String_Char (New_Line);
+ Store_String_Chars (" case guard at ");
+ Store_String_Chars (Build_Location_String (Error_Loc));
+ Store_String_Chars (" evaluates to True");
+
+ -- Generate:
+ -- New_Msg : constant String :=
+ -- (if Flag then
+ -- Msg & "case guard at Error_Loc evaluates to True"
+ -- else Msg);
+
+ Append_To (Decls,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => New_Msg,
+ Constant_Present => True,
+ Object_Definition => New_Reference_To (Standard_String, Loc),
+ Expression =>
+ Make_If_Expression (Loc,
+ Expressions => New_List (
+ New_Reference_To (Flag, Loc),
+
+ Make_Op_Concat (Loc,
+ Left_Opnd => New_Reference_To (Msg, Loc),
+ Right_Opnd => Make_String_Literal (Loc, End_String)),
+
+ New_Reference_To (Msg, Loc)))));
+
+ Msg := New_Msg;
+ end Case_Guard_Error;
+
+ -----------------------
+ -- Consequence_Error --
+ -----------------------
+
+ procedure Consequence_Error
+ (Checks : in out Node_Id;
+ Flag : Entity_Id;
+ Conseq : Node_Id)
+ is
+ Cond : Node_Id;
+ Error : Node_Id;
+
+ begin
+ -- Generate:
+ -- Flag and then not Conseq
+
+ Cond :=
+ Make_And_Then (Loc,
+ Left_Opnd => New_Reference_To (Flag, Loc),
+ Right_Opnd =>
+ Make_Op_Not (Loc,
+ Right_Opnd => Relocate_Node (Conseq)));
+
+ -- Generate:
+ -- raise Assertion_Error
+ -- with "failed contract case at Sloc (Conseq)";
+
+ Start_String;
+ Store_String_Chars ("failed contract case at ");
+ Store_String_Chars (Build_Location_String (Sloc (Conseq)));
+
+ Error :=
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc),
+ Parameter_Associations => New_List (
+ Make_String_Literal (Loc, End_String)));
+
+ if No (Checks) then
+ Checks :=
+ Make_If_Statement (Loc,
+ Condition => Cond,
+ Then_Statements => New_List (Error));
+
+ else
+ if No (Elsif_Parts (Checks)) then
+ Set_Elsif_Parts (Checks, New_List);
+ end if;
+
+ Append_To (Elsif_Parts (Checks),
+ Make_Elsif_Part (Loc,
+ Condition => Cond,
+ Then_Statements => New_List (Error)));
+ end if;
+ end Consequence_Error;
+
+ --------------------
+ -- Declaration_Of --
+ --------------------
+
+ function Declaration_Of (Id : Entity_Id) return Node_Id is
+ begin
+ return
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Id,
+ Object_Definition =>
+ New_Reference_To (Standard_Boolean, Loc),
+ Expression =>
+ New_Reference_To (Standard_False, Loc));
+ end Declaration_Of;
+
+ ---------------
+ -- Increment --
+ ---------------
+
+ function Increment (Id : Entity_Id) return Node_Id is
+ begin
+ return
+ Make_Assignment_Statement (Loc,
+ Name => New_Reference_To (Id, Loc),
+ Expression =>
+ Make_Op_Add (Loc,
+ Left_Opnd => New_Reference_To (Id, Loc),
+ Right_Opnd => Make_Integer_Literal (Loc, 1)));
+ end Increment;
+
+ ---------
+ -- Set --
+ ---------
+
+ function Set (Id : Entity_Id) return Node_Id is
+ begin
+ return
+ Make_Assignment_Statement (Loc,
+ Name => New_Reference_To (Id, Loc),
+ Expression => New_Reference_To (Standard_True, Loc));
+ end Set;
+
+ -- Local variables
+
+ Aggr : constant Node_Id :=
+ Expression (First
+ (Pragma_Argument_Associations (CCs)));
+ Decls : constant List_Id := Declarations (N);
+ Multiple_PCs : constant Boolean :=
+ List_Length (Component_Associations (Aggr)) > 1;
+ Case_Guard : Node_Id;
+ CG_Checks : Node_Id;
+ CG_Stmts : List_Id;
+ Conseq : Node_Id;
+ Conseq_Checks : Node_Id := Empty;
+ Count : Entity_Id;
+ Error_Decls : List_Id;
+ Flag : Entity_Id;
+ Msg_Str : Entity_Id;
+ Others_Flag : Entity_Id := Empty;
+ Post_Case : Node_Id;
+
+ -- Start of processing for Expand_Contract_Cases
+
+ begin
+ -- Create the counter which tracks the number of case guards that
+ -- evaluate to True.
+
+ -- Count : Natural := 0;
+
+ Count := Make_Temporary (Loc, 'C');
+
+ Prepend_To (Decls,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Count,
+ Object_Definition => New_Reference_To (Standard_Natural, Loc),
+ Expression => Make_Integer_Literal (Loc, 0)));
+
+ -- Create the base error message for multiple overlapping case
+ -- guards.
+
+ -- Msg_Str : constant String :=
+ -- "contract cases overlap for subprogram Subp_Id";
+
+ if Multiple_PCs then
+ Msg_Str := Make_Temporary (Loc, 'S');
+
+ Start_String;
+ Store_String_Chars ("contract cases overlap for subprogram ");
+ Store_String_Chars (Get_Name_String (Chars (Subp_Id)));
+
+ Error_Decls := New_List (
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Msg_Str,
+ Constant_Present => True,
+ Object_Definition => New_Reference_To (Standard_String, Loc),
+ Expression => Make_String_Literal (Loc, End_String)));
+ end if;
+
+ -- Process individual post cases
+
+ Post_Case := First (Component_Associations (Aggr));
+ while Present (Post_Case) loop
+ Case_Guard := First (Choices (Post_Case));
+ Conseq := Expression (Post_Case);
+
+ -- The "others" choice requires special processing
+
+ if Nkind (Case_Guard) = N_Others_Choice then
+ Others_Flag := Make_Temporary (Loc, 'F');
+ Prepend_To (Decls, Declaration_Of (Others_Flag));
+
+ -- Check possible overlap between a case guard and "others"
+
+ if Multiple_PCs then
+ Case_Guard_Error
+ (Decls => Error_Decls,
+ Flag => Others_Flag,
+ Error_Loc => Sloc (Case_Guard),
+ Msg => Msg_Str);
+ end if;
+
+ -- Check the corresponding consequence of "others"
+
+ Consequence_Error
+ (Checks => Conseq_Checks,
+ Flag => Others_Flag,
+ Conseq => Conseq);
+
+ -- Regular post case
+
+ else
+ -- Create the flag which tracks the state of its associated
+ -- case guard.
+
+ Flag := Make_Temporary (Loc, 'F');
+ Prepend_To (Decls, Declaration_Of (Flag));
+
+ -- The flag is set when the case guard is evaluated to True
+ -- if Case_Guard then
+ -- Flag := True;
+ -- Count := Count + 1;
+ -- end if;
+
+ Append_To (Decls,
+ Make_If_Statement (Loc,
+ Condition => Relocate_Node (Case_Guard),
+ Then_Statements => New_List (
+ Set (Flag),
+ Increment (Count))));
+
+ -- Check whether this case guard overlaps with another case
+ -- guard.
+
+ if Multiple_PCs then
+ Case_Guard_Error
+ (Decls => Error_Decls,
+ Flag => Flag,
+ Error_Loc => Sloc (Case_Guard),
+ Msg => Msg_Str);
+ end if;
+
+ -- The corresponding consequence of the case guard which
+ -- evaluated to True must hold on exit from the subprogram.
+
+ Consequence_Error (Conseq_Checks, Flag, Conseq);
+ end if;
+
+ Next (Post_Case);
+ end loop;
+
+ -- Raise Assertion_Error when none of the case guards evaluate to
+ -- True. The only exception is when we have "others", in which case
+ -- there is no error because "others" acts as a default True.
+
+ -- Generate:
+ -- Flag := True;
+
+ if Present (Others_Flag) then
+ CG_Stmts := New_List (Set (Others_Flag));
+
+ -- Generate:
+ -- raise Assetion_Error with "contract cases incomplete";
+
+ else
+ Start_String;
+ Store_String_Chars ("contract cases incomplete");
+
+ CG_Stmts := New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc),
+ Parameter_Associations => New_List (
+ Make_String_Literal (Loc, End_String))));
+ end if;
+
+ CG_Checks :=
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Eq (Loc,
+ Left_Opnd => New_Reference_To (Count, Loc),
+ Right_Opnd => Make_Integer_Literal (Loc, 0)),
+ Then_Statements => CG_Stmts);
+
+ -- Detect a possible failure due to several case guards evaluating to
+ -- True.
+
+ -- Generate:
+ -- elsif Count > 0 then
+ -- declare
+ -- <Error_Decls>
+ -- begin
+ -- raise Assertion_Error with <Msg_Str>;
+ -- end if;
+
+ if Multiple_PCs then
+ Set_Elsif_Parts (CG_Checks, New_List (
+ Make_Elsif_Part (Loc,
+ Condition =>
+ Make_Op_Gt (Loc,
+ Left_Opnd => New_Reference_To (Count, Loc),
+ Right_Opnd => Make_Integer_Literal (Loc, 1)),
+
+ Then_Statements => New_List (
+ Make_Block_Statement (Loc,
+ Declarations => Error_Decls,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Reference_To
+ (RTE (RE_Raise_Assert_Failure), Loc),
+ Parameter_Associations => New_List (
+ New_Reference_To (Msg_Str, Loc))))))))));
+ end if;
+
+ Append_To (Decls, CG_Checks);
+
+ -- Raise Assertion_Error when the corresponding consequence of a case
+ -- guard that evaluated to True fails.
+
+ if No (Plist) then
+ Plist := New_List;
+ end if;
+
+ Append_To (Plist, Conseq_Checks);
+ end Expand_Contract_Cases;
+
-------------
-- Grab_CC --
-------------
@@ -11736,6 +12194,9 @@
else
Append (Grab_CC, Plist);
end if;
+
+ elsif Pragma_Name (Prag) = Name_Contract_Cases then
+ Expand_Contract_Cases (Prag, Spec_Id);
end if;
Prag := Next_Pragma (Prag);
@@ -11850,7 +12311,7 @@
Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
end if;
- -- Same if return value is an access to type with invariants.
+ -- Same if return value is an access to type with invariants
Check_Access_Invariants (Rent);
end;
===================================================================
@@ -1112,6 +1112,7 @@
Pragma_Compile_Time_Warning |
Pragma_Compiler_Unit |
Pragma_Contract_Case |
+ Pragma_Contract_Cases |
Pragma_Convention_Identifier |
Pragma_CPP_Class |
Pragma_CPP_Constructor |
===================================================================
@@ -1629,14 +1629,89 @@
Aitem :=
Make_Pragma (Loc,
- Pragma_Identifier =>
- Make_Identifier (Sloc (Id), Nam),
- Pragma_Argument_Associations =>
- Args);
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Nam),
+ Pragma_Argument_Associations => Args);
Delay_Required := False;
end;
+ when Aspect_Contract_Cases => Contract_Cases : declare
+ Case_Guard : Node_Id;
+ Extra : Node_Id;
+ Others_Seen : Boolean := False;
+ Post_Case : Node_Id;
+
+ begin
+ if Nkind (Parent (N)) = N_Compilation_Unit then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_N ("incorrect placement of aspect `%`", E);
+ goto Continue;
+ end if;
+
+ if Nkind (Expr) /= N_Aggregate then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_NE
+ ("wrong syntax for aspect `%` for &", Id, E);
+ goto Continue;
+ end if;
+
+ -- Verify the legality of individual post cases
+
+ Post_Case := First (Component_Associations (Expr));
+ while Present (Post_Case) loop
+ if Nkind (Post_Case) /= N_Component_Association then
+ Error_Msg_N ("wrong syntax in post case", Post_Case);
+ goto Continue;
+ end if;
+
+ -- Each post case must have exactly one case guard
+
+ Case_Guard := First (Choices (Post_Case));
+ Extra := Next (Case_Guard);
+
+ if Present (Extra) then
+ Error_Msg_N
+ ("post case may have only one case guard", Extra);
+ goto Continue;
+ end if;
+
+ -- Check the placement of "others" (if available)
+
+ if Nkind (Case_Guard) = N_Others_Choice then
+ if Others_Seen then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_N
+ ("only one others choice allowed in aspect %",
+ Case_Guard);
+ goto Continue;
+ else
+ Others_Seen := True;
+ end if;
+
+ elsif Others_Seen then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_N
+ ("others must be the last choice in aspect %", N);
+ goto Continue;
+ end if;
+
+ Next (Post_Case);
+ end loop;
+
+ -- Transform the aspect into a pragma
+
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Loc, Nam),
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))));
+
+ Delay_Required := False;
+ end Contract_Cases;
+
-- Case 5: Special handling for aspects with an optional
-- boolean argument.
@@ -6764,6 +6839,7 @@
-- Here is the list of aspects that don't require delay analysis.
when Aspect_Contract_Case |
+ Aspect_Contract_Cases |
Aspect_Dimension |
Aspect_Dimension_System |
Aspect_Implicit_Dereference |
===================================================================
@@ -463,6 +463,7 @@
Name_Complete_Representation : constant Name_Id := N + $; -- GNAT
Name_Complex_Representation : constant Name_Id := N + $; -- GNAT
Name_Contract_Case : constant Name_Id := N + $; -- GNAT
+ Name_Contract_Cases : constant Name_Id := N + $; -- GNAT
Name_Controlled : constant Name_Id := N + $;
Name_Convention : constant Name_Id := N + $;
Name_CPP_Class : constant Name_Id := N + $; -- GNAT
@@ -1736,6 +1737,7 @@
Pragma_Complete_Representation,
Pragma_Complex_Representation,
Pragma_Contract_Case,
+ Pragma_Contract_Cases,
Pragma_Controlled,
Pragma_Convention,
Pragma_CPP_Class,