end if;
end Component_May_Be_Bit_Aligned;
- ----------------------------------------
- -- Containing_Package_With_Ext_Axioms --
- ----------------------------------------
-
- function Containing_Package_With_Ext_Axioms
- (E : Entity_Id) return Entity_Id
- is
- begin
- -- E is the package or generic package which is externally axiomatized
-
- if Is_Package_Or_Generic_Package (E)
- and then Has_Annotate_Pragma_For_External_Axiomatization (E)
- then
- return E;
- end if;
-
- -- If E's scope is axiomatized, E is axiomatized
-
- if Present (Scope (E)) then
- declare
- First_Ax_Parent_Scope : constant Entity_Id :=
- Containing_Package_With_Ext_Axioms (Scope (E));
- begin
- if Present (First_Ax_Parent_Scope) then
- return First_Ax_Parent_Scope;
- end if;
- end;
- end if;
-
- -- Otherwise, if E is a package instance, it is axiomatized if the
- -- corresponding generic package is axiomatized.
-
- if Ekind (E) = E_Package then
- declare
- Par : constant Node_Id := Parent (E);
- Decl : Node_Id;
-
- begin
- if Nkind (Par) = N_Defining_Program_Unit_Name then
- Decl := Parent (Par);
- else
- Decl := Par;
- end if;
-
- if Present (Generic_Parent (Decl)) then
- return
- Containing_Package_With_Ext_Axioms (Generic_Parent (Decl));
- end if;
- end;
- end if;
-
- return Empty;
- end Containing_Package_With_Ext_Axioms;
-
-------------------------------
-- Convert_To_Actual_Subtype --
-------------------------------
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
- Name_GNATprove : constant String :=
- "gnatprove";
- Name_External_Axiomatization : constant String :=
- "external_axiomatization";
- -- Special names
-
- begin
- if Nkind (N) = N_Pragma
- and then Get_Pragma_Id (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;
-
- -- Local variables
-
- Decl : Node_Id;
- Vis_Decls : List_Id;
- N : Node_Id;
-
- -- Start of processing for Has_Annotate_Pragma_For_External_Axiomatization
-
- 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;
-
--------------------
-- Homonym_Number --
--------------------
-- for trouble using this function and, if so, the assignment is expanded
-- component-wise, which the back end is required to handle correctly.
- function Containing_Package_With_Ext_Axioms
- (E : Entity_Id) return Entity_Id;
- -- Returns the package entity with an external axiomatization containing E,
- -- if any, or Empty if none.
-
procedure Convert_To_Actual_Subtype (Exp : Node_Id);
-- The Etype of an expression is the nominal type of the expression,
-- not the actual subtype. Often these are the same, but not always.
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 Homonym_Number (Subp : Entity_Id) return Pos;
-- Here subp is the entity for a subprogram. This routine returns the
-- homonym number used to disambiguate overloaded subprograms in the same
-- Check whether the renaming is for a defaulted actual subprogram
-- with a class-wide actual.
- -- The class-wide wrapper is not needed in GNATprove_Mode and there
- -- is an external axiomatization on the package.
-
- if CW_Actual
- and then Box_Present (Inst_Node)
- and then not
- (GNATprove_Mode
- and then
- Present (Containing_Package_With_Ext_Axioms (Formal_Spec)))
- then
+ if CW_Actual and then Box_Present (Inst_Node) then
Build_Class_Wide_Wrapper (New_S, Old_S);
elsif Is_Entity_Name (Nam)
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. Wrappers are generated if formal
- -- subprogram is subject to axiomatization.
-
- -- The types in the wrapper profiles are obtained from (instances of)
- -- the types of the formal subprogram.
-
- if Is_Actual
- and then GNATprove_Mode
- and then Present (Containing_Package_With_Ext_Axioms (Formal_Spec))
- and then not Inside_A_Generic
- then
- if Ekind (Old_S) = E_Function then
- Rewrite (N, Build_Function_Wrapper (Formal_Spec, Old_S));
- Analyze (N);
-
- elsif Ekind (Old_S) = E_Operator then
- Rewrite (N, Build_Operator_Wrapper (Formal_Spec, Old_S));
- Analyze (N);
- end if;
- end if;
-
-- Check if we are looking at an Ada 2012 defaulted formal subprogram
-- and mark any use_package_clauses that affect the visibility of the
-- implicit generic actual.
projects / gcc.git / commitdiff