From 27bb79414764b83bf6c7208d6081afd01f98869f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 13 Jan 2017 10:59:17 +0100 Subject: [PATCH] [multiple changes] 2017-01-13 Hristian Kirtchev * exp_util.adb (Add_Inherited_Tagged_DIC): Pass the object parameters of both the parent and the derived type DIC procedure to the reference replacement circuitry. (Find_DIC_Type): Modify the circuitry to present the partial view of a private type in case the private type defines its own DIC pragma. (Replace_Object_And_Primitive_References): Add two optional formal parameters. Update the comment on usage. Update the replacement of references to object parameters. 2017-01-13 Gary Dismukes * einfo.adb, sem_ch6.adb, atree.adb: Minor reformatting and typo fix. 2017-01-13 Ed Schonberg * sem_res.adb (Resolve_Actuals): Apply Scalar_Range_Check to an out parameter that is a type conversion, independently of th range check that may apply to the expression of the conversion, for use in GNATProve. 2017-01-13 Yannick Moy * gnat1drv.adb (Gnat1drv): Move the implicit with for System in GNATprove_Mode here to Frontend. * frontend.adb (Frontend): Move the implicit with for System in GNATprove_Mode here as it ismore correct this way; the old place only worked by chance, since there were no overloaded names. * rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Tasking_State. * sem_attr.adb (Analyze_Attribute): In GNATprove_Mode, for the four attributes identified in SRM 9(18), add an implicit with to Ada.Task_Identification. * sem_ch8.adb (Analyze_Subprogram_Renaming.Build_Class_Wide_Wrapper): Deal specially with the wrapper introduced for AI05-0071 in GNATprove mode. * checks.adb (Apply_Discriminant_Check, Apply_Selected_Length_Checks, Apply_Selected_Range_Checks): In GNATprove mode, we do not apply the checks, but we still analyze the expression to possibly issue errors on SPARK code when a run-time error can be detected at compile time. (Selected_Length_Checks, Selected_Range_Checks): Perform analysis in GNATprove mode. From-SVN: r244398 --- gcc/ada/ChangeLog | 45 ++++++++++++++++++ gcc/ada/atree.adb | 4 +- gcc/ada/checks.adb | 66 +++++++++++++++++++++------ gcc/ada/einfo.adb | 8 ++-- gcc/ada/exp_util.adb | 82 ++++++++++++++++++--------------- gcc/ada/frontend.adb | 13 ++++++ gcc/ada/gnat1drv.adb | 13 ------ gcc/ada/rtsfind.ads | 2 + gcc/ada/sem_attr.adb | 21 +++++++++ gcc/ada/sem_ch6.adb | 8 ++-- gcc/ada/sem_ch8.adb | 106 ++++++++++++++++++++++++++++++++++++------- gcc/ada/sem_res.adb | 18 ++++++-- 12 files changed, 293 insertions(+), 93 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0569679f841..f9d3a503035 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,48 @@ +2017-01-13 Hristian Kirtchev + + * exp_util.adb (Add_Inherited_Tagged_DIC): + Pass the object parameters of both the parent and the derived + type DIC procedure to the reference replacement circuitry. + (Find_DIC_Type): Modify the circuitry to present the partial + view of a private type in case the private type defines its own + DIC pragma. + (Replace_Object_And_Primitive_References): Add two + optional formal parameters. Update the comment on usage. Update + the replacement of references to object parameters. + +2017-01-13 Gary Dismukes + + * einfo.adb, sem_ch6.adb, atree.adb: Minor reformatting and typo fix. + +2017-01-13 Ed Schonberg + + * sem_res.adb (Resolve_Actuals): Apply Scalar_Range_Check to + an out parameter that is a type conversion, independently of th + range check that may apply to the expression of the conversion, + for use in GNATProve. + +2017-01-13 Yannick Moy + + * gnat1drv.adb (Gnat1drv): Move the implicit with for System in + GNATprove_Mode here to Frontend. + * frontend.adb (Frontend): Move the implicit with for System + in GNATprove_Mode here as it ismore correct this way; the old + place only worked by chance, since there were no overloaded names. + * rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Tasking_State. + * sem_attr.adb (Analyze_Attribute): In GNATprove_Mode, for the + four attributes identified in SRM 9(18), add an implicit with + to Ada.Task_Identification. + * sem_ch8.adb (Analyze_Subprogram_Renaming.Build_Class_Wide_Wrapper): + Deal specially with the wrapper introduced for AI05-0071 in GNATprove + mode. + * checks.adb (Apply_Discriminant_Check, + Apply_Selected_Length_Checks, Apply_Selected_Range_Checks): + In GNATprove mode, we do not apply the checks, but we still + analyze the expression to possibly issue errors on SPARK + code when a run-time error can be detected at compile time. + (Selected_Length_Checks, Selected_Range_Checks): Perform analysis + in GNATprove mode. + 2017-01-13 Hristian Kirtchev * expander.adb (Expand): Add a warning about using return diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 1444fcb6dfe..2e56371600b 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -556,7 +556,7 @@ package body Atree is -- information for the newly-allocated node is copied from it. procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id); - -- Fixup parent pointers for the syntactic children of Fix_Node after a + -- Fix up parent pointers for the syntactic children of Fix_Node after a -- copy, setting them to Fix_Node when they pointed to Ref_Node. procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id); @@ -1430,7 +1430,7 @@ package body Atree is procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id) is procedure Fix_Parent (Field : Union_Id); - -- Fixup one parent pointer. Field is checked to see if it points to + -- Fix up one parent pointer. Field is checked to see if it points to -- a node, list, or element list that has a parent that points to -- Ref_Node. If so, the parent is reset to point to Fix_Node. diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 10dbbaf75e9..6689cb56f07 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -1447,13 +1447,17 @@ package body Checks is T_Typ := Typ; end if; - -- Nothing to do if discriminant checks are suppressed or else no code - -- is to be generated - - if not Expander_Active - or else Discriminant_Checks_Suppressed (T_Typ) - then - return; + -- Only apply checks when generating code and discriminant checks are + -- not suppressed. In GNATprove mode, we do not apply the checks, but we + -- still analyze the expression to possibly issue errors on SPARK code + -- when a run-time error can be detected at compile time. + + if not GNATprove_Mode then + if not Expander_Active + or else Discriminant_Checks_Suppressed (T_Typ) + then + return; + end if; end if; -- No discriminant checks necessary for an access when expression is @@ -1690,6 +1694,12 @@ package body Checks is end; end if; + -- In GNATprove mode, we do not apply the checks + + if GNATprove_Mode then + return; + end if; + -- Here we need a discriminant check. First build the expression -- for the comparisons of the discriminants: @@ -3075,16 +3085,25 @@ package body Checks is or else (not Length_Checks_Suppressed (Target_Typ)); begin + -- Only apply checks when generating code. In GNATprove mode, we do + -- not apply the checks, but we still call Selected_Length_Checks to + -- possibly issue errors on SPARK code when a run-time error can be + -- detected at compile time. + -- Note: this means that we lose some useful warnings if the expander - -- is not active, and we also lose these warnings in SPARK mode ??? + -- is not active. - if not Expander_Active then + if not Expander_Active and not GNATprove_Mode then return; end if; R_Result := Selected_Length_Checks (Ck_Node, Target_Typ, Source_Typ, Empty); + if GNATprove_Mode then + return; + end if; + for J in 1 .. 2 loop R_Cno := R_Result (J); exit when No (R_Cno); @@ -3186,13 +3205,24 @@ package body Checks is R_Result : Check_Result; begin - if not Expander_Active or not Checks_On then - return; + -- Only apply checks when generating code. In GNATprove mode, we do not + -- apply the checks, but we still call Selected_Range_Checks to possibly + -- issue errors on SPARK code when a run-time error can be detected at + -- compile time. + + if not GNATprove_Mode then + if not Expander_Active or not Checks_On then + return; + end if; end if; R_Result := Selected_Range_Checks (Ck_Node, Target_Typ, Source_Typ, Empty); + if GNATprove_Mode then + return; + end if; + for J in 1 .. 2 loop R_Cno := R_Result (J); exit when No (R_Cno); @@ -9052,7 +9082,12 @@ package body Checks is -- Start of processing for Selected_Length_Checks begin - if not Expander_Active then + -- Checks will be applied only when generating code. In GNATprove mode, + -- we do not apply the checks, but we still call Selected_Length_Checks + -- to possibly issue errors on SPARK code when a run-time error can be + -- detected at compile time. + + if not Expander_Active and not GNATprove_Mode then return Ret_Result; end if; @@ -9602,7 +9637,12 @@ package body Checks is -- Start of processing for Selected_Range_Checks begin - if not Expander_Active then + -- Checks will be applied only when generating code. In GNATprove mode, + -- we do not apply the checks, but we still call Selected_Range_Checks + -- to possibly issue errors on SPARK code when a run-time error can be + -- detected at compile time. + + if not Expander_Active and not GNATprove_Mode then return Ret_Result; end if; diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index c2146756843..f007c2a4e3d 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -2093,7 +2093,7 @@ package body Einfo is function Is_Checked_Ghost_Entity (Id : E) return B is begin - -- Allow this attribute to appear on non-analyzed entities + -- Allow this attribute to appear on unanalyzed entities pragma Assert (Nkind (Id) in N_Entity or else Ekind (Id) = E_Void); @@ -2283,7 +2283,7 @@ package body Einfo is function Is_Ignored_Ghost_Entity (Id : E) return B is begin - -- Allow this attribute to appear on non-analyzed entities + -- Allow this attribute to appear on unanalyzed entities pragma Assert (Nkind (Id) in N_Entity or else Ekind (Id) = E_Void); @@ -5167,7 +5167,7 @@ package body Einfo is procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is begin - -- Allow this attribute to appear on non-analyzed entities + -- Allow this attribute to appear on unanalyzed entities pragma Assert (Nkind (Id) in N_Entity or else Ekind (Id) = E_Void); @@ -5372,7 +5372,7 @@ package body Einfo is procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is begin - -- Allow this attribute to appear on non-analyzed entities + -- Allow this attribute to appear on unanalyzed entities pragma Assert (Nkind (Id) in N_Entity or else Ekind (Id) = E_Void); diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 3d09a963865..ea71e38fe0b 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1237,14 +1237,17 @@ package body Exp_Util is procedure Replace_Object_And_Primitive_References (Expr : Node_Id; Par_Typ : Entity_Id; - Deriv_Typ : Entity_Id); + Deriv_Typ : Entity_Id; + Par_Obj : Entity_Id := Empty; + Deriv_Obj : Entity_Id := Empty); -- Expr denotes an arbitrary expression. Par_Typ is a parent type in a - -- type hierarchy. Deriv_Typ is a type derived from Par_Typ. Perform the - -- following substitutions: + -- type hierarchy. Deriv_Typ is a type derived from Par_Typ. Par_Obj is + -- the formal parameter which emulates the current instance of Par_Typ. + -- Deriv_Obj is the formal parameter which emulates the current instance + -- of Deriv_Typ. Perform the following substitutions: -- - -- * Replace a reference to the _object parameter of the parent type's - -- DIC procedure with a reference to the _object parameter of the - -- derived type's DIC procedure. + -- * Replace a reference to Par_Obj with a reference to Deriv_Obj if + -- applicable. -- -- * Replace a call to an overridden parent primitive with a call to -- the overriding derived type primitive. @@ -1340,11 +1343,13 @@ package body Exp_Util is Deriv_Typ : Entity_Id; Stmts : in out List_Id) is - DIC_Args : constant List_Id := - Pragma_Argument_Associations (DIC_Prag); - DIC_Arg : constant Node_Id := First (DIC_Args); - DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg); - Typ_Decl : constant Node_Id := Declaration_Node (Deriv_Typ); + Deriv_Decl : constant Node_Id := Declaration_Node (Deriv_Typ); + Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ); + DIC_Args : constant List_Id := + Pragma_Argument_Associations (DIC_Prag); + DIC_Arg : constant Node_Id := First (DIC_Args); + DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg); + Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ); Expr : Node_Id; @@ -1373,15 +1378,19 @@ package body Exp_Util is -- handled by the overriding/inheritance mechanism and do not require -- an extra replacement pass. + pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc)); + Replace_Object_And_Primitive_References (Expr => Expr, Par_Typ => Par_Typ, - Deriv_Typ => Deriv_Typ); + Deriv_Typ => Deriv_Typ, + Par_Obj => First_Formal (Par_Proc), + Deriv_Obj => First_Formal (Deriv_Proc)); -- Preanalyze the DIC expression to detect errors and at the same -- time capture the visibility of the proper package part. - Set_Parent (Expr, Typ_Decl); + Set_Parent (Expr, Deriv_Decl); Preanalyze_Assert_Expression (Expr, Any_Boolean); -- Once the DIC assertion expression is fully processed, add a check @@ -1514,14 +1523,10 @@ package body Exp_Util is procedure Replace_Object_And_Primitive_References (Expr : Node_Id; Par_Typ : Entity_Id; - Deriv_Typ : Entity_Id) + Deriv_Typ : Entity_Id; + Par_Obj : Entity_Id := Empty; + Deriv_Obj : Entity_Id := Empty) is - Deriv_Obj : Entity_Id; - -- The _object parameter of the derived type's DIC procedure - - Par_Obj : Entity_Id; - -- The _object parameter of the parent type's DIC procedure - function Replace_Ref (Ref : Node_Id) return Traverse_Result; -- Substitute a reference to an entity with a reference to the -- corresponding entity stored in in table Primitives_Mapping. @@ -1556,7 +1561,10 @@ package body Exp_Util is -- The reference mentions the _object parameter of the parent -- type's DIC procedure. - elsif Ref_Id = Par_Obj then + elsif Present (Par_Obj) + and then Present (Deriv_Obj) + and then Ref_Id = Par_Obj + then New_Ref := New_Occurrence_Of (Deriv_Obj, Loc); -- The reference to _object acts as an actual parameter in a @@ -1624,19 +1632,9 @@ package body Exp_Util is procedure Replace_Refs is new Traverse_Proc (Replace_Ref); - -- Local variables - - Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ); - Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ); - -- Start of processing for Replace_Object_And_Primitive_References begin - pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc)); - - Deriv_Obj := First_Entity (Deriv_Proc); - Par_Obj := First_Entity (Par_Proc); - -- Map each primitive operation of the parent type to the proper -- primitive of the derived type. @@ -3908,7 +3906,15 @@ package body Exp_Util is function Find_DIC_Type (Typ : Entity_Id) return Entity_Id is Curr_Typ : Entity_Id; - DIC_Typ : Entity_Id; + -- The current type being examined in the parent hierarchy traversal + + DIC_Typ : Entity_Id; + -- The type which carries the DIC pragma. This variable denotes the + -- partial view when private types are involved. + + Par_Typ : Entity_Id; + -- The parent type of the current type. This variable denotes the full + -- view when private types are involved. begin -- The input type defines its own DIC pragma, therefore it is the owner @@ -3933,19 +3939,21 @@ package body Exp_Util is -- Look at the full view of a private type because the type may -- have a hidden parent introduced in the full view. - if Is_Private_Type (DIC_Typ) - and then Present (Full_View (DIC_Typ)) + Par_Typ := DIC_Typ; + + if Is_Private_Type (Par_Typ) + and then Present (Full_View (Par_Typ)) then - DIC_Typ := Full_View (DIC_Typ); + Par_Typ := Full_View (Par_Typ); end if; -- Stop the climb once the nearest parent type which defines a DIC -- pragma of its own is encountered or when the root of the parent -- chain is reached. - exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = DIC_Typ; + exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = Par_Typ; - Curr_Typ := DIC_Typ; + Curr_Typ := Par_Typ; end loop; end if; diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb index ff5418a1340..c71c78e40c4 100644 --- a/gcc/ada/frontend.adb +++ b/gcc/ada/frontend.adb @@ -460,6 +460,19 @@ begin end if; end if; + -- In GNATprove mode, force loading of a few RTE units. + + if GNATprove_Mode then + declare + Unused_E : Entity_Id; + begin + -- Ensure that System.Interrupt_Priority is available to + -- GNATprove for the generation of VCs related to ceiling + -- priority. + Unused_E := RTE (RE_Interrupt_Priority); + end; + end if; + -- Qualify all entity names in inner packages, package bodies, etc. Exp_Dbug.Qualify_All_Entity_Names; diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 1bf10b6b4b4..a2e6e897b74 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -1071,19 +1071,6 @@ begin Original_Operating_Mode := Operating_Mode; Frontend; - -- In GNATprove mode, force loading of System unit to ensure that - -- System.Interrupt_Priority is available to GNATprove for the - -- generation of VCs related to ceiling priority. - - if GNATprove_Mode then - declare - Unused_E : constant Entity_Id := - Rtsfind.RTE (Rtsfind.RE_Interrupt_Priority); - begin - null; - end; - end if; - -- Exit with errors if the main source could not be parsed if Sinput.Main_Source_File = No_Source_File then diff --git a/gcc/ada/rtsfind.ads b/gcc/ada/rtsfind.ads index a79064644d9..f3dfd3191a0 100644 --- a/gcc/ada/rtsfind.ads +++ b/gcc/ada/rtsfind.ads @@ -704,6 +704,7 @@ package Rtsfind is RE_Abort_Task, -- Ada.Task_Identification RE_Current_Task, -- Ada.Task_Identification RO_AT_Task_Id, -- Ada.Task_Identification + RE_Tasking_State, -- Ada.Task_Identification RE_Decimal_IO, -- Ada.Text_IO RE_Fixed_IO, -- Ada.Text_IO @@ -1936,6 +1937,7 @@ package Rtsfind is RE_Abort_Task => Ada_Task_Identification, RE_Current_Task => Ada_Task_Identification, RO_AT_Task_Id => Ada_Task_Identification, + RE_Tasking_State => Ada_Task_Identification, RE_Decimal_IO => Ada_Text_IO, RE_Fixed_IO => Ada_Text_IO, diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 494579ac9f8..9adbe7a2e55 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -7109,6 +7109,27 @@ package body Sem_Attr is end case; + -- In SPARK some attribute references depend on Tasking_State, so we + -- need to make sure we load this so that gnat2why has the entity + -- available. See SPARK RM 9(18) for the relevant rule. + + if GNATprove_Mode then + declare + Unused : Entity_Id; + begin + case Attr_Id is + when Attribute_Callable | + Attribute_Caller | + Attribute_Count | + Attribute_Terminated => + Unused := RTE (RE_Tasking_State); + + when others => + null; + end case; + end; + end if; + -- All errors raise Bad_Attribute, so that we get out before any further -- damage occurs when an error is detected (for example, if we check for -- one attribute expression, and the check succeeds, we want to be able diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 33233bdb854..d092134d73d 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -8408,7 +8408,7 @@ package body Sem_Ch6 is -- Start of processing for Fully_Conformant_Expressions begin - -- Non-conformant if paren count does not match. Note: if some idiot + -- Nonconformant if paren count does not match. Note: if some idiot -- complains that we don't do this right for more than 3 levels of -- parentheses, they will be treated with the respect they deserve. @@ -8423,14 +8423,14 @@ package body Sem_Ch6 is return Entity (E1) = Entity (E2) -- One may be a discriminant that has been replaced by - -- the correspondding discriminal + -- the corresponding discriminal. or else (Chars (Entity (E1)) = Chars (Entity (E2)) and then Ekind (Entity (E1)) = E_Discriminant and then Ekind (Entity (E2)) = E_In_Parameter) - -- AI12-050 : the loop variables of quantified expressions - -- match if the have the same identifier, even though they + -- AI12-050 : The loop variables of quantified expressions + -- match if they have the same identifier, even though they -- are different entities. or else (Chars (Entity (E1)) = Chars (Entity (E2)) diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 86eed89bd7b..1ba49628396 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -1934,6 +1934,14 @@ package body Sem_Ch8 is is Loc : constant Source_Ptr := Sloc (N); + function Build_Expr_Fun_Call + (Subp_Id : Entity_Id; + Params : List_Id) return Node_Id; + -- Create a dispatching call to invoke function Subp_Id with actuals + -- built from the parameter specifications of list Params. Return + -- directly the call, so that it can be used inside an expression + -- function. This is a specificity of the GNATprove mode. + function Build_Call (Subp_Id : Entity_Id; Params : List_Id) return Node_Id; @@ -2004,6 +2012,38 @@ package body Sem_Ch8 is end if; end Build_Call; + ------------------------- + -- Build_Expr_Fun_Call -- + ------------------------- + + function Build_Expr_Fun_Call + (Subp_Id : Entity_Id; + Params : List_Id) return Node_Id + is + Actuals : constant List_Id := New_List; + Call_Ref : constant Node_Id := New_Occurrence_Of (Subp_Id, Loc); + Formal : Node_Id; + + begin + -- Build the actual parameters of the call + + Formal := First (Params); + while Present (Formal) loop + Append_To (Actuals, + Make_Identifier (Loc, Chars (Defining_Identifier (Formal)))); + Next (Formal); + end loop; + + -- Generate: + -- Subp_Id (Actuals); + + pragma Assert (Ekind_In (Subp_Id, E_Function, E_Operator)); + + return Make_Function_Call (Loc, + Name => Call_Ref, + Parameter_Associations => Actuals); + end Build_Expr_Fun_Call; + ---------------- -- Build_Spec -- ---------------- @@ -2199,6 +2239,7 @@ package body Sem_Ch8 is Formal : Node_Id; Prim_Op : Entity_Id; Spec_Decl : Node_Id; + New_Spec : Node_Id; -- Start of processing for Build_Class_Wide_Wrapper @@ -2334,31 +2375,62 @@ package body Sem_Ch8 is -- Step 3: Create the declaration and the body of the wrapper, insert -- all the pieces into the tree. - Spec_Decl := - Make_Subprogram_Declaration (Loc, - Specification => Build_Spec (Ren_Id)); - Insert_Before_And_Analyze (N, Spec_Decl); + -- In GNATprove mode, create a function wrapper in the form of an + -- expression function, so that an implicit postcondition relating + -- the result of calling the wrapper function and the result of the + -- dispatching call to the wrapped function is known during proof. + + if GNATprove_Mode + and then Ekind_In (Ren_Id, E_Function, E_Operator) + then + New_Spec := Build_Spec (Ren_Id); + Body_Decl := + Make_Expression_Function (Loc, + Specification => New_Spec, + Expression => Build_Expr_Fun_Call + (Subp_Id => Prim_Op, + Params => Parameter_Specifications (New_Spec))); + + Wrap_Id := Defining_Entity (Body_Decl); + + -- Otherwise, create separate spec and body for the subprogram + + else + Spec_Decl := + Make_Subprogram_Declaration (Loc, + Specification => Build_Spec (Ren_Id)); + Insert_Before_And_Analyze (N, Spec_Decl); + + Wrap_Id := Defining_Entity (Spec_Decl); + + Body_Decl := + Make_Subprogram_Body (Loc, + Specification => Build_Spec (Ren_Id), + Declarations => New_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List ( + Build_Call + (Subp_Id => Prim_Op, + Params => + Parameter_Specifications + (Specification (Spec_Decl)))))); + + Set_Corresponding_Body (Spec_Decl, Defining_Entity (Body_Decl)); + end if; -- If the operator carries an Eliminated pragma, indicate that the -- wrapper is also to be eliminated, to prevent spurious error when -- using gnatelim on programs that include box-initialization of -- equality operators. - Wrap_Id := Defining_Entity (Spec_Decl); Set_Is_Eliminated (Wrap_Id, Is_Eliminated (Prim_Op)); - Body_Decl := - Make_Subprogram_Body (Loc, - Specification => Build_Spec (Ren_Id), - Declarations => New_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => New_List ( - Build_Call - (Subp_Id => Prim_Op, - Params => - Parameter_Specifications - (Specification (Spec_Decl)))))); + -- In GNATprove mode, insert the body in the tree for analysis + + if GNATprove_Mode then + Insert_Before_And_Analyze (N, Body_Decl); + end if; -- The generated body does not freeze and must be analyzed when the -- class-wide wrapper is frozen. The body is only needed if expansion diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index fc377a952fd..235a535c7f9 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -4328,24 +4328,36 @@ package body Sem_Res is if Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) then - -- If there is a type conversion, to make sure the return value + -- If there is a type conversion, make sure the return value -- meets the constraints of the variable before the conversion. if Nkind (A) = N_Type_Conversion then if Is_Scalar_Type (A_Typ) then Apply_Scalar_Range_Check (Expression (A), Etype (Expression (A)), A_Typ); + + -- In addition, the returned value of the parameter + -- must satisfy the bounds of the object type (see + -- comment below). + + Apply_Scalar_Range_Check (A, A_Typ, F_Typ); + else Apply_Range_Check (Expression (A), Etype (Expression (A)), A_Typ); end if; - -- If no conversion apply scalar range checks and length checks - -- base on the subtype of the actual (NOT that of the formal). + -- If no conversion, apply scalar range checks and length check + -- based on the subtype of the actual (NOT that of the formal). + -- This indicates that the check takes place on return from the + -- call. During expansion the required constraint checks are + -- inserted. In GNATprove mode, in the absence of expansion, + -- the flag indicates that the returned value is valid. else if Is_Scalar_Type (F_Typ) then Apply_Scalar_Range_Check (A, A_Typ, F_Typ); + elsif Is_Array_Type (F_Typ) and then Ekind (F) = E_Out_Parameter then -- 2.30.2