diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2013-10-10 12:35:07 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2013-10-10 12:35:07 +0000 |
| commit | 4befb1a023b3eaa917101fe5eeb699d51f501762 (patch) | |
| tree | 5033b93dc220ac16f90eeba1b770e74614c9d3e3 | |
| parent | be9124d0a1202dff2afe8d88f3511647f485e1ea (diff) | |
| download | ppe42-gcc-4befb1a023b3eaa917101fe5eeb699d51f501762.tar.gz ppe42-gcc-4befb1a023b3eaa917101fe5eeb699d51f501762.zip | |
2013-10-10 Hristian Kirtchev <kirtchev@adacore.com>
* aspects.adb: Add entries in table Canonical_Aspects for aspects
Refined_Depends and Refined_Global.
* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
Aspect_Names, Aspect_Declay, Aspect_On_Body_Or_Stub_OK for
aspects Refined_Depends and Refined_Global.
* einfo.adb (Contract): Subprogram bodies are now valid owners
of contracts.
(Set_Contract): Subprogram bodies are now valid
owners of contracts.
(Write_Field24_Name): Output the contract
attribute for subprogram bodies.
* exp_ch6.adb (Expand_Subprogram_Contract): New routine.
* exp_ch6.ads (Expand_Subprogram_Contract): New routine.
* par-prag.adb: Pragmas Refined_Depends and Refined_Global do
not require any special processing by the parser.
* sem_ch3.adb (Adjust_D): Renamed to Adjust_Decl.
(Analyze_Declarations): Code reformatting. Analyze the contract
of a subprogram body at the end of the declarative region.
* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
Subprogram bodies can now have contracts. Use
Expand_Subprogram_Contract to handle the various contract
assertions.
(Analyze_Subprogram_Body_Contract): New null routine.
(Analyze_Subprogram_Body_Helper): Subprogram bodies can now have
contracts. Use Expand_Subprogram_Contract to handle the various
contract assertions.
(Analyze_Subprogram_Contract): Add local
variable Nam. Update the call to Analyze_PPC_In_Decl_Part. Capture
the pragma name in Nam.
(Process_PPCs): Removed.
* sem_ch6.ads (Analyze_Subprogram_Body_Contract): New routine.
(Analyze_Subprogram_Contract): Update the comment on usage.
* sem_ch13.adb (Analyze_Aspect_Specifications): Add null
implementations for aspects Refined_Depends and Refined_Global.
(Check_Aspect_At_Freeze_Point): Aspects Refined_Depends and
Refined_Global do not need to be checked at the freeze point.
* sem_prag.adb: Add entries in table Sig_Flags
for pragmas Refined_Depends and Refined_Global.
(Analyze_Contract_Cases_In_Decl_Part): Add local
variable Restore. Use Restore to pop the scope.
(Analyze_Depends_In_Decl_Part): Add local variable Restore. Use
Restore to pop the scope.
(Analyze_Global_In_Decl_List): Add local variable Restore. Use Restore
to pop the scope.
(Analyze_PPC_In_Decl_Part): Renamed to
Analyze_Pre_Post_Condition_In_Decl_Part.
(Analyze_Pragma):
Add null implementations for pragmas Refined_Depends and
Refined_Global. Refined_Pre and Refined_Post are now
handled by routine Analyze_Refined_Pre_Post_Condition
exclusively.
(Analyze_Refined_Depends_In_Decl_Part): New
null routine.
(Analyze_Refined_Global_In_Decl_Part):
New null routine.
(Analyze_Refined_Pre_Post):
Renamed to Analyze_Refined_Pre_Post_Condition.
(Analyze_Refined_Pre_Post_Condition): Analyze the boolean
expression.
(Check_Precondition_Postcondition): Update the call
to Analyze_PPC_In_Decl_Part.
* sem_prag.ads: Add entries in table
Pragma_On_Body_Or_Stub_OK for pragmas Refined_Depends
and Refined_Global.
(Analyze_PPC_In_Decl_Part): Renamed
to Analyze_Pre_Post_Condition_In_Decl_Part. Update the
comment on usage.
(Analyze_Refined_Depends_In_Decl_Part): New routine.
(Analyze_Refined_Global_In_Decl_Part): New routine.
(Analyze_Test_Case_In_Decl_Part): Update the comment on usage.
* sem_util.adb (Add_Contract_Item): Rename formal Item to Prag
and update all occurrences. Subprogram body contracts can now
contain pragmas Refined_Depends and Refined_Global.
* sem_util.ads (Add_Contract_Item): Rename formal Item to
Prag. Update the comment on usage.
* sinfo.ads: Update the comment on structure and usage of
N_Contract.
* snames.ads-tmpl: Add new predefined names for Refined_Depends
and Refined_Global. Add entries in table Pragma_Id for
Refined_Depends and Refined_Global.
2013-10-10 Robert Dewar <dewar@adacore.com>
* types.ads: Minor reformatting.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@203365 138bc75d-0d04-0410-961f-82ee72b054a4
| -rw-r--r-- | gcc/ada/ChangeLog | 87 | ||||
| -rw-r--r-- | gcc/ada/aspects.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/aspects.ads | 12 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 9 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.adb | 1044 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.ads | 12 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 94 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 925 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.ads | 14 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 485 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 44 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 44 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 15 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 18 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 4 | ||||
| -rw-r--r-- | gcc/ada/types.ads | 2 |
18 files changed, 1598 insertions, 1231 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1526c73960e..ce65c67ceaa 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,90 @@ +2013-10-10 Hristian Kirtchev <kirtchev@adacore.com> + + * aspects.adb: Add entries in table Canonical_Aspects for aspects + Refined_Depends and Refined_Global. + * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument, + Aspect_Names, Aspect_Declay, Aspect_On_Body_Or_Stub_OK for + aspects Refined_Depends and Refined_Global. + * einfo.adb (Contract): Subprogram bodies are now valid owners + of contracts. + (Set_Contract): Subprogram bodies are now valid + owners of contracts. + (Write_Field24_Name): Output the contract + attribute for subprogram bodies. + * exp_ch6.adb (Expand_Subprogram_Contract): New routine. + * exp_ch6.ads (Expand_Subprogram_Contract): New routine. + * par-prag.adb: Pragmas Refined_Depends and Refined_Global do + not require any special processing by the parser. + * sem_ch3.adb (Adjust_D): Renamed to Adjust_Decl. + (Analyze_Declarations): Code reformatting. Analyze the contract + of a subprogram body at the end of the declarative region. + * sem_ch6.adb (Analyze_Generic_Subprogram_Body): + Subprogram bodies can now have contracts. Use + Expand_Subprogram_Contract to handle the various contract + assertions. + (Analyze_Subprogram_Body_Contract): New null routine. + (Analyze_Subprogram_Body_Helper): Subprogram bodies can now have + contracts. Use Expand_Subprogram_Contract to handle the various + contract assertions. + (Analyze_Subprogram_Contract): Add local + variable Nam. Update the call to Analyze_PPC_In_Decl_Part. Capture + the pragma name in Nam. + (Process_PPCs): Removed. + * sem_ch6.ads (Analyze_Subprogram_Body_Contract): New routine. + (Analyze_Subprogram_Contract): Update the comment on usage. + * sem_ch13.adb (Analyze_Aspect_Specifications): Add null + implementations for aspects Refined_Depends and Refined_Global. + (Check_Aspect_At_Freeze_Point): Aspects Refined_Depends and + Refined_Global do not need to be checked at the freeze point. + * sem_prag.adb: Add entries in table Sig_Flags + for pragmas Refined_Depends and Refined_Global. + (Analyze_Contract_Cases_In_Decl_Part): Add local + variable Restore. Use Restore to pop the scope. + (Analyze_Depends_In_Decl_Part): Add local variable Restore. Use + Restore to pop the scope. + (Analyze_Global_In_Decl_List): Add local variable Restore. Use Restore + to pop the scope. + (Analyze_PPC_In_Decl_Part): Renamed to + Analyze_Pre_Post_Condition_In_Decl_Part. + (Analyze_Pragma): + Add null implementations for pragmas Refined_Depends and + Refined_Global. Refined_Pre and Refined_Post are now + handled by routine Analyze_Refined_Pre_Post_Condition + exclusively. + (Analyze_Refined_Depends_In_Decl_Part): New + null routine. + (Analyze_Refined_Global_In_Decl_Part): + New null routine. + (Analyze_Refined_Pre_Post): + Renamed to Analyze_Refined_Pre_Post_Condition. + (Analyze_Refined_Pre_Post_Condition): Analyze the boolean + expression. + (Check_Precondition_Postcondition): Update the call + to Analyze_PPC_In_Decl_Part. + * sem_prag.ads: Add entries in table + Pragma_On_Body_Or_Stub_OK for pragmas Refined_Depends + and Refined_Global. + (Analyze_PPC_In_Decl_Part): Renamed + to Analyze_Pre_Post_Condition_In_Decl_Part. Update the + comment on usage. + (Analyze_Refined_Depends_In_Decl_Part): New routine. + (Analyze_Refined_Global_In_Decl_Part): New routine. + (Analyze_Test_Case_In_Decl_Part): Update the comment on usage. + * sem_util.adb (Add_Contract_Item): Rename formal Item to Prag + and update all occurrences. Subprogram body contracts can now + contain pragmas Refined_Depends and Refined_Global. + * sem_util.ads (Add_Contract_Item): Rename formal Item to + Prag. Update the comment on usage. + * sinfo.ads: Update the comment on structure and usage of + N_Contract. + * snames.ads-tmpl: Add new predefined names for Refined_Depends + and Refined_Global. Add entries in table Pragma_Id for + Refined_Depends and Refined_Global. + +2013-10-10 Robert Dewar <dewar@adacore.com> + + * types.ads: Minor reformatting. + 2013-10-10 Thomas Quinot <quinot@adacore.com> * s-taprop-posix.adb: Add missing comment. diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 638fdbedc29..0f21ad48b37 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -466,6 +466,8 @@ package body Aspects is Aspect_Pure_05 => Aspect_Pure_05, Aspect_Pure_12 => Aspect_Pure_12, Aspect_Pure_Function => Aspect_Pure_Function, + Aspect_Refined_Depends => Aspect_Refined_Depends, + Aspect_Refined_Global => Aspect_Refined_Global, Aspect_Refined_Post => Aspect_Refined_Post, Aspect_Refined_Pre => Aspect_Refined_Pre, Aspect_Remote_Access_Type => Aspect_Remote_Access_Type, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index d2f5d6939a6..50ac1aa58cb 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -111,6 +111,8 @@ package Aspects is Aspect_Predicate, -- GNAT Aspect_Priority, Aspect_Read, + Aspect_Refined_Depends, -- GNAT + Aspect_Refined_Global, -- GNAT Aspect_Refined_Post, -- GNAT Aspect_Refined_Pre, -- GNAT Aspect_Relative_Deadline, @@ -321,6 +323,8 @@ package Aspects is Aspect_Predicate => Expression, Aspect_Priority => Expression, Aspect_Read => Name, + Aspect_Refined_Depends => Expression, + Aspect_Refined_Global => Expression, Aspect_Refined_Post => Expression, Aspect_Refined_Pre => Expression, Aspect_Relative_Deadline => Expression, @@ -419,6 +423,8 @@ package Aspects is Aspect_Pure_12 => Name_Pure_12, Aspect_Pure_Function => Name_Pure_Function, Aspect_Read => Name_Read, + Aspect_Refined_Depends => Name_Refined_Depends, + Aspect_Refined_Global => Name_Refined_Global, Aspect_Refined_Post => Name_Refined_Post, Aspect_Refined_Pre => Name_Refined_Pre, Aspect_Relative_Deadline => Name_Relative_Deadline, @@ -612,6 +618,8 @@ package Aspects is Aspect_Pure_12 => Always_Delay, Aspect_Pure_Function => Always_Delay, Aspect_Read => Always_Delay, + Aspect_Refined_Depends => Always_Delay, + Aspect_Refined_Global => Always_Delay, Aspect_Relative_Deadline => Always_Delay, Aspect_Remote_Access_Type => Always_Delay, Aspect_Remote_Call_Interface => Always_Delay, @@ -703,7 +711,9 @@ package Aspects is -- Sem_Prag if the aspects below are implemented by a pragma. Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean := - (Aspect_Refined_Post => True, + (Aspect_Refined_Depends => True, + Aspect_Refined_Global => True, + Aspect_Refined_Post => True, Aspect_Refined_Pre => True, Aspect_SPARK_Mode => True, Aspect_Warnings => True, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index da7fa2d6b3a..fb53f1bb841 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -1065,7 +1065,7 @@ package body Einfo is function Contract (Id : E) return N is begin pragma Assert - (Ekind_In (Id, E_Entry, E_Entry_Family) + (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body) or else Is_Subprogram (Id) or else Is_Generic_Subprogram (Id)); return Node24 (Id); @@ -3651,7 +3651,7 @@ package body Einfo is procedure Set_Contract (Id : E; V : N) is begin pragma Assert - (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void) + (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body, E_Void) or else Is_Subprogram (Id) or else Is_Generic_Subprogram (Id)); Set_Node24 (Id, V); @@ -9012,10 +9012,15 @@ package body Einfo is when E_Entry | E_Entry_Family | + E_Subprogram_Body | Subprogram_Kind | Generic_Subprogram_Kind => Write_Str ("Contract"); + -- The Subprogram_Kind and Generic_Subrpogram_Kind entries + -- here are odd, since the assertions for [Set_]Contract do not + -- allow these possibilities ??? + when others => Write_Str ("Field24???"); end case; diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index d48544fdada..be89e27dca6 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -8489,6 +8489,1050 @@ package body Exp_Ch6 is end Expand_Simple_Function_Return; -------------------------------- + -- Expand_Subprogram_Contract -- + -------------------------------- + + procedure Expand_Subprogram_Contract + (N : Node_Id; + Spec_Id : Entity_Id; + Body_Id : Entity_Id) + is + procedure Add_Invariant_And_Predicate_Checks + (Subp_Id : Entity_Id; + Stmts : in out List_Id; + Result : out Node_Id); + -- Process the result of function Subp_Id (if applicable) and all its + -- formals. Add invariant and predicate checks where applicable. The + -- routine appends all the checks to list Stmts. If Subp_Id denotes a + -- function, Result contains the entity of parameter _Result, to be + -- used in the creation of procedure _Postconditions. + + procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); + -- Append a node to a list. If there is no list, create a new one. When + -- the item denotes a pragma, it is added to the list only when it is + -- enabled. + + procedure Build_Postconditions_Procedure + (Subp_Id : Entity_Id; + Stmts : List_Id; + Result : Entity_Id); + -- Create the body of procedure _Postconditions which handles various + -- assertion actions on exit from subprogram Subp_Id. Stmts is the list + -- of statements to be checked on exit. Parameter Result is the entity + -- of parameter _Result when Subp_Id denotes a function. + + function Build_Pragma_Check_Equivalent + (Prag : Node_Id; + Subp_Id : Entity_Id := Empty; + Inher_Id : Entity_Id := Empty) return Node_Id; + -- Transform a [refined] pre- or postcondition denoted by Prag into an + -- equivalent pragma Check. When the pre- or postcondition is inherited, + -- the routine corrects the references of all formals of Inher_Id to + -- point to the formals of Subp_Id. + + procedure Collect_Body_Postconditions (Stmts : in out List_Id); + -- Process all postconditions found in the declarations of the body. The + -- routine appends the pragma Check equivalents to list Stmts. + + procedure Collect_Spec_Postconditions + (Subp_Id : Entity_Id; + Stmts : in out List_Id); + -- Process all [inherited] postconditions of subprogram spec Subp_Id. + -- The routine appends the pragma Check equivalents to list Stmts. + + procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id); + -- Process all [inherited] preconditions of subprogram spec Subp_Id. The + -- routine prepends the pragma Check equivalents to the declarations of + -- the body. + + procedure Prepend_To_Declarations (Item : Node_Id); + -- Prepend a single item to the declarations of the subprogram body + + procedure Process_Contract_Cases + (Subp_Id : Entity_Id; + Stmts : in out List_Id); + -- Process pragma Contract_Cases of subprogram spec Subp_Id. The routine + -- appends the expanded code to list Stmts. + + ---------------------------------------- + -- Add_Invariant_And_Predicate_Checks -- + ---------------------------------------- + + procedure Add_Invariant_And_Predicate_Checks + (Subp_Id : Entity_Id; + Stmts : in out List_Id; + Result : out Node_Id) + is + procedure Add_Invariant_Access_Checks (Id : Entity_Id); + -- Id denotes the return value of a function or a formal parameter. + -- Add an invariant check if the type of Id is access to a type with + -- invariants. The routine appends the generated code to Stmts. + + function Invariant_Checks_OK (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ can benefit from invariant checks. To + -- qualify, the type must have a non-null invariant procedure and + -- subprogram Subp_Id must appear visible from the point of view of + -- the type. + + function Predicate_Checks_OK (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ can benefit from predicate checks. To + -- qualify, the type must have at least one checked predicate. + + --------------------------------- + -- Add_Invariant_Access_Checks -- + --------------------------------- + + procedure Add_Invariant_Access_Checks (Id : Entity_Id) is + Loc : constant Source_Ptr := Sloc (N); + Ref : Node_Id; + Typ : Entity_Id; + + begin + Typ := Etype (Id); + + if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then + Typ := Designated_Type (Typ); + + if Invariant_Checks_OK (Typ) then + Ref := + Make_Explicit_Dereference (Loc, + Prefix => New_Occurrence_Of (Id, Loc)); + Set_Etype (Ref, Typ); + + -- Generate: + -- if <Id> /= null then + -- <invariant_call (<Ref>)> + -- end if; + + Append_Enabled_Item + (Item => + Make_If_Statement (Loc, + Condition => + Make_Op_Ne (Loc, + Left_Opnd => New_Occurrence_Of (Id, Loc), + Right_Opnd => Make_Null (Loc)), + Then_Statements => New_List ( + Make_Invariant_Call (Ref))), + List => Stmts); + end if; + end if; + end Add_Invariant_Access_Checks; + + ------------------------- + -- Invariant_Checks_OK -- + ------------------------- + + function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is + function Has_Null_Body (Proc_Id : Entity_Id) return Boolean; + -- Determine whether the body of procedure Proc_Id contains a sole + -- null statement, possibly followed by an optional return. + + function Has_Public_Visibility_Of_Subprogram return Boolean; + -- Determine whether type Typ has public visibility of subprogram + -- Subp_Id. + + ------------------- + -- Has_Null_Body -- + ------------------- + + function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is + Body_Id : Entity_Id; + Decl : Node_Id; + Spec : Node_Id; + Stmt1 : Node_Id; + Stmt2 : Node_Id; + + begin + Spec := Parent (Proc_Id); + Decl := Parent (Spec); + + -- Retrieve the entity of the invariant procedure body + + if Nkind (Spec) = N_Procedure_Specification + and then Nkind (Decl) = N_Subprogram_Declaration + then + Body_Id := Corresponding_Body (Decl); + + -- The body acts as a spec + + else + Body_Id := Proc_Id; + end if; + + -- The body will be generated later + + if No (Body_Id) then + return False; + end if; + + Spec := Parent (Body_Id); + Decl := Parent (Spec); + + pragma Assert + (Nkind (Spec) = N_Procedure_Specification + and then Nkind (Decl) = N_Subprogram_Body); + + Stmt1 := First (Statements (Handled_Statement_Sequence (Decl))); + + -- Look for a null statement followed by an optional return + -- statement. + + if Nkind (Stmt1) = N_Null_Statement then + Stmt2 := Next (Stmt1); + + if Present (Stmt2) then + return Nkind (Stmt2) = N_Simple_Return_Statement; + else + return True; + end if; + end if; + + return False; + end Has_Null_Body; + + ----------------------------------------- + -- Has_Public_Visibility_Of_Subprogram -- + ----------------------------------------- + + function Has_Public_Visibility_Of_Subprogram return Boolean is + Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Vis_Decls : constant List_Id := + Visible_Declarations (Specification + (Unit_Declaration_Node (Scope (Typ)))); + begin + -- An Initialization procedure must be considered visible even + -- though it is internally generated. + + if Is_Init_Proc (Defining_Entity (Subp_Decl)) then + return True; + + -- Internally generated code is never publicly visible except + -- for a subprogram that is the implementation of an expression + -- function. In that case the visibility is determined by the + -- last check. + + elsif not Comes_From_Source (Subp_Decl) + and then + (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function + or else not + Comes_From_Source (Defining_Entity (Subp_Decl))) + then + return False; + + -- Determine whether the subprogram is declared in the visible + -- declarations of the package containing the type. + + else + return List_Containing (Subp_Decl) = Vis_Decls; + end if; + end Has_Public_Visibility_Of_Subprogram; + + -- Start of processing for Invariant_Checks_OK + + begin + return + Has_Invariants (Typ) + and then Present (Invariant_Procedure (Typ)) + and then not Has_Null_Body (Invariant_Procedure (Typ)) + and then Has_Public_Visibility_Of_Subprogram; + end Invariant_Checks_OK; + + ------------------------- + -- Predicate_Checks_OK -- + ------------------------- + + function Predicate_Checks_OK (Typ : Entity_Id) return Boolean is + function Has_Checked_Predicate return Boolean; + -- Determine whether type Typ has or inherits at least one + -- predicate aspect or pragma, for which the applicable policy is + -- Checked. + + --------------------------- + -- Has_Checked_Predicate -- + --------------------------- + + function Has_Checked_Predicate return Boolean is + Anc : Entity_Id; + Pred : Node_Id; + + begin + -- Climb the ancestor type chain staring from the input. This + -- is done because the input type may lack aspect/pragma + -- predicate and simply inherit those from its ancestor. + + -- Note that predicate pragmas include all three cases of + -- predicate aspects (Predicate, Dynamic_Predicate, + -- Static_Predicate), so this routine checks for all three + -- cases. + + Anc := Typ; + while Present (Anc) loop + Pred := Get_Pragma (Anc, Pragma_Predicate); + + if Present (Pred) and then not Is_Ignored (Pred) then + return True; + end if; + + Anc := Nearest_Ancestor (Anc); + end loop; + + return False; + end Has_Checked_Predicate; + + -- Start of processing for Predicate_Checks_OK + + begin + return + Has_Predicates (Typ) + and then Present (Predicate_Function (Typ)) + and then Has_Checked_Predicate; + end Predicate_Checks_OK; + + -- Local variables + + Loc : constant Source_Ptr := Sloc (N); + Formal : Entity_Id; + Typ : Entity_Id; + + -- Start of processing for Add_Invariant_And_Predicate_Checks + + begin + Result := Empty; + + -- Do not generate any checks if no code is being generated + + if not Expander_Active then + return; + end if; + + -- Process the result of a function + + if Ekind_In (Subp_Id, E_Function, E_Generic_Function) then + Typ := Etype (Subp_Id); + + -- Generate _Result which is used in procedure _Postconditions to + -- verify the return value. + + Result := Make_Defining_Identifier (Loc, Name_uResult); + Set_Etype (Result, Typ); + + -- Add an invariant check when the return type has invariants and + -- the related function is visible to the outside. + + if Invariant_Checks_OK (Typ) then + Append_Enabled_Item + (Item => + Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), + List => Stmts); + end if; + + -- Add an invariant check when the return type is an access to a + -- type with invariants. + + Add_Invariant_Access_Checks (Result); + end if; + + -- Add invariant and predicates for all formals that qualify + + Formal := First_Formal (Subp_Id); + while Present (Formal) loop + Typ := Etype (Formal); + + if Ekind (Formal) /= E_In_Parameter + or else Is_Access_Type (Typ) + then + if Invariant_Checks_OK (Typ) then + Append_Enabled_Item + (Item => + Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), + List => Stmts); + end if; + + Add_Invariant_Access_Checks (Formal); + + if Predicate_Checks_OK (Typ) then + Append_Enabled_Item + (Item => + Make_Predicate_Check + (Typ, New_Reference_To (Formal, Loc)), + List => Stmts); + end if; + end if; + + Next_Formal (Formal); + end loop; + end Add_Invariant_And_Predicate_Checks; + + ------------------------- + -- Append_Enabled_Item -- + ------------------------- + + procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is + begin + -- Do not chain ignored or disabled pragmas + + if Nkind (Item) = N_Pragma + and then (Is_Ignored (Item) or else Is_Disabled (Item)) + then + null; + + -- Add the item + + else + if No (List) then + List := New_List; + end if; + + Append (Item, List); + end if; + end Append_Enabled_Item; + + ------------------------------------ + -- Build_Postconditions_Procedure -- + ------------------------------------ + + procedure Build_Postconditions_Procedure + (Subp_Id : Entity_Id; + Stmts : List_Id; + Result : Entity_Id) + is + procedure Insert_After_Last_Declaration (Stmt : Node_Id); + -- Insert node Stmt after the last declaration of the subprogram body + + ----------------------------------- + -- Insert_After_Last_Declaration -- + ----------------------------------- + + procedure Insert_After_Last_Declaration (Stmt : Node_Id) is + Decls : List_Id := Declarations (N); + + begin + -- Ensure that the body has a declaration list + + if No (Decls) then + Decls := New_List; + Set_Declarations (N, Decls); + end if; + + Append_To (Decls, Stmt); + end Insert_After_Last_Declaration; + + -- Local variables + + Loc : constant Source_Ptr := Sloc (N); + Params : List_Id := No_List; + Proc_Id : Entity_Id; + + -- Start of processing for Build_Postconditions_Procedure + + begin + -- Do not create the routine if no code is being generated + + if not Expander_Active then + return; + + -- Nothing to do if there are no actions to check on exit + + elsif No (Stmts) then + return; + end if; + + Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); + + -- The related subprogram is a function, create the specification of + -- parameter _Result. + + if Present (Result) then + Params := New_List ( + Make_Parameter_Specification (Loc, + Defining_Identifier => Result, + Parameter_Type => + New_Reference_To (Etype (Result), Loc))); + end if; + + -- Insert _Postconditions after the last declaration of the body. + -- This ensures that the body will not cause any premature freezing + -- as it may mention types: + + -- procedure Proc (Obj : Array_Typ) is + -- procedure _postconditions is + -- begin + -- ... Obj ... + -- end _postconditions; + + -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); + -- begin + + -- In the example above, Obj is of type T but the incorrect placement + -- of _Postconditions will cause a crash in gigi due to an out of + -- order reference. The body of _Postconditions must be placed after + -- the declaration of Temp to preserve correct visibility. + + Insert_After_Last_Declaration ( + Make_Subprogram_Body (Loc, + Specification => + Make_Procedure_Specification (Loc, + Defining_Unit_Name => Proc_Id, + Parameter_Specifications => Params), + + Declarations => Empty_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, Stmts))); + + -- Set the attributes of the related subprogram to capture the + -- generated procedure. + + if Ekind_In (Subp_Id, E_Generic_Procedure, E_Procedure) then + Set_Postcondition_Proc (Subp_Id, Proc_Id); + end if; + + Set_Has_Postconditions (Subp_Id); + end Build_Postconditions_Procedure; + + ----------------------------------- + -- Build_Pragma_Check_Equivalent -- + ----------------------------------- + + function Build_Pragma_Check_Equivalent + (Prag : Node_Id; + Subp_Id : Entity_Id := Empty; + Inher_Id : Entity_Id := Empty) return Node_Id + is + Loc : constant Source_Ptr := Sloc (Prag); + Prag_Nam : constant Name_Id := Pragma_Name (Prag); + Check_Prag : Node_Id; + Formals_Map : Elist_Id; + Inher_Formal : Entity_Id; + Msg_Arg : Node_Id; + Nam : Name_Id; + Subp_Formal : Entity_Id; + + begin + Formals_Map := No_Elist; + + -- When the pre- or postcondition is inherited, map the formals of + -- the inherited subprogram to those of the current subprogram. + + if Present (Inher_Id) then + pragma Assert (Present (Subp_Id)); + + Formals_Map := New_Elmt_List; + + -- Create a relation <inherited formal> => <subprogram formal> + + Inher_Formal := First_Formal (Inher_Id); + Subp_Formal := First_Formal (Subp_Id); + while Present (Inher_Formal) and then Present (Subp_Formal) loop + Append_Elmt (Inher_Formal, Formals_Map); + Append_Elmt (Subp_Formal, Formals_Map); + + Next_Formal (Inher_Formal); + Next_Formal (Subp_Formal); + end loop; + end if; + + -- Copy the original pragma while performing substitutions (if + -- applicable). + + Check_Prag := + New_Copy_Tree + (Source => Prag, + Map => Formals_Map, + New_Scope => Current_Scope); + + -- Mark the pragma as being internally generated and reset the + -- Analyzed flag. + + Set_Comes_From_Source (Check_Prag, False); + Set_Analyzed (Check_Prag, False); + + -- For a postcondition pragma within a generic, preserve the pragma + -- for later expansion. This is also used when an error was detected, + -- thus setting Expander_Active to False. + + if Prag_Nam = Name_Postcondition and then not Expander_Active then + return Check_Prag; + end if; + + if Present (Corresponding_Aspect (Prag)) then + Nam := Chars (Identifier (Corresponding_Aspect (Prag))); + else + Nam := Prag_Nam; + end if; + + -- Convert the copy into pragma Check by correcting the name and + -- adding a check_kind argument. + + Set_Pragma_Identifier + (Check_Prag, Make_Identifier (Loc, Name_Check)); + + Prepend_To (Pragma_Argument_Associations (Check_Prag), + Make_Pragma_Argument_Association (Loc, + Expression => Make_Identifier (Loc, Nam))); + + -- Update the error message when the pragma is inherited + + if Present (Inher_Id) then + Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag)); + + if Chars (Msg_Arg) = Name_Message then + String_To_Name_Buffer (Strval (Expression (Msg_Arg))); + + -- Insert "inherited" to improve the error message + + if Name_Buffer (1 .. 8) = "failed p" then + Insert_Str_In_Name_Buffer ("inherited ", 8); + Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer); + end if; + end if; + end if; + + return Check_Prag; + end Build_Pragma_Check_Equivalent; + + --------------------------------- + -- Collect_Body_Postconditions -- + --------------------------------- + + procedure Collect_Body_Postconditions (Stmts : in out List_Id) is + procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id); + -- Process postconditions of a particular kind denoted by Post_Nam + + ----------------------------------------- + -- Collect_Body_Postconditions_Of_Kind -- + ----------------------------------------- + + procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id) is + Check_Prag : Node_Id; + Decl : Node_Id; + + begin + pragma Assert (Nam_In (Post_Nam, Name_Postcondition, + Name_Refined_Post)); + + -- Inspect the declarations of the subprogram body looking for a + -- pragma that matches the desired name. + + Decl := First (Declarations (N)); + while Present (Decl) loop + if Nkind (Decl) = N_Pragma then + if Pragma_Name (Decl) = Post_Nam then + Analyze (Decl); + Check_Prag := Build_Pragma_Check_Equivalent (Decl); + + if Expander_Active then + Append_Enabled_Item + (Item => Check_Prag, + List => Stmts); + + -- When analyzing a generic unit, save the pragma for + -- later. + + else + Prepend_To_Declarations (Check_Prag); + end if; + end if; + + -- Skip internally generated code + + elsif not Comes_From_Source (Decl) then + null; + + -- Postconditions in bodies are usually grouped at the top of + -- the declarations. There is no point in inspecting the whole + -- source list. + + else + exit; + end if; + + Next (Decl); + end loop; + end Collect_Body_Postconditions_Of_Kind; + + -- Start of processing for Collect_Body_Postconditions + + begin + Collect_Body_Postconditions_Of_Kind (Name_Refined_Post); + Collect_Body_Postconditions_Of_Kind (Name_Postcondition); + end Collect_Body_Postconditions; + + --------------------------------- + -- Collect_Spec_Postconditions -- + --------------------------------- + + procedure Collect_Spec_Postconditions + (Subp_Id : Entity_Id; + Stmts : in out List_Id) + is + Inher_Subps : constant Subprogram_List := + Inherited_Subprograms (Subp_Id); + Check_Prag : Node_Id; + Prag : Node_Id; + Inher_Subp_Id : Entity_Id; + + begin + -- Process the contract of the spec + + Prag := Pre_Post_Conditions (Contract (Subp_Id)); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Postcondition then + Check_Prag := Build_Pragma_Check_Equivalent (Prag); + + if Expander_Active then + Append_Enabled_Item + (Item => Check_Prag, + List => Stmts); + + -- When analyzing a generic unit, save the pragma for later + + else + Prepend_To_Declarations (Check_Prag); + end if; + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Process the contracts of all inherited subprograms, looking for + -- class-wide postconditions. + + for Index in Inher_Subps'Range loop + Inher_Subp_Id := Inher_Subps (Index); + + Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id)); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Postcondition + and then Class_Present (Prag) + then + Check_Prag := + Build_Pragma_Check_Equivalent + (Prag => Prag, + Subp_Id => Subp_Id, + Inher_Id => Inher_Subp_Id); + + if Expander_Active then + Append_Enabled_Item + (Item => Check_Prag, + List => Stmts); + + -- When analyzing a generic unit, save the pragma for later + + else + Prepend_To_Declarations (Check_Prag); + end if; + end if; + + Prag := Next_Pragma (Prag); + end loop; + end loop; + end Collect_Spec_Postconditions; + + -------------------------------- + -- Collect_Spec_Preconditions -- + -------------------------------- + + procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id) is + procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); + -- Merge two class-wide preconditions by "or else"-ing them. The + -- changes are accumulated in parameter Into. Update the error + -- message of Into. + + ------------------------- + -- Merge_Preconditions -- + ------------------------- + + procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is + function Expression_Arg (Prag : Node_Id) return Node_Id; + -- Return the boolean expression argument of a precondition while + -- updating its parenteses count for the subsequent merge. + + function Message_Arg (Prag : Node_Id) return Node_Id; + -- Return the message argument of a precondition + + -------------------- + -- Expression_Arg -- + -------------------- + + function Expression_Arg (Prag : Node_Id) return Node_Id is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); + + begin + if Paren_Count (Arg) = 0 then + Set_Paren_Count (Arg, 1); + end if; + + return Arg; + end Expression_Arg; + + ----------------- + -- Message_Arg -- + ----------------- + + function Message_Arg (Prag : Node_Id) return Node_Id is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + begin + return Get_Pragma_Arg (Last (Args)); + end Message_Arg; + + -- Local variables + + From_Expr : constant Node_Id := Expression_Arg (From); + From_Msg : constant Node_Id := Message_Arg (From); + Into_Expr : constant Node_Id := Expression_Arg (Into); + Into_Msg : constant Node_Id := Message_Arg (Into); + Loc : constant Source_Ptr := Sloc (Into); + + -- Start of processing for Merge_Preconditions + + begin + -- Merge the two preconditions by "or else"-ing them + + Rewrite (Into_Expr, + Make_Or_Else (Loc, + Right_Opnd => Relocate_Node (Into_Expr), + Left_Opnd => From_Expr)); + + -- Merge the two error messages to produce a single message of the + -- form: + + -- failed precondition from ... + -- also failed inherited precondition from ... + + if not Exception_Locations_Suppressed then + Start_String (Strval (Into_Msg)); + Store_String_Char (ASCII.LF); + Store_String_Chars (" also "); + Store_String_Chars (Strval (From_Msg)); + + Set_Strval (Into_Msg, End_String); + end if; + end Merge_Preconditions; + + -- Local variables + + Inher_Subps : constant Subprogram_List := + Inherited_Subprograms (Subp_Id); + Check_Prag : Node_Id; + Class_Pre : Node_Id := Empty; + Inher_Subp_Id : Entity_Id; + Prag : Node_Id; + + -- Start of processing for Collect_Spec_Preconditions + + begin + -- Process the contract of the spec + + Prag := Pre_Post_Conditions (Contract (Subp_Id)); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Precondition then + Check_Prag := Build_Pragma_Check_Equivalent (Prag); + + -- Save the sole class-wide precondition (if any) for the next + -- step where it will be merged with inherited preconditions. + + if Class_Present (Prag) then + Class_Pre := Check_Prag; + + -- Accumulate the corresponding Check pragmas to the top of the + -- declarations. Prepending the items ensures that they will + -- be evaluated in their original order. + + else + Prepend_To_Declarations (Check_Prag); + end if; + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Process the contracts of all inherited subprograms, looking for + -- class-wide preconditions. + + for Index in Inher_Subps'Range loop + Inher_Subp_Id := Inher_Subps (Index); + + Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id)); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Precondition + and then Class_Present (Prag) + then + Check_Prag := + Build_Pragma_Check_Equivalent + (Prag => Prag, + Subp_Id => Subp_Id, + Inher_Id => Inher_Subp_Id); + + -- The spec or an inherited subprogram already yielded a + -- class-wide precondition. Merge the existing precondition + -- with the current one using "or else". + + if Present (Class_Pre) then + Merge_Preconditions (Check_Prag, Class_Pre); + else + Class_Pre := Check_Prag; + end if; + end if; + + Prag := Next_Pragma (Prag); + end loop; + end loop; + + -- Add the merged class-wide preconditions (if any) + + if Present (Class_Pre) then + Prepend_To_Declarations (Class_Pre); + end if; + end Collect_Spec_Preconditions; + + ----------------------------- + -- Prepend_To_Declarations -- + ----------------------------- + + procedure Prepend_To_Declarations (Item : Node_Id) is + Decls : List_Id := Declarations (N); + + begin + -- Ensure that the body has a declarative list + + if No (Decls) then + Decls := New_List; + Set_Declarations (N, Decls); + end if; + + Prepend_To (Decls, Item); + end Prepend_To_Declarations; + + ---------------------------- + -- Process_Contract_Cases -- + ---------------------------- + + procedure Process_Contract_Cases + (Subp_Id : Entity_Id; + Stmts : in out List_Id) + is + Prag : Node_Id; + + begin + -- Do not build the Contract_Cases circuitry if no code is being + -- generated. + + if not Expander_Active then + null; + end if; + + Prag := Contract_Test_Cases (Contract (Subp_Id)); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Contract_Cases then + Expand_Contract_Cases + (CCs => Prag, + Subp_Id => Subp_Id, + Decls => Declarations (N), + Stmts => Stmts); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end Process_Contract_Cases; + + -- Local variables + + Post_Stmts : List_Id := No_List; + Result : Entity_Id; + Subp_Id : Entity_Id; + + -- Start of processing for Expand_Subprogram_Contract + + begin + if Present (Spec_Id) then + Subp_Id := Spec_Id; + else + Subp_Id := Body_Id; + end if; + + -- Do not process a predicate function as its body will end up with a + -- recursive call to itself and blow up the stack. + + if Ekind (Subp_Id) = E_Function + and then Is_Predicate_Function (Subp_Id) + then + return; + + -- Do not process TSS subprograms + + elsif Get_TSS_Name (Subp_Id) /= TSS_Null then + return; + end if; + + -- The expansion of a subprogram contract involves the relocation of + -- various contract assertions to the declarations of the body in a + -- particular order. The order is as follows: + + -- function Example (...) return ... is + -- procedure _Postconditions (...) is + -- begin + -- <refined postconditions from body> + -- <postconditions from body> + -- <postconditions from spec> + -- <inherited postconditions> + -- <contract cases> + -- <invariant check of function result (if applicable)> + -- <invariant and predicate checks of parameters> + -- end _Postconditions; + + -- <inherited preconditions> + -- <preconditions from spec> + -- <preconditions from body> + -- <refined preconditions from body> + + -- <source declarations> + -- begin + -- <source statements> + + -- _Preconditions (Result); + -- return Result; + -- end Example; + + -- Routine _Postconditions holds all contract assertions that must be + -- verified on exit from the related routine. + + -- Collect all [inherited] preconditions from the spec, transform them + -- into Check pragmas and add them to the declarations of the body in + -- the order outlined above. + + if Present (Spec_Id) then + Collect_Spec_Preconditions (Spec_Id); + end if; + + -- Transform all [refined] postconditions of the body into Check + -- pragmas. The resulting pragmas are accumulated in list Post_Stmts. + + Collect_Body_Postconditions (Post_Stmts); + + -- Transform all [inherited] postconditions from the spec into Check + -- pragmas. The resulting pragmas are accumulated in list Post_Stmts. + + if Present (Spec_Id) then + Collect_Spec_Postconditions (Spec_Id, Post_Stmts); + + -- Transform pragma Contract_Cases from the spec into its circuitry + + Process_Contract_Cases (Spec_Id, Post_Stmts); + end if; + + -- Apply invariant and predicate checks on the result of a function (if + -- applicable) and all formals. The resulting checks are accumulated in + -- list Post_Stmts. + + Add_Invariant_And_Predicate_Checks (Subp_Id, Post_Stmts, Result); + + -- Construct procedure _Postconditions + + Build_Postconditions_Procedure (Subp_Id, Post_Stmts, Result); + end Expand_Subprogram_Contract; + + -------------------------------- -- Is_Build_In_Place_Function -- -------------------------------- diff --git a/gcc/ada/exp_ch6.ads b/gcc/ada/exp_ch6.ads index f9829f52b34..02cca2401df 100644 --- a/gcc/ada/exp_ch6.ads +++ b/gcc/ada/exp_ch6.ads @@ -82,6 +82,18 @@ package Exp_Ch6 is -- 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; + Body_Id : Entity_Id); + -- Expand the contracts of a subprogram body and its correspoding spec (if + -- any). This routine processes all [refined] pre- and postconditions as + -- well as Contract_Cases, invariants and predicates. N is the body of the + -- subprogram. Spec_Id denotes the entity of its specification. Body_Id + -- denotes the entity of the subprogram body. This routine is not a "pure" + -- expansion mechanism as it is invoked during analysis and may perform + -- actions for generic subprograms or set up contract assertions for ASIS. + procedure Freeze_Subprogram (N : Node_Id); -- generate the appropriate expansions related to Subprogram freeze -- nodes (e.g. the filling of the corresponding Dispatch Table for diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 85ebe3bdeb7..e8bea1fced3 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1250,6 +1250,8 @@ begin Pragma_Pure_12 | Pragma_Pure_Function | Pragma_Queuing_Policy | + Pragma_Refined_Depends | + Pragma_Refined_Global | Pragma_Refined_Post | Pragma_Refined_Pre | Pragma_Relative_Deadline | diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index e307e87ec2c..30c5bc4adb8 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1928,6 +1928,20 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_SPARK_Mode); + -- Refined_Depends + + -- ??? To be implemented + + when Aspect_Refined_Depends => + null; + + -- Refined_Global + + -- ??? To be implemented + + when Aspect_Refined_Global => + null; + -- Refined_Post when Aspect_Refined_Post => @@ -7962,6 +7976,8 @@ package body Sem_Ch13 is Aspect_Postcondition | Aspect_Pre | Aspect_Precondition | + Aspect_Refined_Depends | + Aspect_Refined_Global | Aspect_Refined_Post | Aspect_Refined_Pre | Aspect_SPARK_Mode | diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index e900cfaa153..1e6abf24cec 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2056,28 +2056,31 @@ package body Sem_Ch3 is -------------------------- procedure Analyze_Declarations (L : List_Id) is - D : Node_Id; - Freeze_From : Entity_Id := Empty; - Next_Node : Node_Id; + Decl : Node_Id; - procedure Adjust_D; - -- Adjust D not to include implicit label declarations, since these + procedure Adjust_Decl; + -- Adjust Decl not to include implicit label declarations, since these -- have strange Sloc values that result in elaboration check problems. -- (They have the sloc of the label as found in the source, and that -- is ahead of the current declarative part). - -------------- - -- Adjust_D -- - -------------- + ----------------- + -- Adjust_Decl -- + ----------------- - procedure Adjust_D is + procedure Adjust_Decl is begin - while Present (Prev (D)) - and then Nkind (D) = N_Implicit_Label_Declaration + while Present (Prev (Decl)) + and then Nkind (Decl) = N_Implicit_Label_Declaration loop - Prev (D); + Prev (Decl); end loop; - end Adjust_D; + end Adjust_Decl; + + -- Local variables + + Freeze_From : Entity_Id := Empty; + Next_Decl : Node_Id; -- Start of processing for Analyze_Declarations @@ -2086,23 +2089,23 @@ package body Sem_Ch3 is Check_Later_Vs_Basic_Declarations (L, During_Parsing => False); end if; - D := First (L); - while Present (D) loop + Decl := First (L); + while Present (Decl) loop -- Package spec cannot contain a package declaration in SPARK - if Nkind (D) = N_Package_Declaration + if Nkind (Decl) = N_Package_Declaration and then Nkind (Parent (L)) = N_Package_Specification then Check_SPARK_Restriction ("package specification cannot contain a package declaration", - D); + Decl); end if; -- Complete analysis of declaration - Analyze (D); - Next_Node := Next (D); + Analyze (Decl); + Next_Decl := Next (Decl); if No (Freeze_From) then Freeze_From := First_Entity (Current_Scope); @@ -2124,7 +2127,7 @@ package body Sem_Ch3 is -- be a freeze point once delayed freezing of bodies is implemented. -- (This is needed in any case for early instantiations ???). - if No (Next_Node) then + if No (Next_Decl) then if Nkind_In (Parent (L), N_Component_List, N_Task_Definition, N_Protected_Definition) @@ -2136,8 +2139,8 @@ package body Sem_Ch3 is Freeze_From := First_Entity (Current_Scope); end if; - Adjust_D; - Freeze_All (Freeze_From, D); + Adjust_Decl; + Freeze_All (Freeze_From, Decl); Freeze_From := Last_Entity (Current_Scope); elsif Scope (Current_Scope) /= Standard_Standard @@ -2150,8 +2153,8 @@ package body Sem_Ch3 is or else No (Private_Declarations (Parent (L))) or else Is_Empty_List (Private_Declarations (Parent (L))) then - Adjust_D; - Freeze_All (Freeze_From, D); + Adjust_Decl; + Freeze_All (Freeze_From, Decl); Freeze_From := Last_Entity (Current_Scope); end if; @@ -2170,44 +2173,39 @@ package body Sem_Ch3 is -- care to attach the bodies at a proper place in the tree so as to -- not cause unwanted freezing at that point. - elsif not Analyzed (Next_Node) - and then (Nkind_In (Next_Node, N_Subprogram_Body, + elsif not Analyzed (Next_Decl) + and then (Nkind_In (Next_Decl, N_Subprogram_Body, N_Entry_Body, N_Package_Body, N_Protected_Body, N_Task_Body) or else - Nkind (Next_Node) in N_Body_Stub) + Nkind (Next_Decl) in N_Body_Stub) then - Adjust_D; - Freeze_All (Freeze_From, D); + Adjust_Decl; + Freeze_All (Freeze_From, Decl); Freeze_From := Last_Entity (Current_Scope); end if; - D := Next_Node; + Decl := Next_Decl; end loop; - -- One more thing to do, we need to scan the declarations to check for - -- any precondition/postcondition pragmas (Pre/Post aspects have by this - -- stage been converted into corresponding pragmas). It is at this point - -- that we analyze the expressions in such pragmas, to implement the - -- delayed visibility requirement. + -- Analyze the contracts of a subprogram declaration or a body now due + -- to delayed visibility requirements of aspects. - declare - Decl : Node_Id; - Subp_Id : Entity_Id; + Decl := First (L); + while Present (Decl) loop + if Nkind (Decl) = N_Subprogram_Body then + Analyze_Subprogram_Body_Contract + (Defining_Unit_Name (Specification (Decl))); - begin - Decl := First (L); - while Present (Decl) loop - if Nkind (Decl) = N_Subprogram_Declaration then - Subp_Id := Defining_Unit_Name (Specification (Decl)); - Analyze_Subprogram_Contract (Subp_Id); - end if; + elsif Nkind (Decl) = N_Subprogram_Declaration then + Analyze_Subprogram_Contract + (Defining_Unit_Name (Specification (Decl))); + end if; - Next (Decl); - end loop; - end; + Next (Decl); + end loop; end Analyze_Declarations; ----------------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index e313f3518d8..462a7f1732f 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -212,17 +212,6 @@ package body Sem_Ch6 is -- Create the declaration for an inequality operator that is implicitly -- created by a user-defined equality operator that yields a boolean. - procedure Process_PPCs - (N : Node_Id; - Spec_Id : Entity_Id; - Body_Id : Entity_Id); - -- Called from Analyze[_Generic]_Subprogram_Body to deal with scanning post - -- conditions for the body and assembling and inserting the _postconditions - -- procedure. N is the node for the subprogram body and Body_Id/Spec_Id are - -- the entities for the body and separate spec (if there is no separate - -- spec, Spec_Id is Empty). Note that invariants and predicates may also - -- provide postconditions, and are also handled in this procedure. - procedure Set_Formal_Validity (Formal_Id : Entity_Id); -- Formal_Id is an formal parameter entity. This procedure deals with -- setting the proper validity status for this entity, which depends on @@ -1120,7 +1109,7 @@ package body Sem_Ch6 is -- Visible generic entity is callable within its own body Set_Ekind (Gen_Id, Ekind (Body_Id)); - Set_Contract (Body_Id, Empty); + Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); Set_Ekind (Body_Id, E_Subprogram_Body); Set_Convention (Body_Id, Convention (Gen_Id)); Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id)); @@ -1156,13 +1145,14 @@ package body Sem_Ch6 is Set_Actual_Subtypes (N, Current_Scope); - -- Deal with preconditions and postconditions. In formal verification - -- mode, we keep pre- and postconditions attached to entities rather - -- than inserted in the code, in order to facilitate a distinct - -- treatment for them. + -- Deal with [refined] preconditions, postconditions, Contract_Cases, + -- invariants and predicates associated with the body and its spec. + -- Note that this is not pure expansion as Expand_Subprogram_Contract + -- prepares the contract assertions for generic subprograms or for + -- ASIS. Do not generate contract checks in SPARK mode. if not SPARK_Mode then - Process_PPCs (N, Gen_Id, Body_Id); + Expand_Subprogram_Contract (N, Gen_Id, Body_Id); end if; -- If the generic unit carries pre- or post-conditions, copy them @@ -1981,6 +1971,18 @@ package body Sem_Ch6 is end if; end Analyze_Subprogram_Body; + -------------------------------------- + -- Analyze_Subprogram_Body_Contract -- + -------------------------------------- + + -- ??? To be implemented + + procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id) is + pragma Unreferenced (Subp); + begin + null; + end Analyze_Subprogram_Body_Contract; + ------------------------------------ -- Analyze_Subprogram_Body_Helper -- ------------------------------------ @@ -2933,7 +2935,7 @@ package body Sem_Ch6 is end if; Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id); - Set_Contract (Body_Id, Empty); + Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); Set_Ekind (Body_Id, E_Subprogram_Body); Set_Scope (Body_Id, Scope (Spec_Id)); Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id)); @@ -3117,13 +3119,14 @@ package body Sem_Ch6 is HSS := Handled_Statement_Sequence (N); Set_Actual_Subtypes (N, Current_Scope); - -- Deal with preconditions and postconditions. In formal verification - -- mode, we keep pre- and postconditions attached to entities rather - -- than inserted in the code, in order to facilitate a distinct - -- treatment for them. + -- Deal with [refined] preconditions, postconditions, Contract_Cases, + -- invariants and predicates associated with the body and its spec. + -- Note that this is not pure expansion as Expand_Subprogram_Contract + -- prepares the contract assertions for generic subprograms or for ASIS. + -- Do not generate contract checks in SPARK mode. if not SPARK_Mode then - Process_PPCs (N, Spec_Id, Body_Id); + Expand_Subprogram_Contract (N, Spec_Id, Body_Id); end if; -- Add a declaration for the Protection object, renaming declarations @@ -3535,6 +3538,7 @@ package body Sem_Ch6 is Items : constant Node_Id := Contract (Subp); Error_CCase : Node_Id; Error_Post : Node_Id; + Nam : Name_Id; Prag : Node_Id; -- Start of processing for Analyze_Subprogram_Contract @@ -3549,7 +3553,7 @@ package body Sem_Ch6 is Prag := Pre_Post_Conditions (Items); while Present (Prag) loop - Analyze_PPC_In_Decl_Part (Prag, Subp); + Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Subp); -- Verify whether a postcondition mentions attribute 'Result and -- its expression introduces a post-state. @@ -3567,7 +3571,9 @@ package body Sem_Ch6 is Prag := Contract_Test_Cases (Items); while Present (Prag) loop - if Pragma_Name (Prag) = Name_Contract_Cases then + Nam := Pragma_Name (Prag); + + if Nam = Name_Contract_Cases then Analyze_Contract_Cases_In_Decl_Part (Prag); -- Verify whether contract-cases mention attribute 'Result and @@ -3581,7 +3587,7 @@ package body Sem_Ch6 is end if; else - pragma Assert (Pragma_Name (Prag) = Name_Test_Case); + pragma Assert (Nam = Name_Test_Case); Analyze_Test_Case_In_Decl_Part (Prag, Subp); end if; @@ -3592,10 +3598,12 @@ package body Sem_Ch6 is Prag := Classifications (Contract (Subp)); while Present (Prag) loop - if Pragma_Name (Prag) = Name_Depends then + Nam := Pragma_Name (Prag); + + if Nam = Name_Depends then Analyze_Depends_In_Decl_Part (Prag); else - pragma Assert (Pragma_Name (Prag) = Name_Global); + pragma Assert (Nam = Name_Global); Analyze_Global_In_Decl_Part (Prag); end if; @@ -11248,867 +11256,6 @@ package body Sem_Ch6 is end if; end Process_Formals; - ------------------ - -- Process_PPCs -- - ------------------ - - procedure Process_PPCs - (N : Node_Id; - Spec_Id : Entity_Id; - Body_Id : Entity_Id) - is - Loc : constant Source_Ptr := Sloc (N); - Prag : Node_Id; - Parms : List_Id; - - Designator : Entity_Id; - -- Subprogram designator, set from Spec_Id if present, else Body_Id - - Precond : Node_Id := Empty; - -- Set non-Empty if we prepend precondition to the declarations. This - -- is used to hook up inherited preconditions (adding the condition - -- expression with OR ELSE, and adding the message). - - Inherited_Precond : Node_Id; - -- Precondition inherited from parent subprogram - - Inherited : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); - -- List of subprograms inherited by this subprogram - - Plist : List_Id := No_List; - -- List of generated postconditions - - procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id); - -- Append a node to a list. If there is no list, create a new one. When - -- the item denotes a pragma, it is added to the list only when it is - -- enabled. - - procedure Check_Access_Invariants (E : Entity_Id); - -- If the subprogram returns an access to a type with invariants, or - -- has access parameters whose designated type has an invariant, then - -- under the same visibility conditions as for other invariant checks, - -- the type invariant must be applied to the returned value. - - procedure Collect_Body_Postconditions (Post_Nam : Name_Id); - -- Examine the declarations of the body, looking for pragmas with name - -- Post_Nam. Parameter Post_Nam must denote either Name_Postcondition or - -- Name_Refined_Post. Chain any relevant postconditions to Plist. - - function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id; - -- Prag contains an analyzed precondition or postcondition pragma. This - -- function copies the pragma, changes it to the corresponding Check - -- pragma and returns the Check pragma as the result. If Pspec is non- - -- empty, this is the case of inheriting a PPC, where we must change - -- references to parameters of the inherited subprogram to point to the - -- corresponding parameters of the current subprogram. - - function Has_Checked_Predicate (Typ : Entity_Id) return Boolean; - -- Determine whether type Typ has or inherits at least one predicate - -- aspect or pragma, for which the applicable policy is Checked. - - function Has_Null_Body (Proc_Id : Entity_Id) return Boolean; - -- Determine whether the body of procedure Proc_Id contains a sole null - -- statement, possibly followed by an optional return. - - procedure Insert_After_Last_Declaration (Nod : Node_Id); - -- Insert node Nod after the last declaration of the context - - function Is_Public_Subprogram_For (T : Entity_Id) return Boolean; - -- T is the entity for a private type for which invariants are defined. - -- This function returns True if the procedure corresponding to the - -- value of Designator is a public procedure from the point of view of - -- this type (i.e. its spec is in the visible part of the package that - -- contains the declaration of the private type). A True value means - -- that an invariant check is required (for an IN OUT parameter, or - -- the returned value of a function. - - ------------------------- - -- Append_Enabled_Item -- - ------------------------- - - procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is - begin - -- Do not chain ignored or disabled pragmas - - if Nkind (Item) = N_Pragma - and then (Is_Ignored (Item) or else Is_Disabled (Item)) - then - null; - - -- Add the item - - else - if No (List) then - List := New_List; - end if; - - Append (Item, List); - end if; - end Append_Enabled_Item; - - ----------------------------- - -- Check_Access_Invariants -- - ----------------------------- - - procedure Check_Access_Invariants (E : Entity_Id) is - Call : Node_Id; - Obj : Node_Id; - Typ : Entity_Id; - - begin - if Is_Access_Type (Etype (E)) - and then not Is_Access_Constant (Etype (E)) - then - Typ := Designated_Type (Etype (E)); - - if Has_Invariants (Typ) - and then Present (Invariant_Procedure (Typ)) - and then not Has_Null_Body (Invariant_Procedure (Typ)) - and then Is_Public_Subprogram_For (Typ) - then - Obj := - Make_Explicit_Dereference (Loc, - Prefix => New_Occurrence_Of (E, Loc)); - Set_Etype (Obj, Typ); - - Call := Make_Invariant_Call (Obj); - - Append_Enabled_Item - (Make_If_Statement (Loc, - Condition => - Make_Op_Ne (Loc, - Left_Opnd => Make_Null (Loc), - Right_Opnd => New_Occurrence_Of (E, Loc)), - Then_Statements => New_List (Call)), - List => Plist); - end if; - end if; - end Check_Access_Invariants; - - --------------------------------- - -- Collect_Body_Postconditions -- - --------------------------------- - - procedure Collect_Body_Postconditions (Post_Nam : Name_Id) is - Next_Prag : Node_Id; - - begin - pragma Assert - (Nam_In (Post_Nam, Name_Postcondition, Name_Refined_Post)); - - Prag := First (Declarations (N)); - while Present (Prag) loop - Next_Prag := Next (Prag); - - if Nkind (Prag) = N_Pragma then - - -- Capture postcondition pragmas - - if Pragma_Name (Prag) = Post_Nam then - Analyze (Prag); - - -- All Refined_Post pragmas must be relocated to the body - -- of the generated _Postconditions routine, otherwise they - -- will be duplicated twice - once in the declarations of - -- the body and once in _Postconditions. - - if Pragma_Name (Prag) = Name_Refined_Post then - Remove (Prag); - end if; - - -- If expansion is disabled, as in a generic unit, save - -- pragma for later expansion. - - if not Expander_Active then - Prepend (Grab_PPC, Declarations (N)); - else - Append_Enabled_Item (Grab_PPC, Plist); - end if; - end if; - - -- Skip internally generated code - - elsif not Comes_From_Source (Prag) then - null; - - else - exit; - end if; - - Prag := Next_Prag; - end loop; - end Collect_Body_Postconditions; - - -------------- - -- Grab_PPC -- - -------------- - - function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id is - Nam : constant Name_Id := Pragma_Name (Prag); - Map : Elist_Id; - CP : Node_Id; - - Ename : Name_Id; - -- Effective name of pragma (maybe Pre/Post rather than Precondition/ - -- Postcodition if the pragma came from a Pre/Post aspect). We need - -- the name right when we generate the Check pragma, since we want - -- the right set of check policies to apply. - - begin - -- Prepare map if this is the case where we have to map entities of - -- arguments in the overridden subprogram to corresponding entities - -- of the current subprogram. - - if No (Pspec) then - Map := No_Elist; - - else - declare - PF : Entity_Id; - CF : Entity_Id; - - begin - Map := New_Elmt_List; - PF := First_Formal (Pspec); - CF := First_Formal (Designator); - while Present (PF) loop - Append_Elmt (PF, Map); - Append_Elmt (CF, Map); - Next_Formal (PF); - Next_Formal (CF); - end loop; - end; - end if; - - -- Now we can copy the tree, doing any required substitutions - - CP := New_Copy_Tree (Prag, Map => Map, New_Scope => Current_Scope); - - -- Set Analyzed to false, since we want to reanalyze the check - -- procedure. Note that it is only at the outer level that we - -- do this fiddling, for the spec cases, the already preanalyzed - -- parameters are not affected. - - Set_Analyzed (CP, False); - - -- We also make sure Comes_From_Source is False for the copy - - Set_Comes_From_Source (CP, False); - - -- For a postcondition pragma within a generic, preserve the pragma - -- for later expansion. This is also used when an error was detected, - -- thus setting Expander_Active to False. - - if Nam = Name_Postcondition - and then not Expander_Active - then - return CP; - end if; - - -- Get effective name of aspect - - if Present (Corresponding_Aspect (Prag)) then - Ename := Chars (Identifier (Corresponding_Aspect (Prag))); - else - Ename := Nam; - end if; - - -- Change copy of pragma into corresponding pragma Check - - Prepend_To (Pragma_Argument_Associations (CP), - Make_Pragma_Argument_Association (Sloc (Prag), - Expression => Make_Identifier (Loc, Ename))); - Set_Pragma_Identifier (CP, Make_Identifier (Sloc (Prag), Name_Check)); - - -- If this is inherited case and the current message starts with - -- "failed p", we change it to "failed inherited p...". - - if Present (Pspec) then - declare - Msg : constant Node_Id := - Last (Pragma_Argument_Associations (CP)); - - begin - if Chars (Msg) = Name_Message then - String_To_Name_Buffer (Strval (Expression (Msg))); - - if Name_Buffer (1 .. 8) = "failed p" then - Insert_Str_In_Name_Buffer ("inherited ", 8); - Set_Strval - (Expression (Last (Pragma_Argument_Associations (CP))), - String_From_Name_Buffer); - end if; - end if; - end; - end if; - - -- Return the check pragma - - return CP; - end Grab_PPC; - - --------------------------- - -- Has_Checked_Predicate -- - --------------------------- - - function Has_Checked_Predicate (Typ : Entity_Id) return Boolean is - Anc : Entity_Id; - Pred : Node_Id; - - begin - -- Climb the ancestor type chain staring from the input. This is done - -- because the input type may lack aspect/pragma predicate and simply - -- inherit those from its ancestor. - - -- Note that predicate pragmas include all three cases of predicate - -- aspects (Predicate, Dynamic_Predicate, Static_Predicate), so this - -- routine checks for all three cases. - - Anc := Typ; - while Present (Anc) loop - Pred := Get_Pragma (Anc, Pragma_Predicate); - - if Present (Pred) and then not Is_Ignored (Pred) then - return True; - end if; - - Anc := Nearest_Ancestor (Anc); - end loop; - - return False; - end Has_Checked_Predicate; - - ------------------- - -- Has_Null_Body -- - ------------------- - - function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is - Body_Id : Entity_Id; - Decl : Node_Id; - Spec : Node_Id; - Stmt1 : Node_Id; - Stmt2 : Node_Id; - - begin - Spec := Parent (Proc_Id); - Decl := Parent (Spec); - - -- Retrieve the entity of the invariant procedure body - - if Nkind (Spec) = N_Procedure_Specification - and then Nkind (Decl) = N_Subprogram_Declaration - then - Body_Id := Corresponding_Body (Decl); - - -- The body acts as a spec - - else - Body_Id := Proc_Id; - end if; - - -- The body will be generated later - - if No (Body_Id) then - return False; - end if; - - Spec := Parent (Body_Id); - Decl := Parent (Spec); - - pragma Assert - (Nkind (Spec) = N_Procedure_Specification - and then Nkind (Decl) = N_Subprogram_Body); - - Stmt1 := First (Statements (Handled_Statement_Sequence (Decl))); - - -- Look for a null statement followed by an optional return statement - - if Nkind (Stmt1) = N_Null_Statement then - Stmt2 := Next (Stmt1); - - if Present (Stmt2) then - return Nkind (Stmt2) = N_Simple_Return_Statement; - else - return True; - end if; - end if; - - return False; - end Has_Null_Body; - - ----------------------------------- - -- Insert_After_Last_Declaration -- - ----------------------------------- - - procedure Insert_After_Last_Declaration (Nod : Node_Id) is - Decls : constant List_Id := Declarations (N); - - begin - if No (Decls) then - Set_Declarations (N, New_List (Nod)); - else - Append_To (Decls, Nod); - end if; - end Insert_After_Last_Declaration; - - ------------------------------ - -- Is_Public_Subprogram_For -- - ------------------------------ - - -- The type T is a private type, its declaration is therefore in - -- the list of public declarations of some package. The test for a - -- public subprogram is that its declaration is in this same list - -- of declarations for the same package (note that all the public - -- declarations are in one list, and all the private declarations - -- in another, so this deals with the public/private distinction). - - function Is_Public_Subprogram_For (T : Entity_Id) return Boolean is - DD : constant Node_Id := Unit_Declaration_Node (Designator); - -- The subprogram declaration for the subprogram in question - - TL : constant List_Id := - Visible_Declarations - (Specification (Unit_Declaration_Node (Scope (T)))); - -- The list of declarations containing the private declaration of - -- the type. We know it is a private type, so we know its scope is - -- the package in question, and we know it must be in the visible - -- declarations of this package. - - begin - -- If the subprogram declaration is not a list member, it must be - -- an Init_Proc, in which case we want to consider it to be a - -- public subprogram, since we do get initializations to deal with. - -- Other internally generated subprograms are not public. - - if not Is_List_Member (DD) - and then Is_Init_Proc (Defining_Entity (DD)) - then - return True; - - -- The declaration may have been generated for an expression function - -- so check whether that function comes from source. - - elsif not Comes_From_Source (DD) - and then - (Nkind (Original_Node (DD)) /= N_Expression_Function - or else not Comes_From_Source (Defining_Entity (DD))) - then - return False; - - -- Otherwise we test whether the subprogram is declared in the - -- visible declarations of the package containing the type. - - else - return TL = List_Containing (DD); - end if; - end Is_Public_Subprogram_For; - - -- Local variables - - Formal : Node_Id; - Formal_Typ : Entity_Id; - Func_Typ : Entity_Id; - Post_Proc : Entity_Id; - Result : Node_Id; - - -- Start of processing for Process_PPCs - - begin - -- Capture designator from spec if present, else from body - - if Present (Spec_Id) then - Designator := Spec_Id; - else - Designator := Body_Id; - end if; - - -- Do not process a predicate function as its body will contain a - -- recursive call to itself and blow up the stack. - - if Ekind (Designator) = E_Function - and then Is_Predicate_Function (Designator) - then - return; - - -- Internally generated subprograms, such as type-specific functions, - -- don't get assertion checks. - - elsif Get_TSS_Name (Designator) /= TSS_Null then - return; - end if; - - -- Grab preconditions from spec - - if Present (Spec_Id) then - - -- Loop through PPC pragmas from spec. Note that preconditions from - -- the body will be analyzed and converted when we scan the body - -- declarations below. - - Prag := Pre_Post_Conditions (Contract (Spec_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition then - - -- For Pre (or Precondition pragma), we simply prepend the - -- pragma to the list of declarations right away so that it - -- will be executed at the start of the procedure. Note that - -- this processing reverses the order of the list, which is - -- what we want since new entries were chained to the head of - -- the list. There can be more than one precondition when we - -- use pragma Precondition. - - if not Class_Present (Prag) then - Prepend (Grab_PPC, Declarations (N)); - - -- For Pre'Class there can only be one pragma, and we save - -- it in Precond for now. We will add inherited Pre'Class - -- stuff before inserting this pragma in the declarations. - else - Precond := Grab_PPC; - end if; - end if; - - Prag := Next_Pragma (Prag); - end loop; - - -- Now deal with inherited preconditions - - for J in Inherited'Range loop - Prag := Pre_Post_Conditions (Contract (Inherited (J))); - - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition - and then Class_Present (Prag) - then - Inherited_Precond := Grab_PPC (Inherited (J)); - - -- No precondition so far, so establish this as the first - - if No (Precond) then - Precond := Inherited_Precond; - - -- Here we already have a precondition, add inherited one - - else - -- Add new precondition to old one using OR ELSE - - declare - New_Expr : constant Node_Id := - Get_Pragma_Arg - (Next (First (Pragma_Argument_Associations - (Inherited_Precond)))); - Old_Expr : constant Node_Id := - Get_Pragma_Arg - (Next (First (Pragma_Argument_Associations - (Precond)))); - - begin - if Paren_Count (Old_Expr) = 0 then - Set_Paren_Count (Old_Expr, 1); - end if; - - if Paren_Count (New_Expr) = 0 then - Set_Paren_Count (New_Expr, 1); - end if; - - Rewrite (Old_Expr, - Make_Or_Else (Sloc (Old_Expr), - Left_Opnd => Relocate_Node (Old_Expr), - Right_Opnd => New_Expr)); - end; - - -- Add new message in the form: - - -- failed precondition from bla - -- also failed inherited precondition from bla - -- ... - - -- Skip this if exception locations are suppressed - - if not Exception_Locations_Suppressed then - declare - New_Msg : constant Node_Id := - Get_Pragma_Arg - (Last - (Pragma_Argument_Associations - (Inherited_Precond))); - Old_Msg : constant Node_Id := - Get_Pragma_Arg - (Last - (Pragma_Argument_Associations - (Precond))); - begin - Start_String (Strval (Old_Msg)); - Store_String_Chars (ASCII.LF & " also "); - Store_String_Chars (Strval (New_Msg)); - Set_Strval (Old_Msg, End_String); - end; - end if; - end if; - end if; - - Prag := Next_Pragma (Prag); - end loop; - end loop; - - -- If we have built a precondition for Pre'Class (including any - -- Pre'Class aspects inherited from parent subprograms), then we - -- insert this composite precondition at this stage. - - if Present (Precond) then - Prepend (Precond, Declarations (N)); - end if; - end if; - - -- Build postconditions procedure if needed and prepend the following - -- declaration to the start of the declarations for the subprogram. - - -- procedure _postconditions [(_Result : resulttype)] is - -- begin - -- pragma Check (Refined_Post, condition); - -- pragma Check (Refined_Post, condition); - -- pragma Check (Postcondition, condition [,message]); - -- pragma Check (Postcondition, condition [,message]); - -- ... - -- Invariant_Procedure (_Result) ... - -- Invariant_Procedure (Arg1) - -- ... - -- end; - - -- First we deal with the postconditions in the body - - Collect_Body_Postconditions (Name_Refined_Post); - Collect_Body_Postconditions (Name_Postcondition); - - -- Now deal with any postconditions from the spec - - if Present (Spec_Id) then - Spec_Postconditions : declare - procedure Process_Contract_Cases (Spec : Node_Id); - -- This processes the Contract_Test_Cases from Spec, processing - -- any contract-cases from the list. The caller has checked that - -- Contract_Test_Cases is non-Empty. - - procedure Process_Post_Conditions - (Spec : Node_Id; - Class : Boolean); - -- This processes the Pre_Post_Conditions from Spec, processing - -- any postconditions from the list. If Class is True, then only - -- postconditions marked with Class_Present are considered. The - -- caller has checked that Pre_Post_Conditions is non-Empty. - - ---------------------------- - -- Process_Contract_Cases -- - ---------------------------- - - procedure Process_Contract_Cases (Spec : Node_Id) is - begin - -- Loop through Contract_Cases pragmas from spec - - Prag := Contract_Test_Cases (Contract (Spec)); - loop - if Pragma_Name (Prag) = Name_Contract_Cases then - Expand_Contract_Cases - (CCs => Prag, - Subp_Id => Spec_Id, - Decls => Declarations (N), - Stmts => Plist); - end if; - - Prag := Next_Pragma (Prag); - exit when No (Prag); - end loop; - end Process_Contract_Cases; - - ----------------------------- - -- Process_Post_Conditions -- - ----------------------------- - - procedure Process_Post_Conditions - (Spec : Node_Id; - Class : Boolean) - is - Pspec : Node_Id; - - begin - if Class then - Pspec := Spec; - else - Pspec := Empty; - end if; - - -- Loop through PPC pragmas from spec - - Prag := Pre_Post_Conditions (Contract (Spec)); - loop - if Pragma_Name (Prag) = Name_Postcondition - and then (not Class or else Class_Present (Prag)) - then - if not Expander_Active then - Prepend (Grab_PPC (Pspec), Declarations (N)); - else - Append_Enabled_Item (Grab_PPC (Pspec), Plist); - end if; - end if; - - Prag := Next_Pragma (Prag); - exit when No (Prag); - end loop; - end Process_Post_Conditions; - - -- Start of processing for Spec_Postconditions - - begin - -- Process postconditions expressed as contract-cases - - if Present (Contract_Test_Cases (Contract (Spec_Id))) then - Process_Contract_Cases (Spec_Id); - end if; - - -- Process spec postconditions - - if Present (Pre_Post_Conditions (Contract (Spec_Id))) then - Process_Post_Conditions (Spec_Id, Class => False); - end if; - - -- Process inherited postconditions - - for J in Inherited'Range loop - if Present (Pre_Post_Conditions (Contract (Inherited (J)))) then - Process_Post_Conditions (Inherited (J), Class => True); - end if; - end loop; - end Spec_Postconditions; - end if; - - -- Add an invariant call to check the result of a function - - if Ekind (Designator) /= E_Procedure and then Expander_Active then - Func_Typ := Etype (Designator); - Result := Make_Defining_Identifier (Loc, Name_uResult); - - Set_Etype (Result, Func_Typ); - - -- Add argument for return - - Parms := New_List ( - Make_Parameter_Specification (Loc, - Defining_Identifier => Result, - Parameter_Type => New_Occurrence_Of (Func_Typ, Loc))); - - -- Add invariant call if returning type with invariants and this is a - -- public function, i.e. a function declared in the visible part of - -- the package defining the private type. - - if Has_Invariants (Func_Typ) - and then Present (Invariant_Procedure (Func_Typ)) - and then not Has_Null_Body (Invariant_Procedure (Func_Typ)) - and then Is_Public_Subprogram_For (Func_Typ) - then - Append_Enabled_Item - (Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), Plist); - end if; - - -- Same if return value is an access to type with invariants - - Check_Access_Invariants (Result); - - -- Procedure case - - else - Parms := No_List; - end if; - - -- Add invariant calls and predicate calls for parameters. Note that - -- this is done for functions as well, since in Ada 2012 they can have - -- IN OUT args. - - if Expander_Active then - Formal := First_Formal (Designator); - while Present (Formal) loop - if Ekind (Formal) /= E_In_Parameter - or else Is_Access_Type (Etype (Formal)) - then - Formal_Typ := Etype (Formal); - - if Has_Invariants (Formal_Typ) - and then Present (Invariant_Procedure (Formal_Typ)) - and then not Has_Null_Body (Invariant_Procedure (Formal_Typ)) - and then Is_Public_Subprogram_For (Formal_Typ) - then - Append_Enabled_Item - (Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)), - Plist); - end if; - - Check_Access_Invariants (Formal); - - if Has_Predicates (Formal_Typ) - and then Present (Predicate_Function (Formal_Typ)) - and then Has_Checked_Predicate (Formal_Typ) - then - Append_Enabled_Item - (Make_Predicate_Check - (Formal_Typ, New_Occurrence_Of (Formal, Loc)), - Plist); - end if; - end if; - - Next_Formal (Formal); - end loop; - end if; - - -- Build and insert postcondition procedure - - if Expander_Active and then Present (Plist) then - Post_Proc := - Make_Defining_Identifier (Loc, Chars => Name_uPostconditions); - - -- Insert the corresponding body of a post condition pragma after the - -- last declaration of the context. This ensures that the body will - -- not cause any premature freezing as it may mention types: - - -- procedure Proc (Obj : Array_Typ) is - -- procedure _postconditions is - -- begin - -- ... Obj ... - -- end _postconditions; - - -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1)); - -- begin - - -- In the example above, Obj is of type T but the incorrect placement - -- of _postconditions will cause a crash in gigi due to an out of - -- order reference. The body of _postconditions must be placed after - -- the declaration of Temp to preserve correct visibility. - - Insert_After_Last_Declaration ( - Make_Subprogram_Body (Loc, - Specification => - Make_Procedure_Specification (Loc, - Defining_Unit_Name => Post_Proc, - Parameter_Specifications => Parms), - - Declarations => Empty_List, - - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => Plist))); - - Set_Ekind (Post_Proc, E_Procedure); - - -- If this is a procedure, set the Postcondition_Proc attribute on - -- the proper defining entity for the subprogram. - - if Ekind (Designator) = E_Procedure then - Set_Postcondition_Proc (Designator, Post_Proc); - end if; - - Set_Has_Postconditions (Designator); - end if; - end Process_PPCs; - ---------------------------- -- Reference_Body_Formals -- ---------------------------- diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads index d967c017ae0..bc901cc8fab 100644 --- a/gcc/ada/sem_ch6.ads +++ b/gcc/ada/sem_ch6.ads @@ -46,9 +46,21 @@ package Sem_Ch6 is procedure Analyze_Subprogram_Declaration (N : Node_Id); procedure Analyze_Subprogram_Body (N : Node_Id); + procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id); + -- Analyze all delayed aspects chained on the contract of subprogram body + -- Subp as if they appeared at the end of a declarative region. The aspects + -- in question are: + -- Refined_Depends + -- Refined_Global + procedure Analyze_Subprogram_Contract (Subp : Entity_Id); -- Analyze all delayed aspects chained on the contract of subprogram Subp - -- as if they appeared at the end of a declarative region. + -- as if they appeared at the end of a declarative region. The aspects in + -- question are: + -- Contract_Cases + -- Postcondition + -- Precondition + -- Test_Case function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id; -- Analyze subprogram specification in both subprogram declarations diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index ef8df47cdee..7b0f71f15b0 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -404,6 +404,7 @@ package body Sem_Prag is Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); All_Cases : Node_Id; CCase : Node_Id; + Restore : Boolean := False; Subp_Decl : Node_Id; Subp_Id : Entity_Id; @@ -431,6 +432,7 @@ package body Sem_Prag is -- for subprogram bodies because the formals are already visible. if Requires_Profile_Installation (N, Subp_Decl) then + Restore := True; Push_Scope (Subp_Id); Install_Formals (Subp_Id); end if; @@ -441,7 +443,7 @@ package body Sem_Prag is Next (CCase); end loop; - if Requires_Profile_Installation (N, Subp_Decl) then + if Restore then End_Scope; end if; end if; @@ -1234,6 +1236,9 @@ package body Sem_Prag is Last_Clause : Node_Id; Subp_Decl : Node_Id; + Restore_Scope : Boolean := False; + -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit + -- Start of processing for Analyze_Depends_In_Decl_Part begin @@ -1287,6 +1292,7 @@ package body Sem_Prag is -- bodies because the formals are already visible. if Requires_Profile_Installation (N, Subp_Decl) then + Restore_Scope := True; Push_Scope (Subp_Id); Install_Formals (Subp_Id); end if; @@ -1317,7 +1323,7 @@ package body Sem_Prag is Next (Clause); end loop; - if Requires_Profile_Installation (N, Subp_Decl) then + if Restore_Scope then End_Scope; end if; @@ -1690,6 +1696,9 @@ package body Sem_Prag is List : Node_Id; Subp_Decl : Node_Id; + Restore_Scope : Boolean := False; + -- Set True if we do a Push_Scope requiring a Pop_Scope on exit + -- Start of processing for Analyze_Global_In_Decl_List begin @@ -1714,171 +1723,19 @@ package body Sem_Prag is -- subprogram declarations. if Requires_Profile_Installation (N, Subp_Decl) then + Restore_Scope := True; Push_Scope (Subp_Id); Install_Formals (Subp_Id); end if; Analyze_Global_List (List); - if Requires_Profile_Installation (N, Subp_Decl) then + if Restore_Scope then End_Scope; end if; end if; end Analyze_Global_In_Decl_Part; - ------------------------------ - -- Analyze_PPC_In_Decl_Part -- - ------------------------------ - - procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id) is - Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); - - begin - -- Install formals and push subprogram spec onto scope stack so that we - -- can see the formals from the pragma. - - Install_Formals (S); - Push_Scope (S); - - -- Preanalyze the boolean expression, we treat this as a spec expression - -- (i.e. similar to a default expression). - - -- In ASIS mode, for a pragma generated from a source aspect, analyze - -- directly the the original aspect expression, which is shared with - -- the generated pragma. - - if ASIS_Mode and then Present (Corresponding_Aspect (N)) then - Preanalyze_Assert_Expression - (Expression (Corresponding_Aspect (N)), Standard_Boolean); - else - Preanalyze_Assert_Expression - (Get_Pragma_Arg (Arg1), Standard_Boolean); - end if; - - -- For a class-wide condition, a reference to a controlling formal must - -- be interpreted as having the class-wide type (or an access to such) - -- so that the inherited condition can be properly applied to any - -- overriding operation (see ARM12 6.6.1 (7)). - - if Class_Present (N) then - Class_Wide_Condition : declare - T : constant Entity_Id := Find_Dispatching_Type (S); - - ACW : Entity_Id := Empty; - -- Access to T'class, created if there is a controlling formal - -- that is an access parameter. - - function Get_ACW return Entity_Id; - -- If the expression has a reference to an controlling access - -- parameter, create an access to T'class for the necessary - -- conversions if one does not exist. - - function Process (N : Node_Id) return Traverse_Result; - -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class - -- aspect for a primitive subprogram of a tagged type T, a name - -- that denotes a formal parameter of type T is interpreted as - -- having type T'Class. Similarly, a name that denotes a formal - -- accessparameter of type access-to-T is interpreted as having - -- type access-to-T'Class. This ensures the expression is well- - -- defined for a primitive subprogram of a type descended from T. - -- Note that this replacement is not done for selector names in - -- parameter associations. These carry an entity for reference - -- purposes, but semantically they are just identifiers. - - ------------- - -- Get_ACW -- - ------------- - - function Get_ACW return Entity_Id is - Loc : constant Source_Ptr := Sloc (N); - Decl : Node_Id; - - begin - if No (ACW) then - Decl := Make_Full_Type_Declaration (Loc, - Defining_Identifier => Make_Temporary (Loc, 'T'), - Type_Definition => - Make_Access_To_Object_Definition (Loc, - Subtype_Indication => - New_Occurrence_Of (Class_Wide_Type (T), Loc), - All_Present => True)); - - Insert_Before (Unit_Declaration_Node (S), Decl); - Analyze (Decl); - ACW := Defining_Identifier (Decl); - Freeze_Before (Unit_Declaration_Node (S), ACW); - end if; - - return ACW; - end Get_ACW; - - ------------- - -- Process -- - ------------- - - function Process (N : Node_Id) return Traverse_Result is - Loc : constant Source_Ptr := Sloc (N); - Typ : Entity_Id; - - begin - if Is_Entity_Name (N) - and then Present (Entity (N)) - and then Is_Formal (Entity (N)) - and then Nkind (Parent (N)) /= N_Type_Conversion - and then - (Nkind (Parent (N)) /= N_Parameter_Association - or else N /= Selector_Name (Parent (N))) - then - if Etype (Entity (N)) = T then - Typ := Class_Wide_Type (T); - - elsif Is_Access_Type (Etype (Entity (N))) - and then Designated_Type (Etype (Entity (N))) = T - then - Typ := Get_ACW; - else - Typ := Empty; - end if; - - if Present (Typ) then - Rewrite (N, - Make_Type_Conversion (Loc, - Subtype_Mark => - New_Occurrence_Of (Typ, Loc), - Expression => New_Occurrence_Of (Entity (N), Loc))); - Set_Etype (N, Typ); - end if; - end if; - - return OK; - end Process; - - procedure Replace_Type is new Traverse_Proc (Process); - - -- Start of processing for Class_Wide_Condition - - begin - if not Present (T) then - Error_Msg_Name_1 := - Chars (Identifier (Corresponding_Aspect (N))); - - Error_Msg_Name_2 := Name_Class; - - Error_Msg_N - ("aspect `%''%` can only be specified for a primitive " - & "operation of a tagged type", Corresponding_Aspect (N)); - end if; - - Replace_Type (Get_Pragma_Arg (Arg1)); - end Class_Wide_Condition; - end if; - - -- Remove the subprogram from the scope stack now that the pre-analysis - -- of the precondition/postcondition is done. - - End_Scope; - end Analyze_PPC_In_Decl_Part; - -------------------- -- Analyze_Pragma -- -------------------- @@ -1922,15 +1779,9 @@ package body Sem_Prag is -- In Ada 95 or 05 mode, these are implementation defined pragmas, so -- should be caught by the No_Implementation_Pragmas restriction. - procedure Analyze_Refined_Pre_Post - (Body_Decl : out Node_Id; - Spec_Id : out Entity_Id; - Legal : out Boolean); + procedure Analyze_Refined_Pre_Post_Condition; -- Subsidiary routine to the analysis of pragmas Refined_Pre and - -- Refined_Post. Body_Decl is the declaration of the subprogram body - -- [stub] subject to the pragma. Spec_Id is the corresponding spec of - -- the subprogram body [stub]. Flag Legal denotes whether the pragma - -- passes all legality rules. + -- Refined_Post. procedure Check_Ada_83_Warning; -- Issues a warning message for the current pragma if operating in Ada @@ -2458,26 +2309,18 @@ package body Sem_Prag is end if; end Ada_2012_Pragma; - ------------------------------ - -- Analyze_Refined_Pre_Post -- - ------------------------------ + ---------------------------------------- + -- Analyze_Refined_Pre_Post_Condition -- + ---------------------------------------- - procedure Analyze_Refined_Pre_Post - (Body_Decl : out Node_Id; - Spec_Id : out Entity_Id; - Legal : out Boolean) - is + procedure Analyze_Refined_Pre_Post_Condition is + Body_Decl : Node_Id := Parent (N); Pack_Spec : Node_Id; Spec_Decl : Node_Id; + Spec_Id : Entity_Id; Stmt : Node_Id; begin - -- Assume that the pragma is illegal - - Body_Decl := Parent (N); - Spec_Id := Empty; - Legal := False; - GNAT_Pragma; Check_Arg_Count (1); Check_No_Identifiers; @@ -2576,10 +2419,10 @@ package body Sem_Prag is return; end if; - -- If we get here, the placement and legality of the pragma is OK + -- Analyze the boolean expression as a "spec expression" - Legal := True; - end Analyze_Refined_Pre_Post; + Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id); + end Analyze_Refined_Pre_Post_Condition; -------------------------- -- Check_Ada_83_Warning -- @@ -3791,7 +3634,7 @@ package body Sem_Prag is -- analyzed. if SPARK_Mode or else ASIS_Mode then - Analyze_PPC_In_Decl_Part + Analyze_Pre_Post_Condition_In_Decl_Part (N, Defining_Entity (Unit (Parent (PO)))); end if; @@ -16092,32 +15935,35 @@ package body Sem_Prag is when Pragma_Rational => Set_Rational_Profile; - ------------------ - -- Refined_Post -- - ------------------ + --------------------- + -- Refined_Depends -- + --------------------- - -- pragma Refined_Post (boolean_EXPRESSION); + -- ??? To be implemented - when Pragma_Refined_Post => Refined_Post : declare - Body_Decl : Node_Id; - Legal : Boolean; - Spec_Id : Entity_Id; + when Pragma_Refined_Depends => + null; - begin - -- Verify the legal placement of the pragma. The pragma is left - -- intentionally semi-analyzed. Process_PPCs does the remaining - -- analysis of the expression when Refined_Post is converted into - -- pragma Check. + -------------------- + -- Refined_Global -- + -------------------- - Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal); + -- ??? To be implemented - -- Analyze the expression when code generation is disabled because - -- the contract of the related subprogram will never be processed. + -- Would be better if these generated an error message saying that + -- the feature was not yet implemented ??? - if Legal and then not Expander_Active then - Analyze_And_Resolve (Get_Pragma_Arg (Arg1), Standard_Boolean); - end if; - end Refined_Post; + when Pragma_Refined_Global => + null; + + ------------------ + -- Refined_Post -- + ------------------ + + -- pragma Refined_Post (boolean_EXPRESSION); + + when Pragma_Refined_Post => + Analyze_Refined_Pre_Post_Condition; ----------------- -- Refined_Pre -- @@ -16125,48 +15971,8 @@ package body Sem_Prag is -- pragma Refined_Pre (boolean_EXPRESSION); - when Pragma_Refined_Pre => Refined_Pre : declare - Body_Decl : Node_Id; - Legal : Boolean; - Restore : Boolean := False; - Spec_Id : Entity_Id; - - begin - Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal); - - if Legal then - pragma Assert (Present (Body_Decl)); - pragma Assert (Present (Spec_Id)); - - if Nkind (Body_Decl) = N_Subprogram_Body_Stub - and then No (Library_Unit (Body_Decl)) - and then Current_Scope /= Spec_Id - then - Restore := True; - Push_Scope (Spec_Id); - Install_Formals (Spec_Id); - end if; - - -- Convert pragma Refined_Pre into pragma Check. The analysis - -- of the generated pragma will take care of the expression. - - Rewrite (N, - Make_Pragma (Loc, - Chars => Name_Check, - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Pname)), - - Make_Pragma_Argument_Association (Sloc (Arg1), - Expression => Relocate_Node (Get_Pragma_Arg (Arg1)))))); - - Analyze (N); - - if Restore then - Pop_Scope; - end if; - end if; - end Refined_Pre; + when Pragma_Refined_Pre => + Analyze_Refined_Pre_Post_Condition; ----------------------- -- Relative_Deadline -- @@ -18499,6 +18305,195 @@ package body Sem_Prag is when Pragma_Exit => null; end Analyze_Pragma; + --------------------------------------------- + -- Analyze_Pre_Post_Condition_In_Decl_Part -- + --------------------------------------------- + + procedure Analyze_Pre_Post_Condition_In_Decl_Part + (Prag : Node_Id; + Subp_Id : Entity_Id) + is + Arg1 : constant Node_Id := + First (Pragma_Argument_Associations (Prag)); + Expr : Node_Id; + Restore : Boolean := False; + + begin + -- Ensure that the subprogram and its formals are visible when analyzing + -- the expression of the pragma. + + if Current_Scope /= Subp_Id then + Restore := True; + Push_Scope (Subp_Id); + Install_Formals (Subp_Id); + end if; + + -- Preanalyze the boolean expression, we treat this as a spec expression + -- (i.e. similar to a default expression). + + Expr := Get_Pragma_Arg (Arg1); + + -- In ASIS mode, for a pragma generated from a source aspect, analyze + -- the original aspect expression, which is shared with the generated + -- pragma. + + if ASIS_Mode and then Present (Corresponding_Aspect (Prag)) then + Expr := Expression (Corresponding_Aspect (Prag)); + end if; + + Preanalyze_Assert_Expression (Expr, Standard_Boolean); + + -- For a class-wide condition, a reference to a controlling formal must + -- be interpreted as having the class-wide type (or an access to such) + -- so that the inherited condition can be properly applied to any + -- overriding operation (see ARM12 6.6.1 (7)). + + if Class_Present (Prag) then + Class_Wide_Condition : declare + T : constant Entity_Id := Find_Dispatching_Type (Subp_Id); + + ACW : Entity_Id := Empty; + -- Access to T'class, created if there is a controlling formal + -- that is an access parameter. + + function Get_ACW return Entity_Id; + -- If the expression has a reference to an controlling access + -- parameter, create an access to T'class for the necessary + -- conversions if one does not exist. + + function Process (N : Node_Id) return Traverse_Result; + -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class + -- aspect for a primitive subprogram of a tagged type T, a name + -- that denotes a formal parameter of type T is interpreted as + -- having type T'Class. Similarly, a name that denotes a formal + -- accessparameter of type access-to-T is interpreted as having + -- type access-to-T'Class. This ensures the expression is well- + -- defined for a primitive subprogram of a type descended from T. + -- Note that this replacement is not done for selector names in + -- parameter associations. These carry an entity for reference + -- purposes, but semantically they are just identifiers. + + ------------- + -- Get_ACW -- + ------------- + + function Get_ACW return Entity_Id is + Loc : constant Source_Ptr := Sloc (Prag); + Decl : Node_Id; + + begin + if No (ACW) then + Decl := + Make_Full_Type_Declaration (Loc, + Defining_Identifier => Make_Temporary (Loc, 'T'), + Type_Definition => + Make_Access_To_Object_Definition (Loc, + Subtype_Indication => + New_Occurrence_Of (Class_Wide_Type (T), Loc), + All_Present => True)); + + Insert_Before (Unit_Declaration_Node (Subp_Id), Decl); + Analyze (Decl); + ACW := Defining_Identifier (Decl); + Freeze_Before (Unit_Declaration_Node (Subp_Id), ACW); + end if; + + return ACW; + end Get_ACW; + + ------------- + -- Process -- + ------------- + + function Process (N : Node_Id) return Traverse_Result is + Loc : constant Source_Ptr := Sloc (N); + Typ : Entity_Id; + + begin + if Is_Entity_Name (N) + and then Present (Entity (N)) + and then Is_Formal (Entity (N)) + and then Nkind (Parent (N)) /= N_Type_Conversion + and then + (Nkind (Parent (N)) /= N_Parameter_Association + or else N /= Selector_Name (Parent (N))) + then + if Etype (Entity (N)) = T then + Typ := Class_Wide_Type (T); + + elsif Is_Access_Type (Etype (Entity (N))) + and then Designated_Type (Etype (Entity (N))) = T + then + Typ := Get_ACW; + else + Typ := Empty; + end if; + + if Present (Typ) then + Rewrite (N, + Make_Type_Conversion (Loc, + Subtype_Mark => + New_Occurrence_Of (Typ, Loc), + Expression => New_Occurrence_Of (Entity (N), Loc))); + Set_Etype (N, Typ); + end if; + end if; + + return OK; + end Process; + + procedure Replace_Type is new Traverse_Proc (Process); + + -- Start of processing for Class_Wide_Condition + + begin + if not Present (T) then + Error_Msg_Name_1 := + Chars (Identifier (Corresponding_Aspect (Prag))); + + Error_Msg_Name_2 := Name_Class; + + Error_Msg_N + ("aspect `%''%` can only be specified for a primitive " + & "operation of a tagged type", Corresponding_Aspect (Prag)); + end if; + + Replace_Type (Get_Pragma_Arg (Arg1)); + end Class_Wide_Condition; + end if; + + -- Remove the subprogram from the scope stack now that the pre-analysis + -- of the precondition/postcondition is done. + + if Restore then + End_Scope; + end if; + end Analyze_Pre_Post_Condition_In_Decl_Part; + + ------------------------------------------ + -- Analyze_Refined_Depends_In_Decl_Part -- + ------------------------------------------ + + -- ??? To be implemented + + procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id) is + pragma Unreferenced (N); + begin + null; + end Analyze_Refined_Depends_In_Decl_Part; + + ----------------------------------------- + -- Analyze_Refined_Global_In_Decl_Part -- + ----------------------------------------- + + -- ??? To be implemented + + procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id) is + pragma Unreferenced (N); + begin + null; + end Analyze_Refined_Global_In_Decl_Part; + ------------------------------------ -- Analyze_Test_Case_In_Decl_Part -- ------------------------------------ @@ -19251,6 +19246,8 @@ package body Sem_Prag is Pragma_Queuing_Policy => -1, Pragma_Rational => -1, Pragma_Ravenscar => -1, + Pragma_Refined_Depends => -1, + Pragma_Refined_Global => -1, Pragma_Refined_Post => -1, Pragma_Refined_Pre => -1, Pragma_Relative_Deadline => -1, diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 492eb9f779f..3b8114fef0d 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -38,11 +38,13 @@ package Sem_Prag is -- the pragmas below implement an aspect. Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean := - (Pragma_Refined_Post => True, - Pragma_Refined_Pre => True, - Pragma_SPARK_Mode => True, - Pragma_Warnings => True, - others => False); + (Pragma_Refined_Depends => True, + Pragma_Refined_Global => True, + Pragma_Refined_Post => True, + Pragma_Refined_Pre => True, + Pragma_SPARK_Mode => True, + Pragma_Warnings => True, + others => False); ----------------- -- Subprograms -- @@ -60,21 +62,27 @@ package Sem_Prag is procedure Analyze_Global_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Global - procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id); - -- Special analyze routine for precondition/postcondition pragma that - -- appears within a declarative part where the pragma is associated - -- with a subprogram specification. N is the pragma node, and S is the - -- entity for the related subprogram. This procedure does a preanalysis - -- of the expressions in the pragma as "spec expressions" (see section - -- in Sem "Handling of Default and Per-Object Expressions..."). + procedure Analyze_Pre_Post_Condition_In_Decl_Part + (Prag : Node_Id; + Subp_Id : Entity_Id); + -- Perform preanalysis of a [refined] precondition or postcondition that + -- appears on a subprogram declaration or body [stub]. Prag denotes the + -- pragma, Subp_Id is the entity of the related subprogram. The preanalysis + -- of the expression is done as "spec expression" (see section "Handling + -- of Default and Per-Object Expressions in Sem). + + procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id); + -- Preform full analysis of delayed pragma Refined_Depends + + procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id); + -- Perform full analysis of delayed pragma Refined_Global procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id); - -- Special analyze routine for contract-case and test-case pragmas that - -- appears within a declarative part where the pragma is associated with - -- a subprogram specification. N is the pragma node, and S is the entity - -- for the related subprogram. This procedure does a preanalysis of the - -- expressions in the pragma as "spec expressions" (see section in Sem - -- "Handling of Default and Per-Object Expressions..."). + -- Perform preanalysis of pragma Test_Case that applies to a subprogram + -- declaration. Parameter N denotes the pragma, S is the entity of the + -- related subprogram. The preanalysis of the expression is done as "spec + -- expression" (see section "Handling of Default and Per-Object Expressions + -- in Sem). procedure Check_Applicable_Policy (N : Node_Id); -- N is either an N_Aspect or an N_Pragma node. There are two cases. If diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index d5681492233..6913c260884 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -212,25 +212,25 @@ package body Sem_Util is -- Add_Contract_Item -- ----------------------- - procedure Add_Contract_Item (Item : Node_Id; Subp_Id : Entity_Id) is + procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id) is Items : constant Node_Id := Contract (Subp_Id); Nam : Name_Id; begin - if Present (Items) and then Nkind (Item) = N_Pragma then - Nam := Pragma_Name (Item); + -- The related subprogram [body] must have a contract and the item to be + -- added must be a pragma. - if Nam_In (Nam, Name_Precondition, Name_Postcondition) then - Set_Next_Pragma (Item, Pre_Post_Conditions (Items)); - Set_Pre_Post_Conditions (Items, Item); + pragma Assert (Present (Items)); + pragma Assert (Nkind (Prag) = N_Pragma); - elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then - Set_Next_Pragma (Item, Contract_Test_Cases (Items)); - Set_Contract_Test_Cases (Items, Item); + Nam := Pragma_Name (Prag); - elsif Nam_In (Nam, Name_Depends, Name_Global) then - Set_Next_Pragma (Item, Classifications (Items)); - Set_Classifications (Items, Item); + -- Contract items related to subprogram bodies + + if Ekind (Subp_Id) = E_Subprogram_Body then + if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then + Set_Next_Pragma (Prag, Classifications (Items)); + Set_Classifications (Items, Prag); -- The pragma is not a proper contract item @@ -238,10 +238,26 @@ package body Sem_Util is raise Program_Error; end if; - -- The subprogram has not been properly decorated or the item is illegal + -- Contract items related to subprogram declarations else - raise Program_Error; + if Nam_In (Nam, Name_Precondition, Name_Postcondition) then + Set_Next_Pragma (Prag, Pre_Post_Conditions (Items)); + Set_Pre_Post_Conditions (Items, Prag); + + elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then + Set_Next_Pragma (Prag, Contract_Test_Cases (Items)); + Set_Contract_Test_Cases (Items, Prag); + + elsif Nam_In (Nam, Name_Depends, Name_Global) then + Set_Next_Pragma (Prag, Classifications (Items)); + Set_Classifications (Items, Prag); + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; end if; end Add_Contract_Item; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 7ea5657aa2b..3053bee8dcd 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -43,10 +43,17 @@ package Sem_Util is -- Add A to the list of access types to process when expanding the -- freeze node of E. - procedure Add_Contract_Item (Item : Node_Id; Subp_Id : Entity_Id); - -- Add a contract item (pragma Precondition, Postcondition, Test_Case, - -- Contract_Cases, Global, Depends) to the contract of a subprogram. Item - -- denotes a pragma and Subp_Id is the related subprogram. + procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id); + -- Add one of the following contract item to the contract of a subprogram. + -- Prag denotes a pragma and Subp_Id is the related subprogram [body]. + -- Contract_Cases + -- Depends + -- Global + -- Postcondition + -- Precondition + -- Refined_Depends + -- Refined_Global + -- Test_Case procedure Add_Global_Declaration (N : Node_Id); -- These procedures adds a declaration N at the library level, to be diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 149d4c411ce..83a1606cb38 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -7143,11 +7143,10 @@ package Sinfo is -------------- -- This node is used to hold the various parts of an entry or subprogram - -- contract, consisting in pre- and postconditions on the one hand, and - -- test-cases on the other hand. + -- [body] contract, consisting of precondition, postconditions, contract + -- cases, test cases and global dependencies. - -- It is referenced from an entry, a subprogram or a generic subprogram - -- entity. + -- The node appears in an entry and [generic] subprogram [body] entity. -- Sprint syntax: <none> as the node should not appear in the tree, but -- only attached to an entry or [generic] subprogram @@ -7160,9 +7159,10 @@ package Sinfo is -- Classifications (Node3) (set to Empty if none) -- Pre_Post_Conditions contains a collection of pragmas that correspond - -- to pre- and postconditions associated with an entry or a subprogram. - -- The pragmas can either come from source or be the byproduct of aspect - -- expansion. The ordering in the list is in LIFO fashion. + -- to pre- and postconditions associated with an entry or a subprogram + -- [body or stub]. The pragmas can either come from source or be the + -- byproduct of aspect expansion. The ordering in the list is in LIFO + -- fashion. -- Note that there might be multiple preconditions or postconditions -- in this list, either because they come from separate pragmas in the @@ -7175,8 +7175,8 @@ package Sinfo is -- Classifications contains pragmas that either categorize subprogram -- inputs and outputs or establish dependencies between them. Currently - -- pragmas Depends and Global are stored in this list. The ordering is - -- in LIFO fashion. + -- pragmas Depends, Global, Refined_Depends and Refined_Global are + -- stored in this list. The ordering is in LIFO fashion. ------------------- -- Expanded_Name -- diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 9752d2b16f9..8aed6308bae 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -580,6 +580,8 @@ package Snames is Name_Pure_05 : constant Name_Id := N + $; -- GNAT Name_Pure_12 : constant Name_Id := N + $; -- GNAT Name_Pure_Function : constant Name_Id := N + $; -- GNAT + Name_Refined_Depends : constant Name_Id := N + $; -- GNAT + Name_Refined_Global : constant Name_Id := N + $; -- GNAT Name_Refined_Post : constant Name_Id := N + $; -- GNAT Name_Refined_Pre : constant Name_Id := N + $; -- GNAT Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05 @@ -1865,6 +1867,8 @@ package Snames is Pragma_Pure_05, Pragma_Pure_12, Pragma_Pure_Function, + Pragma_Refined_Depends, + Pragma_Refined_Global, Pragma_Refined_Post, Pragma_Refined_Pre, Pragma_Relative_Deadline, diff --git a/gcc/ada/types.ads b/gcc/ada/types.ads index 19e633ab209..4888d69e190 100644 --- a/gcc/ada/types.ads +++ b/gcc/ada/types.ads @@ -172,7 +172,7 @@ package Types is for Physical_Line_Number'Size use 32; -- Line number type, used for storing physical line numbers (i.e. line -- numbers in the physical file being compiled, unaffected by the presence - -- of source reference pragmas. + -- of source reference pragmas). type Column_Number is range 0 .. 32767; for Column_Number'Size use 16; |
