This patch implements rule SPARK RM 6.1.3 (5) which states:
If an Old attribute_reference occurs within a consequence other than the
consequence selected for (later) evaluation as described above, then the
associated implicit constant declaration (see Ada RM 6.1.1) is not
elaborated. [In particular, the prefix of the Old attribute_reference is
not evaluated].
------------
-- Source --
------------
-- old_evaluation.ads
package Old_Evaluation is
procedure Reset_Self;
function Self (Val : Integer) return Integer;
procedure Check_Old (Val : in out Integer)
with Contract_Cases =>
(Val < 0 => Val = Self (Val)'Old - 1,
Val = 0 => Val = Self (Val)'Old,
Val > 0 => Val = Self (Val)'Old + 1);
end Old_Evaluation;
-- old_evaluation.adb
package body Old_Evaluation is
Self_Called : Boolean := False;
procedure Check_Old (Val : in out Integer) is
begin
if Val < 0 then
Val := Val - 1;
elsif Val > 0 then
Val := Val + 1;
end if;
end Check_Old;
procedure Reset_Self is
begin
Self_Called := False;
end Reset_Self;
function Self (Val : Integer) return Integer is
begin
if Self_Called then
raise Program_Error;
else
Self_Called := True;
return Val;
end if;
end Self;
end Old_Evaluation;
-- old_main.adb
with Ada.Text_IO; use Ada.Text_IO;
with Old_Evaluation; use Old_Evaluation;
procedure Old_Main is
procedure Test_Value (Val : Integer) is
Num : Integer := Val;
begin
Reset_Self;
Check_Old (Num);
exception
when others => Put_Line ("ERROR:" & Val'Img & " failed");
end Test_Value;
begin
Test_Value (-2);
Test_Value (0);
Test_Value (5);
end Old_Main;
-----------------
-- Compilation --
-----------------
$ gnatmake -q -gnata old_main.adb
$ ./old_main
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-19 Hristian Kirtchev <[email protected]>
* exp_ch6.adb Add with and use clause for Exp_Prag.
(Expand_Contract_Cases): Relocated to Exp_Prag.
* exp_ch6.ads (Expand_Contract_Cases): Relocated to Exp_Prag.
* exp_prag.adb Add with and use clauses for Checks and Validsw.
(Expand_Contract_Cases): Relocated from Exp_Ch6. Update the
structure of the expanded code to showcase the evaluation of
attribute 'Old prefixes. Add local variable Old_Evals. Expand
any attribute 'Old references found within a consequence. Add
circuitry to evaluate the prefixes of attribute 'Old that
belong to a selected consequence.
(Expand_Old_In_Consequence): New routine.
* exp_prag.ads (Expand_Contract_Cases): Relocated from Exp_Ch6.
* sem_attr.adb (Check_Use_In_Contract_Cases): Warn that a
potentially unevaluated prefix is always evaluated.
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb (revision 207890)
+++ exp_ch6.adb (working copy)
@@ -41,6 +41,7 @@
with Exp_Dist; use Exp_Dist;
with Exp_Intr; use Exp_Intr;
with Exp_Pakd; use Exp_Pakd;
+with Exp_Prag; use Exp_Prag;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Exp_VFpt; use Exp_VFpt;
@@ -4118,476 +4119,6 @@
end if;
end Expand_Call;
- ---------------------------
- -- 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 "xxx 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;
- Decls : List_Id;
- Stmts : in out List_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_Implicit_If_Statement (CCs,
- 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)));
- 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;
- Multiple_PCs : Boolean;
- Others_Flag : Entity_Id := Empty;
- Post_Case : Node_Id;
-
- -- Start of processing for Expand_Contract_Cases
-
- begin
- -- Do nothing if pragma is not enabled. If pragma is disabled, it has
- -- already been rewritten as a Null statement.
-
- if Is_Ignored (CCs) then
- return;
-
- -- Guard against malformed contract cases
-
- elsif Nkind (Aggr) /= N_Aggregate then
- return;
- end if;
-
- Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
-
- -- 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 and Exception_Extra_Info 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_Implicit_If_Statement (CCs,
- Condition => Relocate_Node (Case_Guard),
- Then_Statements => New_List (
- Set (Flag),
- Increment (Count))));
-
- -- Check whether this case guard overlaps with another one
-
- if Multiple_PCs and Exception_Extra_Info 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
- (Checks => Conseq_Checks,
- Flag => Flag,
- Conseq => 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 Assertion_Error with "xxx contract cases incomplete";
-
- else
- Start_String;
- Store_String_Chars (Build_Location_String (Loc));
- 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_Implicit_If_Statement (CCs,
- 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 (Stmts) then
- Stmts := New_List;
- end if;
-
- Append_To (Stmts, Conseq_Checks);
- end Expand_Contract_Cases;
-
-------------------------------
-- Expand_Ctrl_Function_Call --
-------------------------------
Index: exp_ch6.ads
===================================================================
--- exp_ch6.ads (revision 207879)
+++ exp_ch6.ads (working copy)
@@ -71,17 +71,6 @@
-- This procedure contains common processing for Expand_N_Function_Call,
-- Expand_N_Procedure_Statement, and Expand_N_Entry_Call.
- procedure Expand_Contract_Cases
- (CCs : Node_Id;
- Subp_Id : Entity_Id;
- Decls : List_Id;
- Stmts : in out List_Id);
- -- Given pragma Contract_Cases CCs, create the circuitry needed to evaluate
- -- case guards and trigger consequence expressions. Subp_Id is the related
- -- subprogram for which the pragma applies. Decls are the declarations of
- -- Subp_Id's body. All generated code is added to list Stmts. If Stmts is
- -- empty, a new list is created.
-
procedure Expand_Subprogram_Contract
(N : Node_Id;
Spec_Id : Entity_Id;
Index: exp_prag.adb
===================================================================
--- exp_prag.adb (revision 207879)
+++ exp_prag.adb (working copy)
@@ -25,6 +25,7 @@
with Atree; use Atree;
with Casing; use Casing;
+with Checks; use Checks;
with Debug; use Debug;
with Einfo; use Einfo;
with Errout; use Errout;
@@ -50,6 +51,7 @@
with Targparm; use Targparm;
with Tbuild; use Tbuild;
with Uintp; use Uintp;
+with Validsw; use Validsw;
package body Exp_Prag is
@@ -148,6 +150,645 @@
end if;
end Arg3;
+ ---------------------------
+ -- Expand_Contract_Cases --
+ ---------------------------
+
+ -- Pragma Contract_Cases is expanded in the following manner:
+
+ -- subprogram S is
+ -- Count : Natural := 0;
+ -- Flag_1 : Boolean := False;
+ -- . . .
+ -- Flag_N : Boolean := False;
+ -- Flag_N+1 : Boolean := False; -- when "others" present
+ -- Pref_1 : ...;
+ -- . . .
+ -- Pref_M : ...;
+
+ -- <preconditions (if any)>
+
+ -- -- Evaluate all case guards
+
+ -- 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;
+
+ -- -- Emit errors depending on the number of case guards that
+ -- -- evaluated to True.
+
+ -- if Count = 0 then
+ -- raise Assertion_Error with "xxx 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;
+
+ -- -- Evaluate all attribute 'Old prefixes found in the selected
+ -- -- consequence.
+
+ -- if Flag_1 then
+ -- Pref_1 := <prefix of 'Old found in Consequence_1>
+ -- . . .
+ -- elsif Flag_N then
+ -- Pref_M := <prefix of 'Old found in Consequence_N>
+ -- 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;
+ Decls : List_Id;
+ Stmts : in out List_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;
+
+ procedure Expand_Old_In_Consequence
+ (Decls : List_Id;
+ Evals : in out Node_Id;
+ Flag : Entity_Id;
+ Conseq : Node_Id);
+ -- Perform specialized expansion of all attribute 'Old references found
+ -- in consequence Conseq such that at runtime only prefixes coming from
+ -- the selected consequence are evaluated. Any temporaries generated in
+ -- the process are added to declarative list Decls. Evals is a complex
+ -- if statement tasked with the evaluation of all prefixes coming from
+ -- a selected consequence. Flag is the corresponding case guard flag.
+ -- Conseq is the consequence expression.
+
+ 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_Implicit_If_Statement (CCs,
+ 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;
+
+ -------------------------------
+ -- Expand_Old_In_Consequence --
+ -------------------------------
+
+ procedure Expand_Old_In_Consequence
+ (Decls : List_Id;
+ Evals : in out Node_Id;
+ Flag : Entity_Id;
+ Conseq : Node_Id)
+ is
+ Eval_Stmts : List_Id := No_List;
+ -- The evaluation sequence expressed as assignment statements of all
+ -- prefixes of attribute 'Old found in the current consequence.
+
+ function Expand_Old (N : Node_Id) return Traverse_Result;
+ -- Determine whether an arbitrary node denotes attribute 'Old and if
+ -- it does, perform all expansion-related actions.
+
+ ----------------
+ -- Expand_Old --
+ ----------------
+
+ function Expand_Old (N : Node_Id) return Traverse_Result is
+ Decl : Node_Id;
+ Pref : Node_Id;
+ Temp : Entity_Id;
+
+ begin
+ if Nkind (N) = N_Attribute_Reference
+ and then Attribute_Name (N) = Name_Old
+ then
+ Pref := Prefix (N);
+ Temp := Make_Temporary (Loc, 'T', Pref);
+
+ -- Generate a temporary to capture the value of the prefix:
+ -- Temp : <Pref type>;
+
+ Decl :=
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Temp,
+ Object_Definition =>
+ New_Reference_To (Etype (Pref), Loc));
+ Set_No_Initialization (Decl);
+
+ Append_To (Decls, Decl);
+
+ -- Evaluate the prefix, generate:
+ -- Temp := <Pref>;
+
+ if No (Eval_Stmts) then
+ Eval_Stmts := New_List;
+ end if;
+
+ Append_To (Eval_Stmts,
+ Make_Assignment_Statement (Loc,
+ Name => New_Reference_To (Temp, Loc),
+ Expression => Pref));
+
+ -- Ensure that the prefix is valid
+
+ if Validity_Checks_On and then Validity_Check_Operands then
+ Ensure_Valid (Pref);
+ end if;
+
+ -- Replace the original attribute 'Old by a reference to the
+ -- generated temporary.
+
+ Rewrite (N, New_Reference_To (Temp, Loc));
+ end if;
+
+ return OK;
+ end Expand_Old;
+
+ procedure Expand_Olds is new Traverse_Proc (Expand_Old);
+
+ -- Start of processing for Expand_Old_In_Consequence
+
+ begin
+ -- Inspect the consequence and expand any attribute 'Old references
+ -- found within.
+
+ Expand_Olds (Conseq);
+
+ -- Augment the machinery to trigger the evaluation of all prefixes
+ -- found in the step above. If Eval is empty, then this is the first
+ -- consequence to yield expansion of 'Old. Generate:
+
+ -- if Flag then
+ -- <evaluation statements>
+ -- end if;
+
+ if No (Evals) then
+ Evals :=
+ Make_Implicit_If_Statement (CCs,
+ Condition => New_Reference_To (Flag, Loc),
+ Then_Statements => Eval_Stmts);
+
+ -- Otherwise generate:
+ -- elsif Flag then
+ -- <evaluation statements>
+ -- end if;
+
+ else
+ if No (Elsif_Parts (Evals)) then
+ Set_Elsif_Parts (Evals, New_List);
+ end if;
+
+ Append_To (Elsif_Parts (Evals),
+ Make_Elsif_Part (Loc,
+ Condition => New_Reference_To (Flag, Loc),
+ Then_Statements => Eval_Stmts));
+ end if;
+ end Expand_Old_In_Consequence;
+
+ ---------------
+ -- 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)));
+ 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;
+ Multiple_PCs : Boolean;
+ Old_Evals : Node_Id := Empty;
+ Others_Flag : Entity_Id := Empty;
+ Post_Case : Node_Id;
+
+ -- Start of processing for Expand_Contract_Cases
+
+ begin
+ -- Do nothing if pragma is not enabled. If pragma is disabled, it has
+ -- already been rewritten as a Null statement.
+
+ if Is_Ignored (CCs) then
+ return;
+
+ -- Guard against malformed contract cases
+
+ elsif Nkind (Aggr) /= N_Aggregate then
+ return;
+ end if;
+
+ Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
+
+ -- 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 and Exception_Extra_Info then
+ Case_Guard_Error
+ (Decls => Error_Decls,
+ Flag => Others_Flag,
+ Error_Loc => Sloc (Case_Guard),
+ Msg => Msg_Str);
+ end if;
+
+ -- Inspect the consequence and perform special expansion of any
+ -- attribute 'Old references found within.
+
+ Expand_Old_In_Consequence
+ (Decls => Decls,
+ Evals => Old_Evals,
+ Flag => Others_Flag,
+ Conseq => Conseq);
+
+ -- 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_Implicit_If_Statement (CCs,
+ Condition => Relocate_Node (Case_Guard),
+ Then_Statements => New_List (
+ Set (Flag),
+ Increment (Count))));
+
+ -- Check whether this case guard overlaps with another one
+
+ if Multiple_PCs and Exception_Extra_Info then
+ Case_Guard_Error
+ (Decls => Error_Decls,
+ Flag => Flag,
+ Error_Loc => Sloc (Case_Guard),
+ Msg => Msg_Str);
+ end if;
+
+ -- Inspect the consequence and perform special expansion of any
+ -- attribute 'Old references found within.
+
+ Expand_Old_In_Consequence
+ (Decls => Decls,
+ Evals => Old_Evals,
+ Flag => Flag,
+ Conseq => Conseq);
+
+ -- The corresponding consequence of the case guard which evaluated
+ -- to True must hold on exit from the subprogram.
+
+ Consequence_Error
+ (Checks => Conseq_Checks,
+ Flag => Flag,
+ Conseq => 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 Assertion_Error with "xxx contract cases incomplete";
+
+ else
+ Start_String;
+ Store_String_Chars (Build_Location_String (Loc));
+ 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_Implicit_If_Statement (CCs,
+ 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);
+
+ -- Once all case guards are evaluated and checked, evaluate any prefixes
+ -- of attribute 'Old founds in the selected consequence.
+
+ Append_To (Decls, Old_Evals);
+
+ -- Raise Assertion_Error when the corresponding consequence of a case
+ -- guard that evaluated to True fails.
+
+ if No (Stmts) then
+ Stmts := New_List;
+ end if;
+
+ Append_To (Stmts, Conseq_Checks);
+ end Expand_Contract_Cases;
+
---------------------
-- Expand_N_Pragma --
---------------------
Index: exp_prag.ads
===================================================================
--- exp_prag.ads (revision 207879)
+++ exp_prag.ads (working copy)
@@ -31,4 +31,15 @@
procedure Expand_N_Pragma (N : Node_Id);
+ procedure Expand_Contract_Cases
+ (CCs : Node_Id;
+ Subp_Id : Entity_Id;
+ Decls : List_Id;
+ Stmts : in out List_Id);
+ -- Given pragma Contract_Cases CCs, create the circuitry needed to evaluate
+ -- case guards and trigger consequence expressions. Subp_Id is the related
+ -- subprogram for which the pragma applies. Decls are the declarations of
+ -- Subp_Id's body. All generated code is added to list Stmts. If Stmts is
+ -- No_List on entry, a new list is created.
+
end Exp_Prag;
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 207881)
+++ sem_attr.adb (working copy)
@@ -4466,7 +4466,22 @@
-- contract case as this is the only postcondition-like part of
-- the pragma.
- if Expr /= Expression (Parent (Expr)) then
+ if Expr = Expression (Parent (Expr)) then
+
+ -- Warn that a potentially unevaluated prefix is always
+ -- evaluated when the corresponding consequence is selected.
+
+ if Is_Potentially_Unevaluated (P) then
+ Error_Msg_Name_1 := Aname;
+ Error_Msg_N
+ ("?prefix of attribute % is always evaluated when "
+ & "related consequence is selected", P);
+ end if;
+
+ -- Attribute 'Old appears in the condition of a contract case.
+ -- Emit an error since this is not a postcondition-like context.
+
+ else
Error_Attr
("attribute % cannot appear in the condition of a contract "
& "case (SPARK RM 6.1.3(2))", P);
