From 948ed277461760a367678c9afbd55e45eda8707e Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 6 Jan 2015 10:20:55 +0100 Subject: [PATCH] [multiple changes] 2015-01-06 Ed Schonberg * sem_ch6.adb (New_Overloaded_Entity): In GNATprove mode, a function wrapper may be a homonym of another local declaration. * sem_ch8.adb (Analyze_Subprogram_Renaming): In GNATprove mode, build function and operator wrappers after the actual subprogram has been resolved, and replace the standard renaming declaration with the declaration of wrapper. * sem_ch12.ads (Build_Function_Wrapper, Build_Operator_Wraooer): make public for use elsewhere. * sem_ch12.adb (Build_Function_Wrapper, Build_Operator_Wraooer): rewrite, now that actual is fully resolved when wrapper is constructed. 2015-01-06 Javier Miranda * exp_disp.adb: Revert previous change. From-SVN: r219232 --- gcc/ada/ChangeLog | 18 ++ gcc/ada/exp_disp.adb | 24 +-- gcc/ada/sem_ch12.adb | 548 +++++++++++++++++++++------------------------------ gcc/ada/sem_ch12.ads | 18 +- gcc/ada/sem_ch6.adb | 21 +- gcc/ada/sem_ch8.adb | 18 ++ 6 files changed, 296 insertions(+), 351 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index dde69e5..2685b58 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,21 @@ +2015-01-06 Ed Schonberg + + * sem_ch6.adb (New_Overloaded_Entity): In GNATprove mode, a + function wrapper may be a homonym of another local declaration. + * sem_ch8.adb (Analyze_Subprogram_Renaming): In GNATprove mode, + build function and operator wrappers after the actual subprogram + has been resolved, and replace the standard renaming declaration + with the declaration of wrapper. + * sem_ch12.ads (Build_Function_Wrapper, Build_Operator_Wraooer): + make public for use elsewhere. + * sem_ch12.adb (Build_Function_Wrapper, Build_Operator_Wraooer): + rewrite, now that actual is fully resolved when wrapper is + constructed. + +2015-01-06 Javier Miranda + + * exp_disp.adb: Revert previous change. + 2015-01-06 Robert Dewar * exp_util.adb: Change name Name_Table_Boolean to diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 302f721..99105e0 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -1138,25 +1138,6 @@ package body Exp_Disp is Operand_Typ := Base_Type (Corresponding_Record_Type (Operand_Typ)); end if; - -- No displacement of the pointer to the object needed when the type of - -- the operand is not an interface type and the interface is one of - -- its parent types (since they share the primary dispatch table). - - declare - Opnd : Entity_Id := Operand_Typ; - - begin - if Is_Access_Type (Opnd) then - Opnd := Designated_Type (Opnd); - end if; - - if not Is_Interface (Opnd) - and then Is_Ancestor (Iface_Typ, Opnd, Use_Full_View => True) - then - return; - end if; - end; - -- Evaluate if we can statically displace the pointer to the object declare @@ -1196,6 +1177,11 @@ package body Exp_Disp is Prefix => New_Occurrence_Of (Iface_Typ, Loc), Attribute_Name => Name_Tag)))); end if; + + -- Just do a conversion ??? + + Rewrite (N, Unchecked_Convert_To (Etype (N), N)); + Analyze (N); end if; return; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 7861c45..905181d 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -30,7 +30,6 @@ with Elists; use Elists; with Errout; use Errout; with Expander; use Expander; with Exp_Disp; use Exp_Disp; -with Exp_Util; use Exp_Util; with Fname; use Fname; with Fname.UF; use Fname.UF; with Freeze; use Freeze; @@ -954,24 +953,6 @@ package body Sem_Ch12 is -- In Ada 2005, indicates partial parameterization of a formal -- package. As usual an other association must be last in the list. - function Build_Function_Wrapper - (Formal : Entity_Id; - Actual : Entity_Id := Empty) return Node_Id; - -- In GNATprove mode, create a wrapper function for actuals that are - -- functions with any number of formal parameters, in order to propagate - -- their contract to the renaming declarations generated for them. - -- If the actual is absent, the formal has a default, and the name of - -- the function is that of the formal. - - function Build_Operator_Wrapper - (Formal : Entity_Id; - Actual : Entity_Id := Empty) return Node_Id; - -- In GNATprove mode, create a wrapper function for actuals that are - -- operators, in order to propagate their contract to the renaming - -- declarations generated for them. If the actual is absent, this is - -- a formal with a default, and the name of the operator is that of the - -- formal. - procedure Check_Overloaded_Formal_Subprogram (Formal : Entity_Id); -- Apply RM 12.3 (9): if a formal subprogram is overloaded, the instance -- cannot have a named association for it. AI05-0025 extends this rule @@ -1019,257 +1000,6 @@ package body Sem_Ch12 is -- anonymous types, the presence a formal equality will introduce an -- implicit declaration for the corresponding inequality. - ---------------------------- - -- Build_Function_Wrapper -- - ---------------------------- - - function Build_Function_Wrapper - (Formal : Entity_Id; - Actual : Entity_Id := Empty) return Node_Id - is - Loc : constant Source_Ptr := Sloc (I_Node); - Actuals : List_Id; - Decl : Node_Id; - Func_Name : Node_Id; - Func : Entity_Id; - Parm_Type : Node_Id; - Profile : List_Id := New_List; - Spec : Node_Id; - Act_F : Entity_Id; - Form_F : Entity_Id; - New_F : Entity_Id; - - begin - -- If there is no actual, the formal has a default and is retrieved - -- by name. Otherwise the wrapper encloses a call to the actual. - - if No (Actual) then - Func_Name := Make_Identifier (Loc, Chars (Formal)); - else - Func_Name := New_Occurrence_Of (Entity (Actual), Loc); - end if; - - Func := Make_Defining_Identifier (Loc, Chars (Formal)); - Set_Ekind (Func, E_Function); - Set_Is_Generic_Actual_Subprogram (Func); - - Actuals := New_List; - Profile := New_List; - - if Present (Actual) then - Act_F := First_Formal (Entity (Actual)); - else - Act_F := Empty; - end if; - - Form_F := First_Formal (Formal); - while Present (Form_F) loop - - -- Create new formal for profile of wrapper, and add a reference - -- to it in the list of actuals for the enclosing call. The name - -- must be that of the formal in the formal subprogram, because - -- calls to it in the generic body may use named associations. - - New_F := Make_Defining_Identifier (Loc, Chars (Form_F)); - - if No (Actual) then - - -- If formal has a class-wide type rewrite as the corresponding - -- attribute, because the class-wide type is not retrievable by - -- visbility. - - if Is_Class_Wide_Type (Etype (Form_F)) then - Parm_Type := - Make_Attribute_Reference (Loc, - Attribute_Name => Name_Class, - Prefix => - Make_Identifier (Loc, Chars (Etype (Etype (Form_F))))); - - else - Parm_Type := - Make_Identifier (Loc, - Chars => Chars (First_Subtype (Etype (Form_F)))); - end if; - - -- If actual is present, use the type of its own formal - - else - Parm_Type := New_Occurrence_Of (Etype (Act_F), Loc); - end if; - - Append_To (Profile, - Make_Parameter_Specification (Loc, - Defining_Identifier => New_F, - Parameter_Type => Parm_Type)); - - Append_To (Actuals, New_Occurrence_Of (New_F, Loc)); - Next_Formal (Form_F); - - if Present (Act_F) then - Next_Formal (Act_F); - end if; - end loop; - - Spec := - Make_Function_Specification (Loc, - Defining_Unit_Name => Func, - Parameter_Specifications => Profile, - Result_Definition => - Make_Identifier (Loc, Chars (Etype (Formal)))); - - Decl := - Make_Expression_Function (Loc, - Specification => Spec, - Expression => - Make_Function_Call (Loc, - Name => Func_Name, - Parameter_Associations => Actuals)); - - return Decl; - end Build_Function_Wrapper; - - ---------------------------- - -- Build_Operator_Wrapper -- - ---------------------------- - - function Build_Operator_Wrapper - (Formal : Entity_Id; - Actual : Entity_Id := Empty) return Node_Id - is - Loc : constant Source_Ptr := Sloc (I_Node); - Typ : constant Entity_Id := Etype (Formal); - Is_Binary : constant Boolean := - Present (Next_Formal (First_Formal (Formal))); - - Decl : Node_Id; - Expr : Node_Id; - F1, F2 : Entity_Id; - Func : Entity_Id; - Op_Name : Name_Id; - Spec : Node_Id; - L, R : Node_Id; - - begin - if No (Actual) then - Op_Name := Chars (Formal); - else - Op_Name := Chars (Actual); - end if; - - -- Create entities for wrapper function and its formals - - F1 := Make_Temporary (Loc, 'A'); - F2 := Make_Temporary (Loc, 'B'); - L := New_Occurrence_Of (F1, Loc); - R := New_Occurrence_Of (F2, Loc); - - Func := Make_Defining_Identifier (Loc, Chars (Formal)); - Set_Ekind (Func, E_Function); - Set_Is_Generic_Actual_Subprogram (Func); - - Spec := - Make_Function_Specification (Loc, - Defining_Unit_Name => Func, - Parameter_Specifications => New_List ( - Make_Parameter_Specification (Loc, - Defining_Identifier => F1, - Parameter_Type => - Make_Identifier (Loc, - Chars => Chars (Etype (First_Formal (Formal)))))), - Result_Definition => Make_Identifier (Loc, Chars (Typ))); - - if Is_Binary then - Append_To (Parameter_Specifications (Spec), - Make_Parameter_Specification (Loc, - Defining_Identifier => F2, - Parameter_Type => - Make_Identifier (Loc, - Chars (Etype (Next_Formal (First_Formal (Formal))))))); - end if; - - -- Build expression as a function call, or as an operator node - -- that corresponds to the name of the actual, starting with binary - -- operators. - - if Present (Actual) and then Op_Name not in Any_Operator_Name then - Expr := - Make_Function_Call (Loc, - Name => - New_Occurrence_Of (Entity (Actual), Loc), - Parameter_Associations => New_List (L)); - - if Is_Binary then - Append_To (Parameter_Associations (Expr), R); - end if; - - -- Binary operators - - elsif Is_Binary then - if Op_Name = Name_Op_And then - Expr := Make_Op_And (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Or then - Expr := Make_Op_Or (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Xor then - Expr := Make_Op_Xor (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Eq then - Expr := Make_Op_Eq (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Ne then - Expr := Make_Op_Ne (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Le then - Expr := Make_Op_Le (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Gt then - Expr := Make_Op_Gt (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Ge then - Expr := Make_Op_Ge (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Lt then - Expr := Make_Op_Lt (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Add then - Expr := Make_Op_Add (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Subtract then - Expr := Make_Op_Subtract (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Concat then - Expr := Make_Op_Concat (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Multiply then - Expr := Make_Op_Multiply (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Divide then - Expr := Make_Op_Divide (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Mod then - Expr := Make_Op_Mod (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Rem then - Expr := Make_Op_Rem (Loc, Left_Opnd => L, Right_Opnd => R); - elsif Op_Name = Name_Op_Expon then - Expr := Make_Op_Expon (Loc, Left_Opnd => L, Right_Opnd => R); - end if; - - -- Unary operators - - else - if Op_Name = Name_Op_Add then - Expr := Make_Op_Plus (Loc, Right_Opnd => L); - elsif Op_Name = Name_Op_Subtract then - Expr := Make_Op_Minus (Loc, Right_Opnd => L); - elsif Op_Name = Name_Op_Abs then - Expr := Make_Op_Abs (Loc, Right_Opnd => L); - elsif Op_Name = Name_Op_Not then - Expr := Make_Op_Not (Loc, Right_Opnd => L); - end if; - end if; - - -- Propagate visible entity to operator node, either from a - -- given actual or from a default. - - if Is_Entity_Name (Actual) and then Nkind (Expr) in N_Op then - Set_Entity (Expr, Entity (Actual)); - end if; - - Decl := - Make_Expression_Function (Loc, - Specification => Spec, - Expression => Expr); - - return Decl; - end Build_Operator_Wrapper; - ---------------------------------------- -- Check_Overloaded_Formal_Subprogram -- ---------------------------------------- @@ -1798,64 +1528,9 @@ package body Sem_Ch12 is end if; else - if GNATprove_Mode - and then Present - (Containing_Package_With_Ext_Axioms - (Defining_Entity (Analyzed_Formal))) - and then Ekind (Defining_Entity (Analyzed_Formal)) = - E_Function - and then Expander_Active - then - -- If actual is an entity (function or operator), - -- and expander is active, build wrapper for it. - -- Note that wrappers play no role within a generic. - - if Present (Match) then - if Nkind (Match) = N_Operator_Symbol then - - -- If the name is a default, find its visible - -- entity at the point of instantiation. - - if Is_Entity_Name (Match) - and then No (Entity (Match)) - then - Find_Direct_Name (Match); - end if; - - Append_To - (Assoc, - Build_Operator_Wrapper - (Defining_Entity (Analyzed_Formal), Match)); - - else - Append_To (Assoc, - Build_Function_Wrapper - (Defining_Entity (Analyzed_Formal), Match)); - end if; - - -- Ditto if formal is an operator with a default. - - elsif Box_Present (Formal) - and then Nkind (Defining_Entity (Analyzed_Formal)) = - N_Defining_Operator_Symbol - then - Append_To (Assoc, - Build_Operator_Wrapper - (Defining_Entity (Analyzed_Formal))); - - -- Otherwise create renaming declaration. - - else - Append_To (Assoc, - Build_Function_Wrapper - (Defining_Entity (Analyzed_Formal))); - end if; - - else - Append_To (Assoc, - Instantiate_Formal_Subprogram - (Formal, Match, Analyzed_Formal)); - end if; + Append_To (Assoc, + Instantiate_Formal_Subprogram + (Formal, Match, Analyzed_Formal)); -- An instantiation is a freeze point for the actuals, -- unless this is a rewritten formal package. @@ -5445,6 +5120,223 @@ package body Sem_Ch12 is end if; end Get_Associated_Node; + ---------------------------- + -- Build_Function_Wrapper -- + ---------------------------- + + function Build_Function_Wrapper + (Formal : Entity_Id; + Actual : Entity_Id) return Node_Id + is + Loc : constant Source_Ptr := Sloc (Formal); + Actuals : List_Id; + Decl : Node_Id; + Func_Name : Node_Id; + Func : Entity_Id; + Parm_Type : Node_Id; + Profile : List_Id := New_List; + Spec : Node_Id; + Act_F : Entity_Id; + Form_F : Entity_Id; + New_F : Entity_Id; + + begin + Func_Name := New_Occurrence_Of (Actual, Loc); + + Func := Make_Defining_Identifier (Loc, Chars (Formal)); + Set_Ekind (Func, E_Function); + Set_Is_Generic_Actual_Subprogram (Func); + + Actuals := New_List; + Profile := New_List; + + if Present (Actual) then + Act_F := First_Formal (Actual); + else + Act_F := Empty; + end if; + + Form_F := First_Formal (Formal); + while Present (Form_F) loop + + -- Create new formal for profile of wrapper, and add a reference + -- to it in the list of actuals for the enclosing call. The name + -- must be that of the formal in the formal subprogram, because + -- calls to it in the generic body may use named associations. + + New_F := Make_Defining_Identifier (Loc, Chars (Form_F)); + + Parm_Type := New_Occurrence_Of (Etype (Act_F), Loc); + + Append_To (Profile, + Make_Parameter_Specification (Loc, + Defining_Identifier => New_F, + Parameter_Type => Parm_Type)); + + Append_To (Actuals, New_Occurrence_Of (New_F, Loc)); + Next_Formal (Form_F); + + if Present (Act_F) then + Next_Formal (Act_F); + end if; + end loop; + + Spec := + Make_Function_Specification (Loc, + Defining_Unit_Name => Func, + Parameter_Specifications => Profile, + Result_Definition => + Make_Identifier (Loc, Chars (Etype (Formal)))); + + Decl := + Make_Expression_Function (Loc, + Specification => Spec, + Expression => + Make_Function_Call (Loc, + Name => Func_Name, + Parameter_Associations => Actuals)); + + return Decl; + end Build_Function_Wrapper; + + ---------------------------- + -- Build_Operator_Wrapper -- + ---------------------------- + + function Build_Operator_Wrapper + (Formal : Entity_Id; + Actual : Entity_Id) return Node_Id + is + Loc : constant Source_Ptr := Sloc (Formal); + Typ : constant Entity_Id := Etype (Formal); + Is_Binary : constant Boolean := + Present (Next_Formal (First_Formal (Formal))); + + Decl : Node_Id; + Expr : Node_Id; + F1, F2 : Entity_Id; + Func : Entity_Id; + Op_Name : Name_Id; + Spec : Node_Id; + L, R : Node_Id; + + begin + Op_Name := Chars (Actual); + + -- Create entities for wrapper function and its formals + + F1 := Make_Temporary (Loc, 'A'); + F2 := Make_Temporary (Loc, 'B'); + L := New_Occurrence_Of (F1, Loc); + R := New_Occurrence_Of (F2, Loc); + + Func := Make_Defining_Identifier (Loc, Chars (Formal)); + Set_Ekind (Func, E_Function); + Set_Is_Generic_Actual_Subprogram (Func); + + Spec := + Make_Function_Specification (Loc, + Defining_Unit_Name => Func, + Parameter_Specifications => New_List ( + Make_Parameter_Specification (Loc, + Defining_Identifier => F1, + Parameter_Type => + Make_Identifier (Loc, + Chars => Chars (Etype (First_Formal (Formal)))))), + Result_Definition => Make_Identifier (Loc, Chars (Typ))); + + if Is_Binary then + Append_To (Parameter_Specifications (Spec), + Make_Parameter_Specification (Loc, + Defining_Identifier => F2, + Parameter_Type => + Make_Identifier (Loc, + Chars (Etype (Next_Formal (First_Formal (Formal))))))); + end if; + + -- Build expression as a function call, or as an operator node + -- that corresponds to the name of the actual, starting with + -- binary operators. + + if Present (Actual) and then Op_Name not in Any_Operator_Name then + Expr := + Make_Function_Call (Loc, + Name => + New_Occurrence_Of (Entity (Actual), Loc), + Parameter_Associations => New_List (L)); + + if Is_Binary then + Append_To (Parameter_Associations (Expr), R); + end if; + + -- Binary operators + + elsif Is_Binary then + if Op_Name = Name_Op_And then + Expr := Make_Op_And (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Or then + Expr := Make_Op_Or (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Xor then + Expr := Make_Op_Xor (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Eq then + Expr := Make_Op_Eq (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Ne then + Expr := Make_Op_Ne (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Le then + Expr := Make_Op_Le (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Gt then + Expr := Make_Op_Gt (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Ge then + Expr := Make_Op_Ge (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Lt then + Expr := Make_Op_Lt (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Add then + Expr := Make_Op_Add (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Subtract then + Expr := Make_Op_Subtract (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Concat then + Expr := Make_Op_Concat (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Multiply then + Expr := Make_Op_Multiply (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Divide then + Expr := Make_Op_Divide (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Mod then + Expr := Make_Op_Mod (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Rem then + Expr := Make_Op_Rem (Loc, Left_Opnd => L, Right_Opnd => R); + elsif Op_Name = Name_Op_Expon then + Expr := Make_Op_Expon (Loc, Left_Opnd => L, Right_Opnd => R); + end if; + + -- Unary operators + + else + if Op_Name = Name_Op_Add then + Expr := Make_Op_Plus (Loc, Right_Opnd => L); + elsif Op_Name = Name_Op_Subtract then + Expr := Make_Op_Minus (Loc, Right_Opnd => L); + elsif Op_Name = Name_Op_Abs then + Expr := Make_Op_Abs (Loc, Right_Opnd => L); + elsif Op_Name = Name_Op_Not then + Expr := Make_Op_Not (Loc, Right_Opnd => L); + end if; + end if; + + -- Propagate visible entity to operator node, either from a + -- given actual or from a default. + + if Is_Entity_Name (Actual) and then Nkind (Expr) in N_Op then + Set_Entity (Expr, Entity (Actual)); + end if; + + Decl := + Make_Expression_Function (Loc, + Specification => Spec, + Expression => Expr); + + return Decl; + end Build_Operator_Wrapper; + ------------------------------------------- -- Build_Instance_Compilation_Unit_Nodes -- ------------------------------------------- diff --git a/gcc/ada/sem_ch12.ads b/gcc/ada/sem_ch12.ads index 450237b..c29a0a7 100644 --- a/gcc/ada/sem_ch12.ads +++ b/gcc/ada/sem_ch12.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -37,6 +37,22 @@ package Sem_Ch12 is procedure Analyze_Formal_Subprogram_Declaration (N : Node_Id); procedure Analyze_Formal_Package_Declaration (N : Node_Id); + function Build_Function_Wrapper + (Formal : Entity_Id; + Actual : Entity_Id) return Node_Id; + -- In GNATprove mode, create a wrapper function for actuals that are + -- functions with any number of formal parameters, in order to propagate + -- their contract to the renaming declarations generated for them. This + -- is called after the renaming declaration created for the formal in the + -- instance has been analyzed, and the actual is known. + + function Build_Operator_Wrapper + (Formal : Entity_Id; + Actual : Entity_Id) return Node_Id; + -- In GNATprove mode, create a wrapper function for actuals that are + -- operators, in order to propagate their contract to the renaming + -- declarations generated for them. + procedure Start_Generic; -- Must be invoked before starting to process a generic spec or body diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 8962079..5794209 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -9641,11 +9641,26 @@ package body Sem_Ch6 is -- in the formal part, because in a generic body the -- entity chain starts with the formals. - pragma Assert - (Present (Prev) or else Chars (E) = Name_Op_Concat); + -- In GNATprove mode, a wrapper for an operation with + -- axiomatization may be a homonym of another declaration + -- for an actual subprogram (needs refinement ???). + + if No (Prev) then + if In_Instance + and then GNATprove_Mode + and then + Nkind (Original_Node (Unit_Declaration_Node (S))) = + N_Subprogram_Renaming_Declaration + then + return; + else + pragma Assert (Chars (E) = Name_Op_Concat); + null; + end if; + end if; -- E must be removed both from the entity_list of the - -- current scope, and from the visibility chain + -- current scope, and from the visibility chain. if Debug_Flag_E then Write_Str ("Override implicit operation "); diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 4edeac9..cd008c1 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -3451,6 +3451,24 @@ package body Sem_Ch8 is Ada_Version := Save_AV; Ada_Version_Pragma := Save_AVP; Ada_Version_Explicit := Save_AV_Exp; + + -- In GNATprove mode, the renamings of actual subprograms are replaced + -- with wrapper functions that make it easier to propagate axioms to the + -- points of call within an instance. + + if Is_Actual + and then GNATprove_Mode + and then Present (Containing_Package_With_Ext_Axioms (Old_S)) + and then not Inside_A_Generic + then + if Ekind (Old_S) = E_Function then + Rewrite (N, Build_Function_Wrapper (New_S, Old_S)); + Analyze (N); + elsif Ekind (Old_S) = E_Operator then + Rewrite (N, Build_Operator_Wrapper (New_S, Old_S)); + Analyze (N); + end if; + end if; end Analyze_Subprogram_Renaming; ------------------------- -- 2.7.4