Support for external axiomatization in GNATprove has been deconstructed
few years ago, so the related frontend code can be deconstructed too.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_ch12.ads (Build_Function_Wrapper, Build_Operator_Wrapper):
Remove unreferenced spec.
* sem_ch12.adb (Build_Function_Wrapper, Build_Operator_Wrapper):
Remove dead bodies.diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -6080,211 +6080,6 @@ package body Sem_Ch12 is
end if;
end Get_Associated_Node;
- ----------------------------
- -- Build_Function_Wrapper --
- ----------------------------
-
- function Build_Function_Wrapper
- (Formal_Subp : Entity_Id;
- Actual_Subp : Entity_Id) return Node_Id
- is
- Loc : constant Source_Ptr := Sloc (Current_Scope);
- Ret_Type : constant Entity_Id := Get_Instance_Of (Etype (Formal_Subp));
- 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_Subp, Loc);
-
- Func := Make_Defining_Identifier (Loc, Chars (Formal_Subp));
- Mutate_Ekind (Func, E_Function);
- Set_Is_Generic_Actual_Subprogram (Func);
-
- Actuals := New_List;
- Profile := New_List;
-
- Act_F := First_Formal (Actual_Subp);
- Form_F := First_Formal (Formal_Subp);
- 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 (Get_Instance_Of (Etype (Form_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 => New_Occurrence_Of (Ret_Type, Loc));
-
- 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_Subp : Entity_Id;
- Actual_Subp : Entity_Id) return Node_Id
- is
- Loc : constant Source_Ptr := Sloc (Current_Scope);
- Ret_Type : constant Entity_Id :=
- Get_Instance_Of (Etype (Formal_Subp));
- Op_Type : constant Entity_Id :=
- Get_Instance_Of (Etype (First_Formal (Formal_Subp)));
- Is_Binary : constant Boolean :=
- Present (Next_Formal (First_Formal (Formal_Subp)));
-
- Decl : Node_Id;
- Expr : Node_Id := Empty;
- F1, F2 : Entity_Id;
- Func : Entity_Id;
- Op_Name : Name_Id;
- Spec : Node_Id;
- L, R : Node_Id;
-
- begin
- Op_Name := Chars (Actual_Subp);
-
- -- 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_Subp));
- Mutate_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 => New_Occurrence_Of (Op_Type, Loc))),
- Result_Definition => New_Occurrence_Of (Ret_Type, Loc));
-
- if Is_Binary then
- Append_To (Parameter_Specifications (Spec),
- Make_Parameter_Specification (Loc,
- Defining_Identifier => F2,
- Parameter_Type => New_Occurrence_Of (Op_Type, Loc)));
- 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 Op_Name not in Any_Operator_Name then
- Expr :=
- Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of (Actual_Subp, 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;
-
- Decl :=
- Make_Expression_Function (Loc,
- Specification => Spec,
- Expression => Expr);
-
- return Decl;
- end Build_Operator_Wrapper;
-
-----------------------------------
-- Build_Subprogram_Decl_Wrapper --
-----------------------------------
diff --git a/gcc/ada/sem_ch12.ads b/gcc/ada/sem_ch12.ads
--- a/gcc/ada/sem_ch12.ads
+++ b/gcc/ada/sem_ch12.ads
@@ -37,23 +37,6 @@ 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_Subp : Entity_Id;
- Actual_Subp : 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_Subp : Entity_Id;
- Actual_Subp : 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. The types are (the instances of)
- -- the types of the formal subprogram.
-
procedure Start_Generic;
-- Must be invoked before starting to process a generic spec or body
