[Ada] Aspect / pragma Contract_Cases
Arnaud Charlet
charlet@adacore.com
Wed Dec 5 10:39:00 GMT 2012
This patch provides the initial implementation of aspect/pragma Contract_Cases.
This construct is intended for formal verification proofs.
The syntax of the aspect is as follows:
ASPECT_DEFINITION ::= ( POST_CASE_LIST )
POST_CASE_LIST ::= POST_CASE {, POST_CASE_LIST}
POST_CASE ::= CASE_GUARD => CONSEQUENCE
CASE_GUARD ::= boolean_EXPRESSION | others
CONSEQUENCE ::= boolean_EXPRESSION
The syntax of the pragma is as follows:
pragma Contract_Cases (POST_CASE_LIST)
The brief semantic rules of this construct are:
Case_guard and consequence expressions are expected to be of any Boolean type.
No more than one "other" case guard may be provided. A consequence expression
is considered to be a postcondition expression for purposes of determining the
legality of 'Old and 'Result attribute_references.
Upon a call of a subprogram or entry which is subject to an enabled
Contract_Cases aspect_specification, Contract_Cases checks are performed as
follows:
- Immediately after the specific precondition expression is evaluated and
checked (or, if that check is disabled, at the point where the check would
have been performed if it were enabled), all of the case_guard expressions
are evaluated in textual order. A check is performed that exactly one (if
no others case_guard is provided) or at most one (if an others case_guard
is provided) of these conditions evaluates to True;
Assertions.Assertion_Error is raised if this check fails.
- Immediately after the specific postcondition expression is evaluated and
checked (or, if that check is disabled, at the point where the check would
have been performed if it were enabled), exactly one of the consequences
is evaluated. The consequence to be evaluated is the one corresponding to
the one case_guard whose evaluation yielded True (if such a case_guard
exists), or to the others case_guard (if every case_guard's evaluation
yielded False). A check is performed that the evaluation of the selected
consequence evaluates to True; Assertions.Assertion_Error is raised if
this check fails.
------------
-- Source --
------------
-- subprograms.ads
package Subprograms is
function Return_Self (Val : Integer) return Integer
with Contract_Cases => ((Val >= 0 => Return_Self'Result = 1,
Val = 0 => Return_Self'Result = 2,
Val <= 0 => Return_Self'Result = 3));
end Subprograms;
-- subprograms.adb
package body Subprograms is
function Return_Self (Val : Integer) return Integer is
begin
return Val;
end Return_Self;
end Subprograms;
-- main.adb
with Subprograms; use Subprograms;
procedure Main is
Val : constant Integer := Return_Self (0);
begin
null;
end Main;
----------------------------
-- Compilation and output --
----------------------------
$ gnatmake -q -gnat12 -gnata -gnatd.V main.adb
$ ./main
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : contract cases overlap for subprogram return_self
case guard at subprograms.ads:3 evaluates to True
case guard at subprograms.ads:4 evaluates to True
case guard at subprograms.ads:5 evaluates to True
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-12-05 Hristian Kirtchev <kirtchev@adacore.com>
* aspects.adb: Add Contract_Cases to the canonical aspects map.
* aspects.ads: Add aspect Contract_Cases in the various aspect
tables.
* par-prag.adb: The parser does not need to perform special
actions for pragma Contract_Cases.
* sem_ch6.adb (Expand_Contract_Cases): New routine.
(Process_Contract_Cases): Convert pragma Contract_Cases into pre-
and post- condition checks that verify the runtime state of all
case guards and their corresponding consequences.
* sem_ch13.adb (Analyze_Aspect_Specifications): Perform
various legality checks on aspect Contract_Cases. The aspect is
transformed into a pragma.
* sem_prag.adb: Add an entry in table Sig_Flags for pragma
Contract_Cases.
(Analyze_Pragma): Perform various legality
checks on pragma Contract_Cases. The pragma is associated with
the contract of the related subprogram.
(Chain_CTC): Omit pragma
Contract_Cases because it does not introduce a unique case name
and does not follow the syntax of Contract_Case and Test_Case.
* snames.ads-tmpl: Add new name Name_Contract_Cases. Add a
Pragma_Id for Contract_Cases.
-------------- next part --------------
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 194196)
+++ sem_prag.adb (working copy)
@@ -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,
Index: aspects.adb
===================================================================
--- aspects.adb (revision 194188)
+++ aspects.adb (working copy)
@@ -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,
Index: aspects.ads
===================================================================
--- aspects.ads (revision 194188)
+++ aspects.ads (working copy)
@@ -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,
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 194188)
+++ sem_ch6.adb (working copy)
@@ -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;
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 194193)
+++ par-prag.adb (working copy)
@@ -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 |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 194188)
+++ sem_ch13.adb (working copy)
@@ -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 |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 194193)
+++ snames.ads-tmpl (working copy)
@@ -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,
More information about the Gcc-patches
mailing list