* [Ada] Contract_Cases on entries
@ 2015-11-12 11:15 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2015-11-12 11:15 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 14099 bytes --]
This patch implements apect/pragma Contract_Cases on enties.
------------
-- Source --
------------
-- tracker.ads
package Tracker is
type Check_Kind is
(Pre,
Refined_Post,
Post,
Conseq_1,
Conseq_2);
type Tested_Array is array (Check_Kind) of Boolean;
-- A value of "True" indicates that a check has been tested
function Greater_Than
(Kind : Check_Kind;
Val : Natural;
Exp : Natural) return Boolean;
-- Determine whether value Val is greater than expected value Exp. The
-- routine also updates the history for check of kind Kind. Duplicate
-- attempts to modify the history are flagged as errors.
procedure Reset;
-- Reset the history
procedure Verify (Exp : Tested_Array);
-- Verify whether expected tests Exp were indeed checked. Emit an error if
-- this is not the case.
end Tracker;
-- tacker.adb
with Ada.Text_IO; use Ada.Text_IO;
package body Tracker is
History : array (Check_Kind) of Boolean := (others => False);
-- The history of performed checked. A value of "True" indicates that a
-- check was performed.
------------------
-- Greater_Than --
------------------
function Greater_Than
(Kind : Check_Kind;
Val : Natural;
Exp : Natural) return Boolean
is
begin
if History (Kind) then
Put_Line (" ERROR: " & Kind'Img & " tested multiple times");
else
History (Kind) := True;
end if;
return Val > Exp;
end Greater_Than;
-----------
-- Reset --
-----------
procedure Reset is
begin
History := (others => False);
end Reset;
------------
-- Verify --
------------
procedure Verify (Exp : Tested_Array) is
begin
for Index in Check_Kind'Range loop
if Exp (Index) and not History (Index) then
Put_Line (" ERROR: " & Index'Img & " was not tested");
elsif not Exp (Index) and History (Index) then
Put_Line (" ERROR: " & Index'Img & " was tested");
end if;
end loop;
end Verify;
end Tracker;
-- sync_contracts.ads
with Tracker; use Tracker;
package Sync_Contracts
with SPARK_Mode,
Abstract_State => State
is
protected type Prot_Typ is
entry Prot_Entry (Input : Natural; Output : out Natural)
with Global => (Input => State),
Depends => ((Prot_Typ, Output) => (State, Prot_Typ, Input)),
Pre => Greater_Than (Pre, Input, 1),
Post => Greater_Than (Post, Output, 4),
Contract_Cases =>
(Input < 5 => True,
Input = 5 => Greater_Than (Conseq_1, Output, 6),
Input = 6 => Greater_Than (Conseq_2, Output, 7),
Input > 6 => False);
procedure Prot_Proc (Input : Natural; Output : out Natural)
with Pre => Greater_Than (Pre , Input, 1),
Post => Greater_Than (Post, Output, 4),
Contract_Cases =>
(Input < 5 => True,
Input = 5 => Greater_Than (Conseq_1, Output, 6),
Input = 6 => Greater_Than (Conseq_2, Output, 7),
Input > 6 => False);
function Prot_Func (Input : Natural) return Natural
with Pre => Greater_Than (Pre , Input, 1),
Post => Greater_Than (Post, Prot_Func'Result, 4),
Contract_Cases =>
(Input < 5 => True,
Input = 5 => Greater_Than (Conseq_1, Prot_Func'Result, 6),
Input = 6 => Greater_Than (Conseq_2, Prot_Func'Result, 7),
Input > 6 => False);
end Prot_Typ;
task type Tsk_Typ is
entry Tsk_Entry (Input : Natural; Output : out Natural)
with Pre => Greater_Than (Pre , Input, 1),
Post => Greater_Than (Post, Output, 4),
Contract_Cases =>
(Input < 5 => True,
Input = 5 => Greater_Than (Conseq_1, Output, 6),
Input = 6 => Greater_Than (Conseq_2, Output, 7),
Input > 6 => False);
end Tsk_Typ;
end Sync_Contracts;
-- sync_contracts.adb
package body Sync_Contracts
with SPARK_Mode,
Refined_State => (State => Var)
is
Var : Integer := 1;
protected body Prot_Typ is
entry Prot_Entry (Input : Natural; Output : out Natural)
with Refined_Global => (Input => Var),
Refined_Depends => ((Prot_Typ, Output) => (Var, Prot_Typ, Input)),
Refined_Post => Greater_Than (Refined_Post, Output, 3)
when True
is
begin
Output := Input + 1;
end Prot_Entry;
procedure Prot_Proc (Input : Natural; Output : out Natural)
with Refined_Post => Greater_Than (Refined_Post, Output, 3)
is
begin
Output := Input + 1;
end Prot_Proc;
function Prot_Func (Input : Natural) return Natural
with Refined_Post => Greater_Than (Refined_Post, Prot_Func'Result, 3)
is
begin
return Input + 1;
end Prot_Func;
end Prot_Typ;
task body Tsk_Typ is
begin
select
accept Tsk_Entry (Input : Natural; Output : out Natural) do
Output := Input + 1;
end Tsk_Entry;
or
terminate;
end select;
end Tsk_Typ;
end Sync_Contracts;
-- main.adb
with Ada.Assertions; use Ada.Assertions;
with Ada.Text_IO; use Ada.Text_IO;
with Sync_Contracts; use Sync_Contracts;
with Tracker; use Tracker;
procedure Main is
Result : Natural;
begin
-- NOTES:
-- 1) Refined_Post does not work on entry bodies due to an implementation
-- limitation.
-- 2) The consequences of Contract_Cases are mutually exclusive, only one
-- should fail at any one time.
declare
P : Prot_Typ;
begin
-- Protected preconditions
Put_Line ("Test 1");
Reset;
begin
P.Prot_Entry (1, Result);
Put_Line ("ERROR: Test 1: did not fail");
exception
when Assertion_Error => Verify ((True, False, False, False, False));
when others => Put_Line ("ERROR: Test 1: unexpected error");
end;
Put_Line ("Test 2");
Reset;
begin
P.Prot_Proc (1, Result);
Put_Line ("ERROR: Test 2: did not fail");
exception
when Assertion_Error => Verify ((True, False, False, False, False));
when others => Put_Line ("ERROR: Test 2: unexpected error");
end;
Put_Line ("Test 3");
Reset;
begin
Result := P.Prot_Func (1);
Put_Line ("ERROR: Test 3: did not fail");
exception
when Assertion_Error => Verify ((True, False, False, False, False));
when others => Put_Line ("ERROR: Test 3: unexpected error");
end;
-- Protected refined postconditions
Put_Line ("Test 4");
Reset;
begin
P.Prot_Entry (2, Result);
Put_Line ("ERROR: Test 4: did not fail");
exception
when Assertion_Error => Verify ((True, False, True, False, False));
when others => Put_Line ("ERROR: Test 4: unexpected error");
end;
Put_Line ("Test 5");
Reset;
begin
P.Prot_Proc (2, Result);
Put_Line ("ERROR: Test 5: did not fail");
exception
when Assertion_Error => Verify ((True, True, False, False, False));
when others => Put_Line ("ERROR: Test 5: unexpected error");
end;
Put_Line ("Test 6");
Reset;
begin
Result := P.Prot_Func (2);
Put_Line ("ERROR: Test 6: did not fail");
exception
when Assertion_Error => Verify ((True, True, False, False, False));
when others => Put_Line ("ERROR: Test 6: unexpected error");
end;
-- Protected postconditions
Put_Line ("Test 7");
Reset;
begin
P.Prot_Entry (3, Result);
Put_Line ("ERROR: Test 7: did not fail");
exception
when Assertion_Error => Verify ((True, False, True, False, False));
when others => Put_Line ("ERROR: Test 7: unexpected error");
end;
Put_Line ("Test 8");
Reset;
begin
P.Prot_Proc (3, Result);
Put_Line ("ERROR: Test 8: did not fail");
exception
when Assertion_Error => Verify ((True, True, True, False, False));
when others => Put_Line ("ERROR: Test 8: unexpected error");
end;
Put_Line ("Test 9");
Reset;
begin
Result := P.Prot_Func (3);
Put_Line ("ERROR: Test 9: did not fail");
exception
when Assertion_Error => Verify ((True, True, True, False, False));
when others => Put_Line ("ERROR: Test 9: unexpected error");
end;
-- Protected contract cases
Put_Line ("Test 10");
Reset;
begin
P.Prot_Entry (5, Result);
Put_Line ("ERROR: Test 10: did not fail");
exception
when Assertion_Error => Verify ((True, False, True, True, False));
when others => Put_Line ("ERROR: Test 10: unexpected error");
end;
Put_Line ("Test 11");
Reset;
begin
P.Prot_Entry (6, Result);
Put_Line ("ERROR: Test 11: did not fail");
exception
when Assertion_Error => Verify ((True, False, True, False, True));
when others => Put_Line ("ERROR: Test 11: unexpected error");
end;
Put_Line ("Test 12");
Reset;
begin
P.Prot_Proc (5, Result);
Put_Line ("ERROR: Test 12: did not fail");
exception
when Assertion_Error => Verify ((True, True, True, True, False));
when others => Put_Line ("ERROR: Test 12: unexpected error");
end;
-- NOTE:
Put_Line ("Test 13");
Reset;
begin
P.Prot_Proc (6, Result);
Put_Line ("ERROR: Test 13: did not fail");
exception
when Assertion_Error => Verify ((True, True, True, False, True));
when others => Put_Line ("ERROR: Test 13: unexpected error");
end;
Put_Line ("Test 14");
Reset;
begin
Result := P.Prot_Func (5);
Put_Line ("ERROR: Test 14: did not fail");
exception
when Assertion_Error => Verify ((True, True, True, True, False));
when others => Put_Line ("ERROR: Test 14: unexpected error");
end;
Put_Line ("Test 15");
Reset;
begin
Result := P.Prot_Func (6);
Put_Line ("ERROR: Test 15: did not fail");
exception
when Assertion_Error => Verify ((True, True, True, False, True));
when others => Put_Line ("ERROR: Test 15: unexpected error");
end;
end;
-- Task entry precondition
Put_Line ("Test 16");
Reset;
declare
T : Tsk_Typ;
begin
T.Tsk_Entry (1, Result);
Put_Line ("ERROR: Test 16: did not fail");
exception
when Assertion_Error => Verify ((True, False, False, False, False));
when others => Put_Line ("ERROR: Test 16: unexpected error");
end;
-- Task entry postcondition
Put_Line ("Test 17");
Reset;
declare
T : Tsk_Typ;
begin
T.Tsk_Entry (3, Result);
Put_Line ("ERROR: Test 17: did not fail");
exception
when Assertion_Error => Verify ((True, False, True, False, False));
when others => Put_Line ("ERROR: Test 17: unexpected error");
end;
-- Task contract cases
Put_Line ("Test 18");
Reset;
declare
T : Tsk_Typ;
begin
T.Tsk_Entry (5, Result);
Put_Line ("ERROR: Test 18: did not fail");
exception
when Assertion_Error => Verify ((True, False, True, True, False));
when others => Put_Line ("ERROR: Test 18: unexpected error");
end;
Put_Line ("Test 19");
Reset;
declare
T : Tsk_Typ;
begin
T.Tsk_Entry (6, Result);
Put_Line ("ERROR: Test 19: did not fail");
exception
when Assertion_Error => Verify ((True, False, True, False, True));
when others => Put_Line ("ERROR: Test 19: unexpected error");
end;
end Main;
----------------------------
-- Compilation and output --
----------------------------
$ gnatmake -q -gnata main.adb
$ ./main
Test 1
Test 2
Test 3
Test 4
Test 5
Test 6
Test 7
Test 8
Test 9
Test 10
Test 11
Test 12
Test 13
Test 14
Test 15
Test 16
Test 17
Test 18
Test 19
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-11-12 Hristian Kirtchev <kirtchev@adacore.com>
* contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
Remove the guard concerning entry bodies as it is spurious.
(Analyze_Entry_Or_Subprogram_Contract): Skip the analysis of
Contract_Cases when not annotating the tree.
* einfo.adb Node25 is now used as Contract_Wrapper.
(Contract_Wrapper): New routine.
(PPC_Wrapper): Removed.
(Set_Contract_Wrapper): New routine.
(Set_PPC_Wrapper): Removed.
(Write_Field25_Name): Add output for Contract_Wrapper. Remove
output for PPC_Wrapper.
* einfo.ads New attribute Contract_Wrapper along with usage
in entities. Remove attribute PPC_Wrapper along with usage in nodes.
(Contract_Wrapper): New routine along with pragma Inline.
(PPC_Wrapper): Removed along with pragma Inline.
(Set_Contract_Wrapper): New routine along with pragma Inline.
(Set_PPC_Wrapper): Removed along with pragma Inline.
* exp_ch9.adb (Build_Contract_Wrapper): New routine.
(Build_PPC_Wrapper): Removed.
(Build_Protected_Entry): Code cleanup.
(Expand_Entry_Declaration): Create a contract wrapper
which now verifies Contract_Cases along with pre/postconditions.
(Expand_N_Task_Type_Declaration): There is no need to check
whether an entry has pre/postconditions as this is now done
in Build_Contract_Wrapper.
* sem_ch13.adb (Analyze_Aspect_Specifications): Pragma
Refined_Post is now properly inserted in entry bodies.
(Insert_Pragma): Add circuitry to insert in an entry body. Redo
the instance "header" circuitry. Remove the now obsolete special
case of inserting pre- conditions.
* sem_prag.adb (Analyze_Pragma): Pragma Contract_Cases now
applies to entries.
* sem_res.adb (Resolve_Entry_Call): Update the calls to
PPC_Wrapper.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 48102 bytes --]
Index: exp_ch9.adb
===================================================================
--- exp_ch9.adb (revision 230223)
+++ exp_ch9.adb (working copy)
@@ -128,6 +128,15 @@
-- Build a specification for a function implementing the protected entry
-- barrier of the specified entry body.
+ procedure Build_Contract_Wrapper (E : Entity_Id; Decl : Node_Id);
+ -- Build the body of a wrapper procedure for an entry or entry family that
+ -- has contract cases, preconditions, or postconditions. The body gathers
+ -- the executable contract items and expands them in the usual way, and
+ -- performs the entry call itself. This way preconditions are evaluated
+ -- before the call is queued. E is the entry in question, and Decl is the
+ -- enclosing synchronized type declaration at whose freeze point the
+ -- generated body is analyzed.
+
function Build_Corresponding_Record
(N : Node_Id;
Ctyp : Node_Id;
@@ -197,14 +206,6 @@
-- <formalN> : AnnN;
-- end record;
- procedure Build_PPC_Wrapper (E : Entity_Id; Decl : Node_Id);
- -- Build body of wrapper procedure for an entry or entry family that has
- -- pre/postconditions. The body gathers the PPC's and expands them in the
- -- usual way, and performs the entry call itself. This way preconditions
- -- are evaluated before the call is queued. E is the entry in question,
- -- and Decl is the enclosing synchronized type declaration at whose freeze
- -- point the generated body is analyzed.
-
function Build_Protected_Entry
(N : Node_Id;
Ent : Entity_Id;
@@ -409,7 +410,7 @@
Context_Decls : out List_Id);
-- Subsidiary routine to procedures Build_Activation_Chain_Entity and
-- Build_Master_Entity. Given an arbitrary node in the tree, find the
- -- nearest enclosing body, block, package or return statement and return
+ -- nearest enclosing body, block, package, or return statement and return
-- its constituents. Context is the enclosing construct, Context_Id is
-- the scope of Context_Id and Context_Decls is the declarative list of
-- Context.
@@ -1218,6 +1219,276 @@
Set_Master_Id (Typ, Master_Id);
end Build_Class_Wide_Master;
+ ----------------------------
+ -- Build_Contract_Wrapper --
+ ----------------------------
+
+ procedure Build_Contract_Wrapper (E : Entity_Id; Decl : Node_Id) is
+ Conc_Typ : constant Entity_Id := Scope (E);
+ Loc : constant Source_Ptr := Sloc (E);
+
+ procedure Add_Discriminant_Renamings
+ (Obj_Id : Entity_Id;
+ Decls : List_Id);
+ -- Add renaming declarations for all discriminants of concurrent type
+ -- Conc_Typ. Obj_Id is the entity of the wrapper formal parameter which
+ -- represents the concurrent object.
+
+ procedure Add_Matching_Formals (Formals : List_Id; Actuals : List_Id);
+ -- Add formal parameters that match those of entry E to list Formals.
+ -- The routine also adds matching actuals for the new formals to list
+ -- Actuals.
+
+ procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id);
+ -- Relocate pragma Prag to list To. The routine creates a new list if
+ -- To does not exist.
+
+ --------------------------------
+ -- Add_Discriminant_Renamings --
+ --------------------------------
+
+ procedure Add_Discriminant_Renamings
+ (Obj_Id : Entity_Id;
+ Decls : List_Id)
+ is
+ Discr : Entity_Id;
+
+ begin
+ -- Inspect the discriminants of the concurrent type and generate a
+ -- renaming for each one.
+
+ if Has_Discriminants (Conc_Typ) then
+ Discr := First_Discriminant (Conc_Typ);
+ while Present (Discr) loop
+ Prepend_To (Decls,
+ Make_Object_Renaming_Declaration (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc, Chars (Discr)),
+ Subtype_Mark =>
+ New_Occurrence_Of (Etype (Discr), Loc),
+ Name =>
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Obj_Id, Loc),
+ Selector_Name =>
+ Make_Identifier (Loc, Chars (Discr)))));
+
+ Next_Discriminant (Discr);
+ end loop;
+ end if;
+ end Add_Discriminant_Renamings;
+
+ --------------------------
+ -- Add_Matching_Formals --
+ --------------------------
+
+ procedure Add_Matching_Formals (Formals : List_Id; Actuals : List_Id) is
+ Formal : Entity_Id;
+ New_Formal : Entity_Id;
+
+ begin
+ -- Inspect the formal parameters of the entry and generate a new
+ -- matching formal with the same name for the wrapper. A reference
+ -- to the new formal becomes an actual in the entry call.
+
+ Formal := First_Formal (E);
+ while Present (Formal) loop
+ New_Formal := Make_Defining_Identifier (Loc, Chars (Formal));
+ Append_To (Formals,
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => New_Formal,
+ In_Present => In_Present (Parent (Formal)),
+ Out_Present => Out_Present (Parent (Formal)),
+ Parameter_Type =>
+ New_Occurrence_Of (Etype (Formal), Loc)));
+
+ Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
+ Next_Formal (Formal);
+ end loop;
+ end Add_Matching_Formals;
+
+ ---------------------
+ -- Transfer_Pragma --
+ ---------------------
+
+ procedure Transfer_Pragma (Prag : Node_Id; To : in out List_Id) is
+ New_Prag : Node_Id;
+
+ begin
+ if No (To) then
+ To := New_List;
+ end if;
+
+ New_Prag := Relocate_Node (Prag);
+
+ Set_Analyzed (New_Prag, False);
+ Append (New_Prag, To);
+ end Transfer_Pragma;
+
+ -- Local variables
+
+ Items : constant Node_Id := Contract (E);
+ Actuals : List_Id;
+ Call : Node_Id;
+ Call_Nam : Node_Id;
+ Decls : List_Id := No_List;
+ Formals : List_Id;
+ Has_Pragma : Boolean := False;
+ Index_Id : Entity_Id;
+ Obj_Id : Entity_Id;
+ Prag : Node_Id;
+ Wrapper_Id : Entity_Id;
+
+ -- Start of processing for Build_Contract_Wrapper
+
+ begin
+ -- This routine generates a specialized wrapper for a protected or task
+ -- entry [family] which implements precondition/postcondition semantics.
+ -- Preconditions and case guards of contract cases are checked before
+ -- the protected action or rendezvous takes place. Postconditions and
+ -- consequences of contract cases are checked after the protected action
+ -- or rendezvous takes place. The structure of the generated wrapper is
+ -- as follows:
+
+ -- procedure Wrapper
+ -- (Obj_Id : Conc_Typ; -- concurrent object
+ -- [Index : Index_Typ;] -- index of entry family
+ -- [Formal_1 : ...; -- parameters of original entry
+ -- Formal_N : ...])
+ -- is
+ -- [Discr_1 : ... renames Obj_Id.Discr_1; -- discriminant
+ -- Discr_N : ... renames Obj_Id.Discr_N;] -- renamings
+
+ -- <precondition checks>
+ -- <case guard checks>
+
+ -- procedure _Postconditions is
+ -- begin
+ -- <postcondition checks>
+ -- <consequence checks>
+ -- end _Postconditions;
+
+ -- begin
+ -- Entry_Call (Obj_Id, [Index,] [Formal_1, Formal_N]);
+ -- _Postconditions;
+ -- end Wrapper;
+
+ -- Create the wrapper only when the entry has at least one executable
+ -- contract item such as contract cases, precondition or postcondition.
+
+ if Present (Items) then
+
+ -- Inspect the list of pre/postconditions and transfer all available
+ -- pragmas to the declarative list of the wrapper.
+
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Nam_In (Pragma_Name (Prag), Name_Postcondition,
+ Name_Precondition)
+ then
+ Has_Pragma := True;
+ Transfer_Pragma (Prag, To => Decls);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Inspect the list of test/contract cases and transfer only contract
+ -- cases pragmas to the declarative part of the wrapper.
+
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Contract_Cases then
+ Has_Pragma := True;
+ Transfer_Pragma (Prag, To => Decls);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- The entry lacks executable contract items and a wrapper is not needed
+
+ if not Has_Pragma then
+ return;
+ end if;
+
+ -- Create the profile of the wrapper. The first formal parameter is the
+ -- concurrent object.
+
+ Obj_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Conc_Typ), 'A'));
+
+ Formals := New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Obj_Id,
+ Out_Present => True,
+ In_Present => True,
+ Parameter_Type => New_Occurrence_Of (Conc_Typ, Loc)));
+
+ -- Construct the call to the original entry. The call will be gradually
+ -- augmented with an optional entry index and extra parameters.
+
+ Call_Nam :=
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Obj_Id, Loc),
+ Selector_Name => New_Occurrence_Of (E, Loc));
+
+ -- When creating a wrapper for an entry family, the second formal is the
+ -- entry index.
+
+ if Ekind (E) = E_Entry_Family then
+ Index_Id := Make_Defining_Identifier (Loc, Name_I);
+
+ Append_To (Formals,
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Index_Id,
+ Parameter_Type =>
+ New_Occurrence_Of (Entry_Index_Type (E), Loc)));
+
+ -- The call to the original entry becomes an indexed component to
+ -- accommodate the entry index.
+
+ Call_Nam :=
+ Make_Indexed_Component (Loc,
+ Prefix => Call_Nam,
+ Expressions => New_List (New_Occurrence_Of (Index_Id, Loc)));
+ end if;
+
+ Actuals := New_List;
+ Call :=
+ Make_Procedure_Call_Statement (Loc,
+ Name => Call_Nam,
+ Parameter_Associations => Actuals);
+
+ -- Add formal parameters to match those of the entry and build actuals
+ -- for the entry call.
+
+ Add_Matching_Formals (Formals, Actuals);
+
+ -- Add renaming declarations for the discriminants of the enclosing type
+ -- as the various contract items may reference them.
+
+ Add_Discriminant_Renamings (Obj_Id, Decls);
+
+ Wrapper_Id :=
+ Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
+ Set_Contract_Wrapper (E, Wrapper_Id);
+
+ -- The wrapper body is analyzed when the enclosing type is frozen
+
+ Append_Freeze_Action (Defining_Entity (Decl),
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Wrapper_Id,
+ Parameter_Specifications => Formals),
+ Declarations => Decls,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (Call))));
+ end Build_Contract_Wrapper;
+
--------------------------------
-- Build_Corresponding_Record --
--------------------------------
@@ -1925,166 +2196,6 @@
return Decl;
end Build_Renamed_Formal_Declaration;
- -----------------------
- -- Build_PPC_Wrapper --
- -----------------------
-
- procedure Build_PPC_Wrapper (E : Entity_Id; Decl : Node_Id) is
- Items : constant Node_Id := Contract (E);
- Loc : constant Source_Ptr := Sloc (E);
- Synch_Type : constant Entity_Id := Scope (E);
- Actuals : List_Id;
- Decls : List_Id;
- Entry_Call : Node_Id;
- Entry_Name : Node_Id;
- Params : List_Id;
- Prag : Node_Id;
- Synch_Id : Entity_Id;
- Wrapper_Id : Entity_Id;
-
- begin
- -- Only build the wrapper if entry has pre/postconditions
- -- Should this be done unconditionally instead ???
-
- if Present (Items) then
- Prag := Pre_Post_Conditions (Items);
-
- if No (Prag) then
- return;
- end if;
-
- -- Transfer ppc pragmas to the declarations of the wrapper
-
- Decls := New_List;
-
- while Present (Prag) loop
- if Nam_In (Pragma_Name (Prag), Name_Precondition,
- Name_Postcondition)
- then
- Append (Relocate_Node (Prag), Decls);
- Set_Analyzed (Last (Decls), False);
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- else
- return;
- end if;
-
- Actuals := New_List;
- Synch_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Scope (E)), 'A'));
-
- -- First formal is synchronized object
-
- Params := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Synch_Id,
- Out_Present => True,
- In_Present => True,
- Parameter_Type => New_Occurrence_Of (Scope (E), Loc)));
-
- Entry_Name :=
- Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Synch_Id, Loc),
- Selector_Name => New_Occurrence_Of (E, Loc));
-
- -- If entity is entry family, second formal is the corresponding index,
- -- and entry name is an indexed component.
-
- if Ekind (E) = E_Entry_Family then
- declare
- Index : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_I);
- begin
- Append_To (Params,
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Index,
- Parameter_Type =>
- New_Occurrence_Of (Entry_Index_Type (E), Loc)));
-
- Entry_Name :=
- Make_Indexed_Component (Loc,
- Prefix => Entry_Name,
- Expressions => New_List (New_Occurrence_Of (Index, Loc)));
- end;
- end if;
-
- Entry_Call :=
- Make_Procedure_Call_Statement (Loc,
- Name => Entry_Name,
- Parameter_Associations => Actuals);
-
- -- Now add formals that match those of the entry, and build actuals for
- -- the nested entry call.
-
- declare
- Form : Entity_Id;
- New_Form : Entity_Id;
- Parm_Spec : Node_Id;
-
- begin
- Form := First_Formal (E);
- while Present (Form) loop
- New_Form := Make_Defining_Identifier (Loc, Chars (Form));
- Parm_Spec :=
- Make_Parameter_Specification (Loc,
- Defining_Identifier => New_Form,
- Out_Present => Out_Present (Parent (Form)),
- In_Present => In_Present (Parent (Form)),
- Parameter_Type => New_Occurrence_Of (Etype (Form), Loc));
-
- Append (Parm_Spec, Params);
- Append (New_Occurrence_Of (New_Form, Loc), Actuals);
- Next_Formal (Form);
- end loop;
- end;
-
- -- Add renaming declarations for the discriminants of the enclosing
- -- type, which may be visible in the preconditions.
-
- if Has_Discriminants (Synch_Type) then
- declare
- D : Entity_Id;
- Decl : Node_Id;
-
- begin
- D := First_Discriminant (Synch_Type);
- while Present (D) loop
- Decl :=
- Make_Object_Renaming_Declaration (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc, Chars (D)),
- Subtype_Mark => New_Occurrence_Of (Etype (D), Loc),
- Name =>
- Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Synch_Id, Loc),
- Selector_Name => Make_Identifier (Loc, Chars (D))));
- Prepend (Decl, Decls);
- Next_Discriminant (D);
- end loop;
- end;
- end if;
-
- Wrapper_Id :=
- Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
- Set_PPC_Wrapper (E, Wrapper_Id);
-
- -- The wrapper body is analyzed when the enclosing type is frozen
-
- Append_Freeze_Action (Defining_Entity (Decl),
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Wrapper_Id,
- Parameter_Specifications => Params),
- Declarations => Decls,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (Entry_Call))));
- end Build_PPC_Wrapper;
-
--------------------------
-- Build_Wrapper_Bodies --
--------------------------
@@ -3214,7 +3325,7 @@
-- Start of processing for Build_Lock_Free_Unprotected_Subprogram_Body
begin
- -- Add renamings for the protection object, discriminals, privals and
+ -- Add renamings for the protection object, discriminals, privals, and
-- the entry index constant for use by debugger.
Debug_Private_Data_Declarations (Decls);
@@ -3619,7 +3730,7 @@
Decls := List_Containing (Context);
-- Default case for object declarations and access types. Note that the
- -- context is updated to the nearest enclosing body, block, package or
+ -- context is updated to the nearest enclosing body, block, package, or
-- return statement.
else
@@ -3810,43 +3921,42 @@
Ent : Entity_Id;
Pid : Node_Id) return Node_Id
is
+ Bod_Decls : constant List_Id := New_List;
+ Decls : constant List_Id := Declarations (N);
+ End_Lab : constant Node_Id :=
+ End_Label (Handled_Statement_Sequence (N));
+ End_Loc : constant Source_Ptr :=
+ Sloc (Last (Statements (Handled_Statement_Sequence (N))));
+ -- Used for the generated call to Complete_Entry_Body
+
Loc : constant Source_Ptr := Sloc (N);
- Decls : constant List_Id := Declarations (N);
- End_Lab : constant Node_Id :=
- End_Label (Handled_Statement_Sequence (N));
- End_Loc : constant Source_Ptr :=
- Sloc (Last (Statements (Handled_Statement_Sequence (N))));
- -- Used for the generated call to Complete_Entry_Body
+ Bod_Id : Entity_Id;
+ Bod_Spec : Node_Id;
+ Bod_Stmts : List_Id;
+ Complete : Node_Id;
+ Ohandle : Node_Id;
- Han_Loc : Source_Ptr;
+ EH_Loc : Source_Ptr;
-- Used for the exception handler, inserted at end of the body
- Op_Decls : constant List_Id := New_List;
- Complete : Node_Id;
- Edef : Entity_Id;
- Espec : Node_Id;
- Ohandle : Node_Id;
- Op_Stats : List_Id;
-
begin
-- Set the source location on the exception handler only when debugging
-- the expanded code (see Make_Implicit_Exception_Handler).
if Debug_Generated_Code then
- Han_Loc := End_Loc;
+ EH_Loc := End_Loc;
-- Otherwise the inserted code should not be visible to the debugger
else
- Han_Loc := No_Location;
+ EH_Loc := No_Location;
end if;
- Edef :=
+ Bod_Id :=
Make_Defining_Identifier (Loc,
Chars => Chars (Protected_Body_Subprogram (Ent)));
- Espec :=
- Build_Protected_Entry_Specification (Loc, Edef, Empty);
+ Bod_Spec := Build_Protected_Entry_Specification (Loc, Bod_Id, Empty);
-- Add the following declarations:
@@ -3856,26 +3966,25 @@
-- where _O is the formal parameter associated with the concurrent
-- object. These declarations are needed for Complete_Entry_Body.
- Add_Object_Pointer (Loc, Pid, Op_Decls);
+ Add_Object_Pointer (Loc, Pid, Bod_Decls);
-- Add renamings for all formals, the Protection object, discriminals,
-- privals and the entry index constant for use by debugger.
- Add_Formal_Renamings (Espec, Op_Decls, Ent, Loc);
+ Add_Formal_Renamings (Bod_Spec, Bod_Decls, Ent, Loc);
Debug_Private_Data_Declarations (Decls);
-- Put the declarations and the statements from the entry
- Op_Stats :=
+ Bod_Stmts :=
New_List (
Make_Block_Statement (Loc,
- Declarations => Decls,
- Handled_Statement_Sequence =>
- Handled_Statement_Sequence (N)));
+ Declarations => Decls,
+ Handled_Statement_Sequence => Handled_Statement_Sequence (N)));
case Corresponding_Runtime_Package (Pid) is
when System_Tasking_Protected_Objects_Entries =>
- Append_To (Op_Stats,
+ Append_To (Bod_Stmts,
Make_Procedure_Call_Statement (End_Loc,
Name =>
New_Occurrence_Of (RTE (RE_Complete_Entry_Body), Loc),
@@ -3901,16 +4010,16 @@
end case;
-- When exceptions can not be propagated, we never need to call
- -- Exception_Complete_Entry_Body
+ -- Exception_Complete_Entry_Body.
if No_Exception_Handlers_Set then
return
Make_Subprogram_Body (Loc,
- Specification => Espec,
- Declarations => Op_Decls,
+ Specification => Bod_Spec,
+ Declarations => Bod_Decls,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Op_Stats,
+ Statements => Bod_Stmts,
End_Label => End_Lab));
else
@@ -3934,39 +4043,40 @@
-- Establish link between subprogram body entity and source entry
- Set_Corresponding_Protected_Entry (Edef, Ent);
+ Set_Corresponding_Protected_Entry (Bod_Id, Ent);
-- Create body of entry procedure. The renaming declarations are
-- placed ahead of the block that contains the actual entry body.
return
Make_Subprogram_Body (Loc,
- Specification => Espec,
- Declarations => Op_Decls,
+ Specification => Bod_Spec,
+ Declarations => Bod_Decls,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Op_Stats,
- End_Label => End_Lab,
+ Statements => Bod_Stmts,
+ End_Label => End_Lab,
Exception_Handlers => New_List (
- Make_Implicit_Exception_Handler (Han_Loc,
+ Make_Implicit_Exception_Handler (EH_Loc,
Exception_Choices => New_List (Ohandle),
- Statements => New_List (
- Make_Procedure_Call_Statement (Han_Loc,
- Name => Complete,
+ Statements => New_List (
+ Make_Procedure_Call_Statement (EH_Loc,
+ Name => Complete,
Parameter_Associations => New_List (
- Make_Attribute_Reference (Han_Loc,
- Prefix =>
- Make_Selected_Component (Han_Loc,
+ Make_Attribute_Reference (EH_Loc,
+ Prefix =>
+ Make_Selected_Component (EH_Loc,
Prefix =>
- Make_Identifier (Han_Loc, Name_uObject),
+ Make_Identifier (EH_Loc, Name_uObject),
Selector_Name =>
- Make_Identifier (Han_Loc, Name_uObject)),
- Attribute_Name => Name_Unchecked_Access),
+ Make_Identifier (EH_Loc, Name_uObject)),
+ Attribute_Name => Name_Unchecked_Access),
- Make_Function_Call (Han_Loc,
- Name => New_Occurrence_Of (
- RTE (RE_Get_GNAT_Exception), Loc)))))))));
+ Make_Function_Call (EH_Loc,
+ Name =>
+ New_Occurrence_Of
+ (RTE (RE_Get_GNAT_Exception), Loc)))))))));
end if;
end Build_Protected_Entry;
@@ -5302,7 +5412,7 @@
Decls : constant List_Id := Declarations (N);
begin
- -- Add renamings for the Protection object, discriminals, privals and
+ -- Add renamings for the Protection object, discriminals, privals, and
-- the entry index constant for use by debugger.
Debug_Private_Data_Declarations (Decls);
@@ -5666,7 +5776,7 @@
if Nkind_In (Decl, N_Full_Type_Declaration, N_Object_Declaration) then
Set_Debug_Info_Needed (Defining_Identifier (Decl));
- -- Declaration for the Protection object, discriminals, privals and
+ -- Declaration for the Protection object, discriminals, privals, and
-- entry index constant:
-- conc_typR : protection_typ renames _object._object;
-- discr_nameD : discr_typ renames _object.discr_name;
@@ -9007,9 +9117,10 @@
Insert_After (Current_Node, Sub);
Analyze (Sub);
- -- Build wrapper procedure for pre/postconditions
+ -- Build a wrapper procedure to handle contract cases, preconditions,
+ -- and postconditions.
- Build_PPC_Wrapper (Comp_Id, N);
+ Build_Contract_Wrapper (Comp_Id, N);
Set_Protected_Body_Subprogram
(Defining_Identifier (Comp),
@@ -12113,7 +12224,8 @@
Expand_Previous_Access_Type (Tasktyp);
- -- Create wrappers for entries that have pre/postconditions
+ -- Create wrappers for entries that have contract cases, preconditions
+ -- and postconditions.
declare
Ent : Entity_Id;
@@ -12121,11 +12233,8 @@
begin
Ent := First_Entity (Tasktyp);
while Present (Ent) loop
- if Ekind_In (Ent, E_Entry, E_Entry_Family)
- and then Present (Contract (Ent))
- and then Present (Pre_Post_Conditions (Contract (Ent)))
- then
- Build_PPC_Wrapper (Ent, N);
+ if Ekind_In (Ent, E_Entry, E_Entry_Family) then
+ Build_Contract_Wrapper (Ent, N);
end if;
Next_Entity (Ent);
Index: einfo.adb
===================================================================
--- einfo.adb (revision 230223)
+++ einfo.adb (working copy)
@@ -216,11 +216,11 @@
-- Related_Expression Node24
-- Subps_Index Uint24
+ -- Contract_Wrapper Node25
-- Debug_Renaming_Link Node25
-- DT_Offset_To_Top_Func Node25
-- Interface_Alias Node25
-- Interfaces Elist25
- -- PPC_Wrapper Node25
-- Related_Array_Object Node25
-- Static_Discrete_Predicate List25
-- Static_Real_Or_String_Predicate Node25
@@ -1231,6 +1231,12 @@
return Node34 (Id);
end Contract;
+ function Contract_Wrapper (Id : E) return E is
+ begin
+ pragma Assert (Ekind_In (Id, E_Entry, E_Entry_Family));
+ return Node25 (Id);
+ end Contract_Wrapper;
+
function Entry_Parameters_Type (Id : E) return E is
begin
return Node15 (Id);
@@ -2876,12 +2882,6 @@
return Node14 (Id);
end Postconditions_Proc;
- function PPC_Wrapper (Id : E) return E is
- begin
- pragma Assert (Ekind_In (Id, E_Entry, E_Entry_Family));
- return Node25 (Id);
- end PPC_Wrapper;
-
function Prival (Id : E) return E is
begin
pragma Assert (Is_Protected_Component (Id));
@@ -3877,6 +3877,12 @@
Set_Node34 (Id, V);
end Set_Contract;
+ procedure Set_Contract_Wrapper (Id : E; V : E) is
+ begin
+ pragma Assert (Ekind_In (Id, E_Entry, E_Entry_Family));
+ Set_Node25 (Id, V);
+ end Set_Contract_Wrapper;
+
procedure Set_Corresponding_Concurrent_Type (Id : E; V : E) is
begin
pragma Assert
@@ -5912,12 +5918,6 @@
Set_Node14 (Id, V);
end Set_Postconditions_Proc;
- procedure Set_PPC_Wrapper (Id : E; V : E) is
- begin
- pragma Assert (Ekind_In (Id, E_Entry, E_Entry_Family));
- Set_Node25 (Id, V);
- end Set_PPC_Wrapper;
-
procedure Set_Direct_Primitive_Operations (Id : E; V : L) is
begin
pragma Assert (Is_Tagged_Type (Id));
@@ -10003,6 +10003,10 @@
E_Package =>
Write_Str ("Abstract_States");
+ when E_Entry |
+ E_Entry_Family =>
+ Write_Str ("Contract_Wrapper");
+
when E_Variable =>
Write_Str ("Debug_Renaming_Link");
@@ -10026,10 +10030,6 @@
when Task_Kind =>
Write_Str ("Task_Body_Procedure");
- when E_Entry |
- E_Entry_Family =>
- Write_Str ("PPC_Wrapper");
-
when Discrete_Kind =>
Write_Str ("Static_Discrete_Predicate");
Index: einfo.ads
===================================================================
--- einfo.ads (revision 230229)
+++ einfo.ads (working copy)
@@ -714,6 +714,12 @@
-- variable and task type entities. Points to the contract of the entity,
-- holding various assertion items and data classifiers.
+-- Contract_Wrapper (Node25)
+-- Defined in entry and entry family entities. Set only when the entry
+-- [family] has contract cases, preconditions, and/or postconditions.
+-- Contains the entity of a wrapper procedure which encapsulates the
+-- original entry and implements precondition/postcondition semantics.
+
-- Corresponding_Concurrent_Type (Node18)
-- Defined in record types that are constructed by the expander to
-- represent task and protected types (Is_Concurrent_Record_Type flag
@@ -3639,7 +3645,7 @@
-- Overlays_Constant (Flag243)
-- Defined in all entities. Set only for E_Constant or E_Variable for
--- which there is an address clause which causes the entity to overlay
+-- which there is an address clause that causes the entity to overlay
-- a constant object.
-- Overridden_Operation (Node26)
@@ -3707,11 +3713,6 @@
-- to the entity of the _Postconditions procedure used to check contract
-- assertions on exit from a subprogram.
--- PPC_Wrapper (Node25)
--- Defined in entries and entry families. Set only if pre- or post-
--- conditions are present. The precondition_wrapper body is the original
--- entry call, decorated with the given precondition for the entry.
-
-- Predicate_Function (synthesized)
-- Defined in all types. Set for types for which (Has_Predicates is True)
-- and for which a predicate procedure has been built that tests that the
@@ -5758,7 +5759,7 @@
-- Accept_Address (Elist21)
-- Scope_Depth_Value (Uint22)
-- Protection_Object (Node23) (protected kind)
- -- PPC_Wrapper (Node25)
+ -- Contract_Wrapper (Node25)
-- Extra_Formals (Node28)
-- Contract (Node34)
-- SPARK_Pragma (Node40) (protected kind)
@@ -6751,6 +6752,7 @@
function Component_Type (Id : E) return E;
function Contains_Ignored_Ghost_Code (Id : E) return B;
function Contract (Id : E) return N;
+ function Contract_Wrapper (Id : E) return E;
function Corresponding_Concurrent_Type (Id : E) return E;
function Corresponding_Discriminant (Id : E) return E;
function Corresponding_Equality (Id : E) return E;
@@ -7089,7 +7091,6 @@
function Partial_View_Has_Unknown_Discr (Id : E) return B;
function Pending_Access_Types (Id : E) return L;
function Postconditions_Proc (Id : E) return E;
- function PPC_Wrapper (Id : E) return E;
function Prival (Id : E) return E;
function Prival_Link (Id : E) return E;
function Private_Dependents (Id : E) return L;
@@ -7415,6 +7416,7 @@
procedure Set_Component_Type (Id : E; V : E);
procedure Set_Contains_Ignored_Ghost_Code (Id : E; V : B := True);
procedure Set_Contract (Id : E; V : N);
+ procedure Set_Contract_Wrapper (Id : E; V : E);
procedure Set_Corresponding_Concurrent_Type (Id : E; V : E);
procedure Set_Corresponding_Discriminant (Id : E; V : E);
procedure Set_Corresponding_Equality (Id : E; V : E);
@@ -7756,7 +7758,6 @@
procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True);
procedure Set_Pending_Access_Types (Id : E; V : L);
procedure Set_Postconditions_Proc (Id : E; V : E);
- procedure Set_PPC_Wrapper (Id : E; V : E);
procedure Set_Prival (Id : E; V : E);
procedure Set_Prival_Link (Id : E; V : E);
procedure Set_Private_Dependents (Id : E; V : L);
@@ -8194,6 +8195,7 @@
pragma Inline (Component_Type);
pragma Inline (Contains_Ignored_Ghost_Code);
pragma Inline (Contract);
+ pragma Inline (Contract_Wrapper);
pragma Inline (Corresponding_Concurrent_Type);
pragma Inline (Corresponding_Discriminant);
pragma Inline (Corresponding_Equality);
@@ -8578,7 +8580,6 @@
pragma Inline (Partial_View_Has_Unknown_Discr);
pragma Inline (Pending_Access_Types);
pragma Inline (Postconditions_Proc);
- pragma Inline (PPC_Wrapper);
pragma Inline (Prival);
pragma Inline (Prival_Link);
pragma Inline (Private_Dependents);
@@ -8702,6 +8703,7 @@
pragma Inline (Set_Component_Type);
pragma Inline (Set_Contains_Ignored_Ghost_Code);
pragma Inline (Set_Contract);
+ pragma Inline (Set_Contract_Wrapper);
pragma Inline (Set_Corresponding_Concurrent_Type);
pragma Inline (Set_Corresponding_Discriminant);
pragma Inline (Set_Corresponding_Equality);
@@ -9039,7 +9041,6 @@
pragma Inline (Set_Partial_View_Has_Unknown_Discr);
pragma Inline (Set_Pending_Access_Types);
pragma Inline (Set_Postconditions_Proc);
- pragma Inline (Set_PPC_Wrapper);
pragma Inline (Set_Prival);
pragma Inline (Set_Prival_Link);
pragma Inline (Set_Private_Dependents);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 230223)
+++ sem_prag.adb (working copy)
@@ -12670,9 +12670,14 @@
Subp_Decl :=
Find_Related_Declaration_Or_Body (N, Do_Checks => True);
+ -- Entry
+
+ if Nkind (Subp_Decl) = N_Entry_Declaration then
+ null;
+
-- Generic subprogram
- if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
null;
-- Body acts as spec
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 230223)
+++ sem_res.adb (working copy)
@@ -7577,8 +7577,8 @@
end if;
if Ekind_In (Nam, E_Entry, E_Entry_Family)
- and then Present (PPC_Wrapper (Nam))
- and then Current_Scope /= PPC_Wrapper (Nam)
+ and then Present (Contract_Wrapper (Nam))
+ and then Current_Scope /= Contract_Wrapper (Nam)
then
-- Rewrite as call to the precondition wrapper, adding the task
-- object to the list of actuals. If the call is to a member of an
@@ -7600,7 +7600,7 @@
New_Call :=
Make_Procedure_Call_Statement (Loc,
Name =>
- New_Occurrence_Of (PPC_Wrapper (Nam), Loc),
+ New_Occurrence_Of (Contract_Wrapper (Nam), Loc),
Parameter_Associations => New_Actuals);
Rewrite (N, New_Call);
Index: contracts.adb
===================================================================
--- contracts.adb (revision 230223)
+++ contracts.adb (working copy)
@@ -366,17 +366,6 @@
if Ekind (Body_Id) = E_Void then
return;
- -- Do not analyze the contract of an entry body unless annotating the
- -- original tree. It is preferable to analyze the contract after the
- -- entry body has been transformed into a subprogram body to properly
- -- handle references to unpacked formals.
-
- elsif Ekind_In (Body_Id, E_Entry, E_Entry_Family)
- and then not ASIS_Mode
- and then not GNATprove_Mode
- then
- return;
-
-- Do not analyze a contract multiple times
elsif Present (Items) then
@@ -442,12 +431,18 @@
procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id) is
Items : constant Node_Id := Contract (Subp_Id);
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
- Depends : Node_Id := Empty;
- Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Prag_Nam : Name_Id;
+ Skip_Assert_Exprs : constant Boolean :=
+ Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
+ and then not ASIS_Mode
+ and then not GNATprove_Mode;
+
+ Depends : Node_Id := Empty;
+ Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+
begin
-- Do not analyze a contract multiple times
@@ -475,17 +470,11 @@
elsif Present (Items) then
-- Do not analyze the pre/postconditions of an entry declaration
- -- unless annotating the original tree for ASIS or GNATprove.
+ -- unless annotating the original tree for ASIS or GNATprove. The
+ -- real analysis occurs when the pre/postconditons are relocated to
+ -- the contract wrapper procedure (see Build_Contract_Wrapper).
- -- ??? References to formals are causing problems during contract
- -- expansion as the references resolve to the entry formals, not
- -- the subprogram body emulating the entry body. This will have to
- -- be addressed.
-
- if Ekind_In (Subp_Id, E_Entry, E_Entry_Family)
- and then not ASIS_Mode
- and then not GNATprove_Mode
- then
+ if Skip_Assert_Exprs then
null;
-- Otherwise analyze the pre/postconditions
@@ -505,7 +494,20 @@
Prag_Nam := Pragma_Name (Prag);
if Prag_Nam = Name_Contract_Cases then
- Analyze_Contract_Cases_In_Decl_Part (Prag);
+
+ -- Do not analyze the contract cases of an entry declaration
+ -- unless annotating the original tree for ASIS or GNATprove.
+ -- The real analysis occurs when the contract cases are moved
+ -- to the contract wrapper procedure (Build_Contract_Wrapper).
+
+ if Skip_Assert_Exprs then
+ null;
+
+ -- Otherwise analyze the contract cases
+
+ else
+ Analyze_Contract_Cases_In_Decl_Part (Prag);
+ end if;
else
pragma Assert (Prag_Nam = Name_Test_Case);
Analyze_Test_Case_In_Decl_Part (Prag);
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 230235)
+++ sem_ch13.adb (working copy)
@@ -1251,22 +1251,25 @@
(Prag : Node_Id;
Is_Instance : Boolean := False)
is
- Aux : Node_Id;
- Decl : Node_Id;
- Decls : List_Id;
- Def : Node_Id;
+ Aux : Node_Id;
+ Decl : Node_Id;
+ Decls : List_Id;
+ Def : Node_Id;
+ Inserted : Boolean := False;
begin
- -- When the aspect appears on a package, protected unit, subprogram
- -- or task unit body, insert the generated pragma at the top of the
- -- body declarations to emulate the behavior of a source pragma.
+ -- When the aspect appears on an entry, package, protected unit,
+ -- subprogram, or task unit body, insert the generated pragma at the
+ -- top of the body declarations to emulate the behavior of a source
+ -- pragma.
-- package body Pack with Aspect is
-- package body Pack is
-- pragma Prag;
- if Nkind_In (N, N_Package_Body,
+ if Nkind_In (N, N_Entry_Body,
+ N_Package_Body,
N_Protected_Body,
N_Subprogram_Body,
N_Task_Body)
@@ -1278,36 +1281,8 @@
Set_Declarations (N, Decls);
end if;
- -- Skip other internally generated pragmas from aspects to find
- -- the proper insertion point. As a result the order of pragmas
- -- is the same as the order of aspects.
+ Prepend_To (Decls, Prag);
- -- As precondition pragmas generated from conjuncts in the
- -- precondition aspect are presented in reverse order to
- -- Insert_Pragma, insert them in the correct order here by not
- -- skipping previously inserted precondition pragmas when the
- -- current pragma is a precondition.
-
- Decl := First (Decls);
- while Present (Decl) loop
- if Nkind (Decl) = N_Pragma
- and then From_Aspect_Specification (Decl)
- and then not (Get_Pragma_Id (Decl) = Pragma_Precondition
- and then
- Get_Pragma_Id (Prag) = Pragma_Precondition)
- then
- Next (Decl);
- else
- exit;
- end if;
- end loop;
-
- if Present (Decl) then
- Insert_Before (Decl, Prag);
- else
- Append_To (Decls, Prag);
- end if;
-
-- When the aspect is associated with a [generic] package declaration
-- insert the generated pragma at the top of the visible declarations
-- to emulate the behavior of a source pragma.
@@ -1335,23 +1310,24 @@
-- <first source declaration>
-- Insert the pragma before the first source declaration by
- -- skipping the instance "header".
+ -- skipping the instance "header" to ensure proper visibility of
+ -- all formals.
if Is_Instance then
Decl := First (Decls);
- while Present (Decl) and then not Comes_From_Source (Decl) loop
- Decl := Next (Decl);
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ Insert_Before (Decl, Prag);
+ Inserted := True;
+ exit;
+ else
+ Next (Decl);
+ end if;
end loop;
- -- The instance "header" is followed by at least one source
- -- declaration.
+ -- The pragma is placed after the instance "header"
- if Present (Decl) then
- Insert_Before (Decl, Prag);
-
- -- Otherwise the pragma is placed after the instance "header"
-
- else
+ if not Inserted then
Append_To (Decls, Prag);
end if;
@@ -2770,6 +2746,10 @@
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_Post);
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
-- Refined_State
when Aspect_Refined_State =>
@@ -4748,7 +4728,7 @@
-- Overlaying controlled objects is erroneous. Emit warning
-- but continue analysis because program is itself legal,
- -- and back-end must see address clause.
+ -- and back end must see address clause.
if Present (O_Ent)
and then (Has_Controlled_Component (Etype (O_Ent))
@@ -6587,7 +6567,7 @@
-- In ASIS_Mode mode, expansion is disabled, but we must convert
-- the Mod clause into an alignment clause anyway, so that the
- -- back-end can compute and back-annotate properly the size and
+ -- back end can compute and back-annotate properly the size and
-- alignment of types that may include this record.
-- This seems dubious, this destroys the source tree in a manner
@@ -13048,7 +13028,7 @@
end loop;
-- Reset homonym link of other entities, but do not modify link
- -- between entities in current scope, so that the back-end can
+ -- between entities in current scope, so that the back end can
-- have a proper count of local overloadings.
if No (Prev) then
@@ -13643,7 +13623,7 @@
-- Make entry in unchecked conversion table for later processing by
-- Validate_Unchecked_Conversions, which will check sizes and alignments
- -- (using values set by the back-end where possible). This is only done
+ -- (using values set by the back end where possible). This is only done
-- if the appropriate warning is active.
if Warn_On_Unchecked_Conversion then
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2015-11-12 11:15 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2015-11-12 11:15 [Ada] Contract_Cases on entries Arnaud Charlet
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).