+2014-07-31 Arnaud Charlet <charlet@adacore.com>
+
+ * lib-writ.adb (Write_Unit_Information): Fix case where U =
+ No_Unit.
+
+2014-07-31 Claire Dross <dross@adacore.com>
+
+ * exp_util.adb, exp_util.ads
+ (Get_First_Parent_With_External_Axiomatization_For_Entity):
+ New routine to find the first parent of an entity with
+ a pragma Annotate (GNATprove, External_Axiomatization).
+ (Has_Annotate_Pragma_For_External_Axiomatization): New function
+ to check if a package has a pragma Annotate (GNATprove,
+ External_Axiomatization).
+ * einfo.ads, einfo.adb (Is_Generic_Actual_Subprogram): New
+ flag on the entity for the declaration created for a formal
+ subprogram in an instance. This is a renaming declaration,
+ or in GNATprove_Mode the declaration of an expression function
+ that captures the axiomatization of the actual.
+ * sem_ch6.adb (Analyze_Expression_Function): For a
+ Generic_Actual_Subprogram, place body immediately after the
+ declaration because it may be used in a subsequent declaration
+ in the instance.
+ * sem_ch12.adb (Build_Wrapper): Add code to handle instances where
+ the actual is a function, not an operator. Handle functions with
+ one and two parameters and binary and unary operators.
+
+2014-07-31 Pascal Obry <obry@adacore.com>
+
+ * cstreams.c (__gnat_is_regular_file_fd): Removed.
+ * adaint.c (__gnat_is_regular_file_fd): Added.
+
2014-07-31 Robert Dewar <dewar@adacore.com>
* exp_strm.adb: Minor reformatting.
return __gnat_is_regular_file_attr (name, &attr);
}
+int
+__gnat_is_regular_file_fd (int fd)
+{
+ int ret;
+ GNAT_STRUCT_STAT statbuf;
+
+ ret = GNAT_FSTAT (fd, &statbuf);
+ return (!ret && S_ISREG (statbuf.st_mode));
+}
+
int
__gnat_is_directory_attr (char* name, struct file_attributes* attr)
{
* *
* Auxiliary C functions for Interfaces.C.Streams *
* *
- * Copyright (C) 1992-2012, 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- *
return (fileno (stream));
}
-int
-__gnat_is_regular_file_fd (int fd)
-{
- int ret;
- GNAT_STRUCT_STAT statbuf;
-
- ret = GNAT_FSTAT (fd, &statbuf);
- return (!ret && S_ISREG (statbuf.st_mode));
-}
-
/* on some systems, the constants for seek are not defined, if so, then
provide the conventional definitions */
-- (SSO_Set_Low_By_Default) Flag272
-- (SSO_Set_Low_By_Default) Flag273
+ -- Is_Generic_Actual_Subprogram Flag274
+
-- (unused) Flag2
-- (unused) Flag3
- -- (unused) Flag274
-- (unused) Flag275
-- (unused) Flag276
-- (unused) Flag277
return Flag4 (Id);
end Is_Frozen;
+ function Is_Generic_Actual_Subprogram (Id : E) return B is
+ begin
+ pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure);
+ return Flag274 (Id);
+ end Is_Generic_Actual_Subprogram;
+
function Is_Generic_Actual_Type (Id : E) return B is
begin
pragma Assert (Is_Type (Id));
Set_Flag4 (Id, V);
end Set_Is_Frozen;
+ procedure Set_Is_Generic_Actual_Subprogram (Id : E; V : B := True) is
+ begin
+ pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure);
+ Set_Flag274 (Id, V);
+ end Set_Is_Generic_Actual_Subprogram;
+
procedure Set_Is_Generic_Actual_Type (Id : E; V : B := True) is
begin
pragma Assert (Is_Type (Id));
W ("Is_For_Access_Subtype", Flag118 (Id));
W ("Is_Formal_Subprogram", Flag111 (Id));
W ("Is_Frozen", Flag4 (Id));
+ W ("Is_Generic_Actual_Subprogram", Flag274 (Id));
W ("Is_Generic_Actual_Type", Flag94 (Id));
W ("Is_Generic_Instance", Flag130 (Id));
W ("Is_Generic_Type", Flag13 (Id));
-- Defined in all type and subtype entities. Set if type or subtype has
-- been frozen.
+-- Is_Generic_Actual_Subprogram (Flag274)
+-- Defined on functions and procedures. Set on the entity of the renaming
+-- declaration created within an instance for an actual subprogram.
+-- Used to generate constraint checks on calls to these subprograms, even
+-- within an instance of a predefined run-time unit, in which checks
+-- are otherwise suppressed.
+--
+-- The flag is also set on the entity of the expression function created
+-- within an instance, for a function that has external axiomatization,
+-- for use in GNATprove mode.
+
-- Is_Generic_Actual_Type (Flag94)
-- Defined in all type and subtype entities. Set in the subtype
-- declaration that renames the generic formal as a subtype of the
-- Is_Discrim_SO_Function (Flag176)
-- Is_Discriminant_Check_Function (Flag264)
-- Is_Eliminated (Flag124)
+ -- Is_Generic_Actual_Subprogram (Flag274) (non-generic case only)
-- Is_Inlined_Always (Flag1) (non-generic case only)
-- Is_Instantiated (Flag126) (generic case only)
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Eliminated (Flag124)
-- Is_Inlined_Always (Flag1) (non-generic case only)
-- Is_Instantiated (Flag126) (generic case only)
+ -- Is_Generic_Actual_Subprogram (Flag274) (non-generic case only)
-- Is_Interrupt_Handler (Flag89)
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Invariant_Procedure (Flag257) (non-generic case only)
function Is_Formal (Id : E) return B;
function Is_Formal_Object (Id : E) return B;
function Is_Formal_Subprogram (Id : E) return B;
+ function Is_Generic_Actual_Subprogram (Id : E) return B;
function Is_Generic_Actual_Type (Id : E) return B;
function Is_Generic_Unit (Id : E) return B;
function Is_Generic_Type (Id : E) return B;
procedure Set_Is_For_Access_Subtype (Id : E; V : B := True);
procedure Set_Is_Formal_Subprogram (Id : E; V : B := True);
procedure Set_Is_Frozen (Id : E; V : B := True);
+ procedure Set_Is_Generic_Actual_Subprogram (Id : E; V : B := True);
procedure Set_Is_Generic_Actual_Type (Id : E; V : B := True);
procedure Set_Is_Generic_Instance (Id : E; V : B := True);
procedure Set_Is_Generic_Type (Id : E; V : B := True);
pragma Inline (Is_Formal_Object);
pragma Inline (Is_Formal_Subprogram);
pragma Inline (Is_Frozen);
+ pragma Inline (Is_Generic_Actual_Subprogram);
pragma Inline (Is_Generic_Actual_Type);
pragma Inline (Is_Generic_Instance);
pragma Inline (Is_Generic_Subprogram);
pragma Inline (Set_Is_For_Access_Subtype);
pragma Inline (Set_Is_Formal_Subprogram);
pragma Inline (Set_Is_Frozen);
+ pragma Inline (Set_Is_Generic_Actual_Subprogram);
pragma Inline (Set_Is_Generic_Actual_Type);
pragma Inline (Set_Is_Generic_Instance);
pragma Inline (Set_Is_Generic_Type);
end;
end Get_Current_Value_Condition;
+ --------------------------------------------------------------
+ -- Get_First_Parent_With_External_Axiomatization_For_Entity --
+ --------------------------------------------------------------
+
+ function Get_First_Parent_With_External_Axiomatization_For_Entity
+ (E : Entity_Id) return Entity_Id is
+
+ Decl : Node_Id;
+
+ begin
+ if Ekind (E) = E_Package then
+ if Nkind (Parent (E)) = N_Defining_Program_Unit_Name then
+ Decl := Parent (Parent (E));
+ else
+ Decl := Parent (E);
+ end if;
+ end if;
+
+ -- E is the package which is externally axiomatized
+
+ if Ekind (E) = E_Package
+ and then Has_Annotate_Pragma_For_External_Axiomatization (E)
+ then
+ return E;
+
+ -- E is a package instance, in which case it is axiomatized iff the
+ -- corresponding generic package is Axiomatized.
+
+ elsif Ekind (E) = E_Package
+ and then Present (Generic_Parent (Decl))
+ then
+ return Get_First_Parent_With_External_Axiomatization_For_Entity
+ (Generic_Parent (Decl));
+
+ -- Otherwise, look at E's scope instead if present
+
+ elsif Present (Scope (E)) then
+ return Get_First_Parent_With_External_Axiomatization_For_Entity
+ (Scope (E));
+
+ -- Else there is no such axiomatized package
+
+ else
+ return Empty;
+ end if;
+ end Get_First_Parent_With_External_Axiomatization_For_Entity;
+
---------------------
-- Get_Stream_Size --
---------------------
end if;
end Has_Access_Constraint;
+ -----------------------------------------------------
+ -- Has_Annotate_Pragma_For_External_Axiomatization --
+ -----------------------------------------------------
+
+ function Has_Annotate_Pragma_For_External_Axiomatization
+ (E : Entity_Id) return Boolean
+ is
+
+ function Is_Annotate_Pragma_For_External_Axiomatization
+ (N : Node_Id) return Boolean;
+ -- Returns whether N is
+ -- pragma Annotate (GNATprove, External_Axiomatization);
+
+ ----------------------------------------------------
+ -- Is_Annotate_Pragma_For_External_Axiomatization --
+ ----------------------------------------------------
+
+ -- The general form of pragma Annotate is
+
+ -- pragma Annotate (IDENTIFIER [, IDENTIFIER {, ARG}]);
+ -- ARG ::= NAME | EXPRESSION
+
+ -- The first two arguments are by convention intended to refer to an
+ -- external tool and a tool-specific function. These arguments are
+ -- not analyzed.
+
+ -- The following is used to annotate a package specification which
+ -- GNATprove should treat specially, because the axiomatization of
+ -- this unit is given by the user instead of being automatically
+ -- generated.
+
+ -- pragma Annotate (GNATprove, External_Axiomatization);
+
+ function Is_Annotate_Pragma_For_External_Axiomatization
+ (N : Node_Id) return Boolean is
+
+ -------------------
+ -- Special Names --
+ -------------------
+
+ Name_GNATprove : constant String := "gnatprove";
+ Name_External_Axiomatization : constant String :=
+ "external_axiomatization";
+ begin
+ if Nkind (N) = N_Pragma
+ and then Get_Pragma_Id (Pragma_Name (N)) = Pragma_Annotate
+ and then List_Length (Pragma_Argument_Associations (N)) = 2
+ then
+ declare
+ Arg1 : constant Node_Id :=
+ First (Pragma_Argument_Associations (N));
+ Arg2 : constant Node_Id := Next (Arg1);
+ Nam1 : Name_Id;
+ Nam2 : Name_Id;
+ begin
+ -- Fill in Name_Buffer with Name_GNATprove first, and then with
+ -- Name_External_Axiomatization so that Name_Find returns the
+ -- corresponding name. This takes care of all possible casings.
+
+ Name_Len := 0;
+ Add_Str_To_Name_Buffer (Name_GNATprove);
+ Nam1 := Name_Find;
+
+ Name_Len := 0;
+ Add_Str_To_Name_Buffer (Name_External_Axiomatization);
+ Nam2 := Name_Find;
+
+ return Chars (Get_Pragma_Arg (Arg1)) = Nam1
+ and then
+ Chars (Get_Pragma_Arg (Arg2)) = Nam2;
+ end;
+
+ else
+ return False;
+ end if;
+ end Is_Annotate_Pragma_For_External_Axiomatization;
+
+ Decl : Node_Id;
+ Vis_Decls : List_Id;
+ N : Node_Id;
+
+ begin
+ if Nkind (Parent (E)) = N_Defining_Program_Unit_Name then
+ Decl := Parent (Parent (E));
+ else
+ Decl := Parent (E);
+ end if;
+
+ Vis_Decls := Visible_Declarations (Decl);
+
+ N := First (Vis_Decls);
+ while Present (N) loop
+
+ -- Skip declarations generated by the frontend. Skip all pragmas
+ -- that are not the desired Annotate pragma. Stop the search on
+ -- the first non-pragma source declaration.
+
+ if Comes_From_Source (N) then
+ if Nkind (N) = N_Pragma then
+ if Is_Annotate_Pragma_For_External_Axiomatization (N) then
+ return True;
+ end if;
+ else
+ return False;
+ end if;
+ end if;
+
+ Next (N);
+ end loop;
+
+ return False;
+ end Has_Annotate_Pragma_For_External_Axiomatization;
+
----------------------------------
-- Has_Following_Address_Clause --
----------------------------------
-- N_Op_Eq), or to determine the result of some other test in other cases
-- (e.g. no access check required if N_Op_Ne Null).
+ function Get_First_Parent_With_External_Axiomatization_For_Entity
+ (E : Entity_Id) return Entity_Id;
+ -- Returns the package entity with an external axiomatization containing E,
+ -- if any, or Empty if none.
+
function Get_Stream_Size (E : Entity_Id) return Uint;
-- Return the stream size value of the subtype E
function Has_Access_Constraint (E : Entity_Id) return Boolean;
-- Given object or type E, determine if a discriminant is of an access type
+ function Has_Annotate_Pragma_For_External_Axiomatization
+ (E : Entity_Id) return Boolean;
+ -- Returns whether E is a package entity, for which the initial list of
+ -- pragmas at the start of the package declaration contains
+ -- pragma Annotate (GNATprove, External_Axiomatization);
+
function Has_Following_Address_Clause (D : Node_Id) return Boolean;
-- D is the node for an object declaration. This function searches the
-- current declarative part to look for an address clause for the object
-- compilation unit.
begin
- if Nkind (Unit (Cunit (U))) = N_Subunit then
+ if U /= No_Unit
+ and then Nkind (Unit (Cunit (U))) = N_Subunit
+ then
Note_Unit := Main_Unit;
else
Note_Unit := U;
-- In Ada 2005, indicates partial parameterization of a formal
-- package. As usual an other association must be last in the list.
- function Build_Wrapper (Formal : Entity_Id) return Node_Id;
+ function Build_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.
+ -- 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
-- Build_Wrapper --
-------------------
- function Build_Wrapper (Formal : Entity_Id) return Node_Id is
+ function Build_Wrapper
+ (Formal : Entity_Id;
+ Actual : Entity_Id := Empty) return Node_Id
+ is
Loc : constant Source_Ptr := Sloc (I_Node);
- Op_Name : constant Name_Id := Chars (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
+ 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');
L := New_Occurrence_Of (F1, Loc);
R := New_Occurrence_Of (F2, Loc);
- Func := Make_Temporary (Loc, 'F');
+ 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,
+ Defining_Unit_Name => Func,
Parameter_Specifications => New_List (
Make_Parameter_Specification (Loc,
Defining_Identifier => F1,
- Parameter_Type => Make_Identifier (Loc, Chars (Typ))),
- Make_Parameter_Specification (Loc,
- Defining_Identifier => F2,
- Parameter_Type => Make_Identifier (Loc, Chars (Typ)))),
+ Parameter_Type => Make_Identifier
+ (Loc, Chars (Etype (First_Formal (Formal)))))),
Result_Definition => Make_Identifier (Loc, Chars (Typ)));
- -- Build expression as an operator node that corresponds to the
- -- name of the actual, starting with binary operators.
+ 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;
- if Op_Name = Name_Op_And then
- Expr := Make_Op_And (Loc, Left_Opnd => L, Right_Opnd => R);
+ -- Build expression as a function call, or as an operator node
+ -- that corresponds to the name of the actual, starting with binary
+ -- operators.
- elsif Op_Name = Name_Op_Or then
- Expr := Make_Op_Or (Loc, Left_Opnd => L, Right_Opnd => R);
+ 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));
- elsif Op_Name = Name_Op_Xor then
- Expr := Make_Op_Xor (Loc, Left_Opnd => L, Right_Opnd => R);
+ if Is_Binary then
+ Append_To (Parameter_Associations (Expr), R);
+ end if;
- elsif Op_Name = Name_Op_Eq then
- Expr := Make_Op_Eq (Loc, Left_Opnd => L, Right_Opnd => R);
+ 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_Ne then
- Expr := Make_Op_Ne (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_Le then
- Expr := Make_Op_Le (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_Gt then
- Expr := Make_Op_Gt (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_Ge then
- Expr := Make_Op_Ge (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_Lt then
- Expr := Make_Op_Lt (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_Add then
- Expr := Make_Op_Add (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_Subtract then
- Expr := Make_Op_Subtract (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_Concat then
- Expr := Make_Op_Concat (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_Multiply then
- Expr := Make_Op_Multiply (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_Divide then
- Expr := Make_Op_Divide (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_Mod then
- Expr := Make_Op_Mod (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_Rem then
- Expr := Make_Op_Rem (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_Expon then
- Expr := Make_Op_Expon (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);
- -- Unary operators.
+ elsif Op_Name = Name_Op_Mod then
+ Expr := Make_Op_Mod (Loc, Left_Opnd => L, Right_Opnd => R);
- elsif Op_Name = Name_Op_Add
- and then No (Next_Formal (First_Formal (Actual)))
- then
- Expr := Make_Op_Plus (Loc, 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_Subtract
- and then No (Next_Formal (First_Formal (Actual)))
- then
- Expr := Make_Op_Minus (Loc, Right_Opnd => R);
+ elsif Op_Name = Name_Op_Expon then
+ Expr := Make_Op_Expon (Loc, Left_Opnd => L, Right_Opnd => R);
+ end if;
+
+ else -- Unary operators.
+
+ if Op_Name = Name_Op_Add then
+ Expr := Make_Op_Plus (Loc, Right_Opnd => L);
- elsif Op_Name = Name_Op_Abs then
- Expr := Make_Op_Abs (Loc, Right_Opnd => R);
+ elsif Op_Name = Name_Op_Subtract then
+ Expr := Make_Op_Minus (Loc, Right_Opnd => L);
- elsif Op_Name = Name_Op_Not then
- Expr := Make_Op_Not (Loc, Right_Opnd => R);
+ 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,
end if;
else
- Append_To (Assoc,
- Instantiate_Formal_Subprogram
- (Formal, Match, Analyzed_Formal));
+ if GNATprove_Mode
+ and then Ekind (Defining_Entity (Analyzed_Formal))
+ = E_Function
+ then
+
+ -- If actual is an entity (function or operator),
+ -- build wrapper for it.
- if GNATprove_Mode then
- if Nkind (Match) = N_Operator_Symbol then
+ if Present (Match) and then Is_Entity_Name (Match) then
Append_To (Assoc,
Build_Wrapper
- (Defining_Entity (Analyzed_Formal)));
+ (Defining_Entity (Analyzed_Formal), Match));
+
+ -- 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_Wrapper
(Defining_Entity (Analyzed_Formal)));
+
+ -- Otherwise create renaming declaration.
+
+ else
+ Append_To (Assoc,
+ Instantiate_Formal_Subprogram
+ (Formal, Match, Analyzed_Formal));
end if;
+
+ else
+ Append_To (Assoc,
+ Instantiate_Formal_Subprogram
+ (Formal, Match, Analyzed_Formal));
end if;
-- An instantiation is a freeze point for the actuals,
Id : constant Entity_Id := Defining_Entity (N);
begin
- if Nkind (Par) = N_Package_Specification
- and then Decls = Visible_Declarations (Par)
- and then Present (Private_Declarations (Par))
- and then not Is_Empty_List (Private_Declarations (Par))
+ -- If this is a wrapper created for in an instance for a formal
+ -- subprogram, insert body after declaration, to be analyzed when
+ -- the enclosing instance is analyzed.
+
+ if GNATprove_Mode
+ and then Is_Generic_Actual_Subprogram (Defining_Entity (N))
then
- Decls := Private_Declarations (Par);
- end if;
+ Insert_After (N, New_Body);
- Insert_After (Last (Decls), New_Body);
- Push_Scope (Id);
- Install_Formals (Id);
+ else
+ if Nkind (Par) = N_Package_Specification
+ and then Decls = Visible_Declarations (Par)
+ and then Present (Private_Declarations (Par))
+ and then not Is_Empty_List (Private_Declarations (Par))
+ then
+ Decls := Private_Declarations (Par);
+ end if;
- -- Preanalyze the expression for name capture, except in an
- -- instance, where this has been done during generic analysis,
- -- and will be redone when analyzing the body.
+ Insert_After (Last (Decls), New_Body);
+ Push_Scope (Id);
+ Install_Formals (Id);
- declare
- Expr : constant Node_Id := Expression (Ret);
+ -- Preanalyze the expression for name capture, except in an
+ -- instance, where this has been done during generic analysis,
+ -- and will be redone when analyzing the body.
- begin
- Set_Parent (Expr, Ret);
+ declare
+ Expr : constant Node_Id := Expression (Ret);
- if not In_Instance then
- Preanalyze_Spec_Expression (Expr, Etype (Id));
- end if;
- end;
+ begin
+ Set_Parent (Expr, Ret);
- End_Scope;
+ if not In_Instance then
+ Preanalyze_Spec_Expression (Expr, Etype (Id));
+ end if;
+ end;
+
+ End_Scope;
+ end if;
end;
end if;
projects / thirdparty / gcc.git / commitdiff
