-- --
-- B o d y --
-- --
--- 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- --
-- --
------------------------------------------------------------------------------
+with Aspects; use Aspects;
with Atree; use Atree;
with Checks; use Checks;
with Debug; use Debug;
-- must appear before the type is frozen, and have the same visibility as
-- that of the type. This procedure checks that this rule is met, and
-- otherwise emits an error on the subprogram declaration and a warning
- -- on the earlier freeze point if it is easy to locate.
+ -- on the earlier freeze point if it is easy to locate. In Ada 2012 mode,
+ -- this routine outputs errors (or warnings if -gnatd.E is set). In earlier
+ -- versions of Ada, warnings are output if Warn_On_Ada_2012_Incompatibility
+ -- is set, otherwise the call has no effect.
procedure Enter_Overloaded_Entity (S : Entity_Id);
-- This procedure makes S, a new overloaded entity, into the first visible
-- Create the declaration for an inequality operator that is implicitly
-- created by a user-defined equality operator that yields a boolean.
- procedure May_Need_Actuals (Fun : Entity_Id);
- -- Flag functions that can be called without parameters, i.e. those that
- -- have no parameters, or those for which defaults exist for all parameters
-
- procedure Process_PPCs
- (N : Node_Id;
- Spec_Id : Entity_Id;
- Body_Id : Entity_Id);
- -- Called from Analyze[_Generic]_Subprogram_Body to deal with scanning post
- -- conditions for the body and assembling and inserting the _postconditions
- -- procedure. N is the node for the subprogram body and Body_Id/Spec_Id are
- -- the entities for the body and separate spec (if there is no separate
- -- spec, Spec_Id is Empty). Note that invariants and predicates may also
- -- provide postconditions, and are also handled in this procedure.
-
procedure Set_Formal_Validity (Formal_Id : Entity_Id);
-- Formal_Id is an formal parameter entity. This procedure deals with
-- setting the proper validity status for this entity, which depends on
if Present (Parameter_Specifications (New_Spec)) then
declare
Formal_Spec : Node_Id;
+ Def : Entity_Id;
+
begin
Formal_Spec := First (Parameter_Specifications (New_Spec));
+
+ -- Create a new formal parameter at the same source position
+
while Present (Formal_Spec) loop
- Set_Defining_Identifier
- (Formal_Spec,
- Make_Defining_Identifier (Sloc (Formal_Spec),
- Chars => Chars (Defining_Identifier (Formal_Spec))));
+ Def := Defining_Identifier (Formal_Spec);
+ Set_Defining_Identifier (Formal_Spec,
+ Make_Defining_Identifier (Sloc (Def),
+ Chars => Chars (Def)));
Next (Formal_Spec);
end loop;
end;
end if;
- Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
+ Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
-- If there are previous overloadable entities with the same name,
-- check whether any of them is completed by the expression function.
if Present (Prev) and then Is_Overloadable (Prev) then
- Def_Id := Analyze_Subprogram_Specification (Spec);
- Prev := Find_Corresponding_Spec (N);
+ Def_Id := Analyze_Subprogram_Specification (Spec);
+ Prev := Find_Corresponding_Spec (N);
end if;
Ret := Make_Simple_Return_Statement (LocX, Expression (N));
Make_Handled_Sequence_Of_Statements (LocX,
Statements => New_List (Ret)));
+ -- If the expression completes a generic subprogram, we must create a
+ -- separate node for the body, because at instantiation the original
+ -- node of the generic copy must be a generic subprogram body, and
+ -- cannot be a expression function. Otherwise we just rewrite the
+ -- expression with the non-generic body.
+
if Present (Prev) and then Ekind (Prev) = E_Generic_Function then
+ Insert_After (N, New_Body);
- -- If the expression completes a generic subprogram, we must create a
- -- separate node for the body, because at instantiation the original
- -- node of the generic copy must be a generic subprogram body, and
- -- cannot be a expression function. Otherwise we just rewrite the
- -- expression with the non-generic body.
+ -- Propagate any aspects or pragmas that apply to the expression
+ -- function to the proper body when the expression function acts
+ -- as a completion.
+
+ if Has_Aspects (N) then
+ Move_Aspects (N, To => New_Body);
+ end if;
+
+ Relocate_Pragmas_To_Body (New_Body);
- Insert_After (N, New_Body);
Rewrite (N, Make_Null_Statement (Loc));
Set_Has_Completion (Prev, False);
Analyze (N);
elsif Present (Prev) and then Comes_From_Source (Prev) then
Set_Has_Completion (Prev, False);
+ -- An expression function that is a completion freezes the
+ -- expression. This means freezing the return type, and if it is
+ -- an access type, freezing its designated type as well.
+
+ -- Note that we cannot defer this freezing to the analysis of the
+ -- expression itself, because a freeze node might appear in a nested
+ -- scope, leading to an elaboration order issue in gigi.
+
+ Freeze_Before (N, Etype (Prev));
+
+ if Is_Access_Type (Etype (Prev)) then
+ Freeze_Before (N, Designated_Type (Etype (Prev)));
+ end if;
+
-- For navigation purposes, indicate that the function is a body
Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True);
Rewrite (N, New_Body);
+
+ -- Correct the parent pointer of the aspect specification list to
+ -- reference the rewritten node.
+
+ if Has_Aspects (N) then
+ Set_Parent (Aspect_Specifications (N), N);
+ end if;
+
+ -- Propagate any pragmas that apply to the expression function to the
+ -- proper body when the expression function acts as a completion.
+ -- Aspects are automatically transfered because of node rewriting.
+
+ Relocate_Pragmas_To_Body (N);
Analyze (N);
-- Prev is the previous entity with the same name, but it is can
Make_Subprogram_Declaration (Loc, Specification => Spec);
Rewrite (N, New_Decl);
+
+ -- Correct the parent pointer of the aspect specification list to
+ -- reference the rewritten node.
+
+ if Has_Aspects (N) then
+ Set_Parent (Aspect_Specifications (N), N);
+ end if;
+
Analyze (N);
Set_Is_Inlined (Defining_Entity (New_Decl));
-- To prevent premature freeze action, insert the new body at the end
-- of the current declarations, or at the end of the package spec.
-- However, resolve usage names now, to prevent spurious visibility
- -- on later entities.
+ -- on later entities. Note that the function can now be called in
+ -- the current declarative part, which will appear to be prior to
+ -- the presence of the body in the code. There are nevertheless no
+ -- order of elaboration issues because all name resolution has taken
+ -- place at the point of declaration.
declare
Decls : List_Id := List_Containing (N);
Push_Scope (Id);
Install_Formals (Id);
- -- Do a preanalysis of the expression on a separate copy, to
- -- prevent visibility issues later with operators in instances.
- -- Attach copy to tree so that parent links are available.
+ -- 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.
declare
- Expr : constant Node_Id := New_Copy_Tree (Expression (Ret));
+ Expr : constant Node_Id := Expression (Ret);
+
begin
Set_Parent (Expr, Ret);
- Preanalyze_Spec_Expression (Expr, Etype (Id));
+
+ if not In_Instance then
+ Preanalyze_Spec_Expression (Expr, Etype (Id));
+ end if;
end;
End_Scope;
procedure Analyze_Extended_Return_Statement (N : Node_Id) is
begin
+ Check_Compiler_Unit ("extended return statement", N);
Analyze_Return_Statement (N);
end Analyze_Extended_Return_Statement;
("(Ada 2005) cannot copy object of a limited type " &
"(RM-2005 6.5(5.5/2))", Expr);
- if Is_Immutably_Limited_Type (R_Type) then
+ if Is_Limited_View (R_Type) then
Error_Msg_N
("\return by reference not permitted in Ada 2005", Expr);
end if;
("return of limited object not permitted in Ada 2005 "
& "(RM-2005 6.5(5.5/2))?y?", Expr);
- elsif Is_Immutably_Limited_Type (R_Type) then
+ elsif Is_Limited_View (R_Type) then
Error_Msg_N
("return by reference not permitted in Ada 2005 "
& "(RM-2005 6.5(5.5/2))?y?", Expr);
Subtype_Ind : constant Node_Id :=
Object_Definition (Original_Node (Obj_Decl));
- R_Type_Is_Anon_Access :
- constant Boolean :=
- Ekind (R_Type) = E_Anonymous_Access_Subprogram_Type
- or else
- Ekind (R_Type) = E_Anonymous_Access_Protected_Subprogram_Type
- or else
- Ekind (R_Type) = E_Anonymous_Access_Type;
+ R_Type_Is_Anon_Access : constant Boolean :=
+ Ekind_In (R_Type,
+ E_Anonymous_Access_Subprogram_Type,
+ E_Anonymous_Access_Protected_Subprogram_Type,
+ E_Anonymous_Access_Type);
-- True if return type of the function is an anonymous access type
-- Can't we make Is_Anonymous_Access_Type in einfo ???
- R_Stm_Type_Is_Anon_Access :
- constant Boolean :=
- Ekind (R_Stm_Type) = E_Anonymous_Access_Subprogram_Type
- or else
- Ekind (R_Stm_Type) = E_Anonymous_Access_Protected_Subprogram_Type
- or else
- Ekind (R_Stm_Type) = E_Anonymous_Access_Type;
+ R_Stm_Type_Is_Anon_Access : constant Boolean :=
+ Ekind_In (R_Stm_Type,
+ E_Anonymous_Access_Subprogram_Type,
+ E_Anonymous_Access_Protected_Subprogram_Type,
+ E_Anonymous_Access_Type);
-- True if type of the return object is an anonymous access type
+ procedure Error_No_Match (N : Node_Id);
+ -- Output error messages for case where types do not statically
+ -- match. N is the location for the messages.
+
+ --------------------
+ -- Error_No_Match --
+ --------------------
+
+ procedure Error_No_Match (N : Node_Id) is
+ begin
+ Error_Msg_N
+ ("subtype must statically match function result subtype", N);
+
+ if not Predicates_Match (R_Stm_Type, R_Type) then
+ Error_Msg_Node_2 := R_Type;
+ Error_Msg_NE
+ ("\predicate of & does not match predicate of &",
+ N, R_Stm_Type);
+ end if;
+ end Error_No_Match;
+
+ -- Start of processing for Check_Return_Subtype_Indication
+
begin
-- First, avoid cascaded errors
Base_Type (Designated_Type (R_Type))
or else not Subtypes_Statically_Match (R_Stm_Type, R_Type)
then
- Error_Msg_N
- ("subtype must statically match function result subtype",
- Subtype_Mark (Subtype_Ind));
+ Error_No_Match (Subtype_Mark (Subtype_Ind));
end if;
else
if not Conforming_Types
(R_Stm_Type, R_Type, Fully_Conformant)
then
- Error_Msg_N
- ("subtype must statically match function result subtype",
- Subtype_Ind);
+ Error_No_Match (Subtype_Ind);
end if;
end if;
or else Null_Exclusion_Present (Parent (Scope_Id))) /=
Can_Never_Be_Null (R_Stm_Type)
then
- Error_Msg_N
- ("subtype must statically match function result subtype",
- Subtype_Ind);
+ Error_No_Match (Subtype_Ind);
end if;
-- AI05-103: for elementary types, subtypes must statically match
or else Is_Access_Type (R_Type)
then
if not Subtypes_Statically_Match (R_Stm_Type, R_Type) then
- Error_Msg_N
- ("subtype must statically match function result subtype",
- Subtype_Ind);
+ Error_No_Match (Subtype_Ind);
end if;
end if;
-- Can it really happen (extended return???)
Error_Msg_N
- ("aliased only allowed for limited"
- & " return objects in Ada 2012?", N);
+ ("aliased only allowed for limited return objects "
+ & "in Ada 2012??", N);
- elsif not Is_Immutably_Limited_Type (R_Type) then
+ elsif not Is_Limited_View (R_Type) then
Error_Msg_N ("aliased only allowed for limited"
& " return objects", N);
end if;
-- check the static cases.
if (Ada_Version < Ada_2005 or else Debug_Flag_Dot_L)
- and then Is_Immutably_Limited_Type (Etype (Scope_Id))
+ and then Is_Limited_View (Etype (Scope_Id))
and then Object_Access_Level (Expr) >
Subprogram_Access_Level (Scope_Id)
then
Reason => PE_Accessibility_Check_Failed));
Analyze (N);
- Error_Msg_N
- ("cannot return a local value by reference??", N);
- Error_Msg_NE
- ("\& will be raised at run time??",
- N, Standard_Program_Error);
+ Error_Msg_Warn := SPARK_Mode /= On;
+ Error_Msg_N ("cannot return a local value by reference<<", N);
+ Error_Msg_NE ("\& [<<", N, Standard_Program_Error);
end if;
end if;
-- Visible generic entity is callable within its own body
Set_Ekind (Gen_Id, Ekind (Body_Id));
+ Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Set_Ekind (Body_Id, E_Subprogram_Body);
Set_Convention (Body_Id, Convention (Gen_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id));
Set_Actual_Subtypes (N, Current_Scope);
- -- Deal with preconditions and postconditions. In formal verification
- -- mode, we keep pre- and postconditions attached to entities rather
- -- than inserted in the code, in order to facilitate a distinct
- -- treatment for them.
+ -- Deal with [refined] preconditions, postconditions, Contract_Cases,
+ -- invariants and predicates associated with the body and its spec.
+ -- Note that this is not pure expansion as Expand_Subprogram_Contract
+ -- prepares the contract assertions for generic subprograms or for
+ -- ASIS. Do not generate contract checks in SPARK mode.
- if not Alfa_Mode then
- Process_PPCs (N, Gen_Id, Body_Id);
+ if not GNATprove_Mode then
+ Expand_Subprogram_Contract (N, Gen_Id, Body_Id);
end if;
-- If the generic unit carries pre- or post-conditions, copy them
end loop;
end;
+ Check_SPARK_Mode_In_Generic (N);
+
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
+
Analyze_Declarations (Declarations (N));
Check_Completion;
Analyze (Handled_Statement_Sequence (N));
Null_Body :=
Make_Subprogram_Body (Loc,
Specification => New_Copy_Tree (Spec),
- Declarations => New_List,
+ Declarations => New_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (Make_Null_Statement (Loc))));
return;
else
-
-- Resolve the types of the formals now, because the freeze point
-- may appear in a different context, e.g. an instantiation.
Par : constant Node_Id := Parent (N);
begin
- if (Nkind (Par) = N_Function_Call
- and then N = Name (Par))
+ if (Nkind (Par) = N_Function_Call and then N = Name (Par))
or else Nkind (Par) = N_Function_Instantiation
- or else (Nkind (Par) = N_Indexed_Component
- and then N = Prefix (Par))
+ or else (Nkind (Par) = N_Indexed_Component and then N = Prefix (Par))
or else (Nkind (Par) = N_Pragma_Argument_Association
- and then not Is_Pragma_String_Literal (Par))
+ and then not Is_Pragma_String_Literal (Par))
or else Nkind (Par) = N_Subprogram_Renaming_Declaration
or else (Nkind (Par) = N_Attribute_Reference
and then Attribute_Name (Par) /= Name_Value)
if Is_Tagged_Type (Typ) then
null;
- elsif Nkind_In (Parent (Parent (N)),
- N_Accept_Statement,
- N_Entry_Body,
- N_Subprogram_Body)
+ elsif Nkind (Parent (N)) = N_Subprogram_Body
+ or else Nkind_In (Parent (Parent (N)), N_Accept_Statement,
+ N_Entry_Body)
then
Error_Msg_NE
("invalid use of untagged incomplete type&",
end if;
-- The type must be completed in the current package. This
- -- is checked at the end of the package declaraton, when
+ -- is checked at the end of the package declaration when
-- Taft-amendment types are identified. If the return type
-- is class-wide, there is no required check, the type can
-- be a bona fide TAT.
end if;
end Analyze_Subprogram_Body;
+ --------------------------------------
+ -- Analyze_Subprogram_Body_Contract --
+ --------------------------------------
+
+ procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
+ Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Ref_Depends : Node_Id := Empty;
+ Ref_Global : Node_Id := Empty;
+ Spec_Id : Entity_Id;
+
+ begin
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related subprogram body.
+
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
+
+ -- When a subprogram body declaration is illegal, its defining entity is
+ -- left unanalyzed. There is nothing left to do in this case because the
+ -- body lacks a contract, or even a proper Ekind.
+
+ if Ekind (Body_Id) = E_Void then
+ return;
+ end if;
+
+ if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
+ Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+ else
+ Spec_Id := Corresponding_Spec (Body_Decl);
+ end if;
+
+ -- Locate and store pragmas Refined_Depends and Refined_Global since
+ -- their order of analysis matters.
+
+ Prag := Classifications (Contract (Body_Id));
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Refined_Depends then
+ Ref_Depends := Prag;
+ elsif Pragma_Name (Prag) = Name_Refined_Global then
+ Ref_Global := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze Refined_Global first as Refined_Depends may mention items
+ -- classified in the global refinement.
+
+ if Present (Ref_Global) then
+ Analyze_Refined_Global_In_Decl_Part (Ref_Global);
+
+ -- When the corresponding Global aspect/pragma references a state with
+ -- visible refinement, the body requires Refined_Global. Refinement is
+ -- not required when SPARK checks are suppressed.
+
+ elsif Present (Spec_Id) then
+ Prag := Get_Pragma (Spec_Id, Pragma_Global);
+
+ if SPARK_Mode /= Off
+ and then Present (Prag)
+ and then Contains_Refined_State (Prag)
+ then
+ Error_Msg_NE
+ ("body of subprogram & requires global refinement",
+ Body_Decl, Spec_Id);
+ end if;
+ end if;
+
+ -- Refined_Depends must be analyzed after Refined_Global in order to see
+ -- the modes of all global refinements.
+
+ if Present (Ref_Depends) then
+ Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
+
+ -- When the corresponding Depends aspect/pragma references a state with
+ -- visible refinement, the body requires Refined_Depends. Refinement is
+ -- not required when SPARK checks are suppressed.
+
+ elsif Present (Spec_Id) then
+ Prag := Get_Pragma (Spec_Id, Pragma_Depends);
+
+ if SPARK_Mode /= Off
+ and then Present (Prag)
+ and then Contains_Refined_State (Prag)
+ then
+ Error_Msg_NE
+ ("body of subprogram & requires dependance refinement",
+ Body_Decl, Spec_Id);
+ end if;
+ end if;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Mode);
+ end Analyze_Subprogram_Body_Contract;
+
------------------------------------
-- Analyze_Subprogram_Body_Helper --
------------------------------------
-- chained beyond that point. It is initialized to Empty to deal with
-- the case where there is no separate spec.
+ procedure Analyze_Aspects_On_Body_Or_Stub;
+ -- Analyze the aspect specifications of a subprogram body [stub]. It is
+ -- assumed that N has aspects.
+
procedure Check_Anonymous_Return;
-- Ada 2005: if a function returns an access type that denotes a task,
-- or a type that contains tasks, we must create a master entity for
-- indicator, check that it is consistent with the known status of the
-- entity.
+ -------------------------------------
+ -- Analyze_Aspects_On_Body_Or_Stub --
+ -------------------------------------
+
+ procedure Analyze_Aspects_On_Body_Or_Stub is
+ procedure Diagnose_Misplaced_Aspects;
+ -- Subprogram body [stub] N has aspects, but they are not properly
+ -- placed. Provide precise diagnostics depending on the aspects
+ -- involved.
+
+ --------------------------------
+ -- Diagnose_Misplaced_Aspects --
+ --------------------------------
+
+ procedure Diagnose_Misplaced_Aspects is
+ Asp : Node_Id;
+ Asp_Nam : Name_Id;
+ Asp_Id : Aspect_Id;
+ -- The current aspect along with its name and id
+
+ procedure SPARK_Aspect_Error (Ref_Nam : Name_Id);
+ -- Emit an error message concerning SPARK aspect Asp. Ref_Nam is
+ -- the name of the refined version of the aspect.
+
+ ------------------------
+ -- SPARK_Aspect_Error --
+ ------------------------
+
+ procedure SPARK_Aspect_Error (Ref_Nam : Name_Id) is
+ begin
+ -- The corresponding spec already contains the aspect in
+ -- question and the one appearing on the body must be the
+ -- refined form:
+
+ -- procedure P with Global ...;
+ -- procedure P with Global ... is ... end P;
+ -- ^
+ -- Refined_Global
+
+ if Has_Aspect (Spec_Id, Asp_Id) then
+ Error_Msg_Name_1 := Asp_Nam;
+
+ -- Subunits cannot carry aspects that apply to a subprogram
+ -- declaration.
+
+ if Nkind (Parent (N)) = N_Subunit then
+ Error_Msg_N ("aspect % cannot apply to a subunit", Asp);
+
+ else
+ Error_Msg_Name_2 := Ref_Nam;
+ Error_Msg_N ("aspect % should be %", Asp);
+ end if;
+
+ -- Otherwise the aspect must appear in the spec, not in the
+ -- body:
+
+ -- procedure P;
+ -- procedure P with Global ... is ... end P;
+
+ else
+ Error_Msg_N
+ ("aspect specification must appear in subprogram "
+ & "declaration", Asp);
+ end if;
+ end SPARK_Aspect_Error;
+
+ -- Start of processing for Diagnose_Misplaced_Aspects
+
+ begin
+ -- Iterate over the aspect specifications and emit specific errors
+ -- where applicable.
+
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ Asp_Nam := Chars (Identifier (Asp));
+ Asp_Id := Get_Aspect_Id (Asp_Nam);
+
+ -- Do not emit errors on aspects that can appear on a
+ -- subprogram body. This scenario occurs when the aspect
+ -- specification list contains both misplaced and properly
+ -- placed aspects.
+
+ if Aspect_On_Body_Or_Stub_OK (Asp_Id) then
+ null;
+
+ -- Special diagnostics for SPARK aspects
+
+ elsif Asp_Nam = Name_Depends then
+ SPARK_Aspect_Error (Name_Refined_Depends);
+
+ elsif Asp_Nam = Name_Global then
+ SPARK_Aspect_Error (Name_Refined_Global);
+
+ elsif Asp_Nam = Name_Post then
+ SPARK_Aspect_Error (Name_Refined_Post);
+
+ else
+ Error_Msg_N
+ ("aspect specification must appear in subprogram "
+ & "declaration", Asp);
+ end if;
+
+ Next (Asp);
+ end loop;
+ end Diagnose_Misplaced_Aspects;
+
+ -- Start of processing for Analyze_Aspects_On_Body_Or_Stub
+
+ begin
+ -- Language-defined aspects cannot be associated with a subprogram
+ -- body [stub] if the subprogram has a spec. Certain implementation
+ -- defined aspects are allowed to break this rule (for list, see
+ -- table Aspect_On_Body_Or_Stub_OK).
+
+ if Present (Spec_Id) and then not Aspects_On_Body_Or_Stub_OK (N) then
+ Diagnose_Misplaced_Aspects;
+ else
+ Analyze_Aspect_Specifications (N, Body_Id);
+ end if;
+ end Analyze_Aspects_On_Body_Or_Stub;
+
----------------------------
-- Check_Anonymous_Return --
----------------------------
Make_Defining_Identifier (Loc, Name_uMaster),
Constant_Present => True,
Object_Definition =>
- New_Reference_To (RTE (RE_Master_Id), Loc),
+ New_Occurrence_Of (RTE (RE_Master_Id), Loc),
Expression =>
Make_Explicit_Dereference (Loc,
- New_Reference_To (RTE (RE_Current_Master), Loc)));
+ New_Occurrence_Of (RTE (RE_Current_Master), Loc)));
if Present (Declarations (N)) then
Prepend (Decl, Declarations (N));
Set_Has_Pragma_Inline_Always (Subp);
end if;
+ -- Prior to copying the subprogram body to create a template
+ -- for it for subsequent inlining, remove the pragma from
+ -- the current body so that the copy that will produce the
+ -- new body will start from a completely unanalyzed tree.
+
+ if Nkind (Parent (Prag)) = N_Subprogram_Body then
+ Rewrite (Prag, Make_Null_Statement (Sloc (Prag)));
+ end if;
+
Spec := Subp;
end;
end if;
begin
if Ekind (Typ) = E_Incomplete_Type
- and then From_With_Type (Typ)
+ and then From_Limited_With (Typ)
and then Present (Non_Limited_View (Typ))
then
Set_Etype (Id, Non_Limited_View (Typ));
elsif not Present (Overridden_Operation (Spec_Id)) then
Error_Msg_NE
("subprogram& is not overriding", Body_Spec, Spec_Id);
+
+ -- Overriding indicators aren't allowed for protected subprogram
+ -- bodies (see the Confirmation in Ada Comment AC95-00213). Change
+ -- this to a warning if -gnatd.E is enabled.
+
+ elsif Ekind (Scope (Spec_Id)) = E_Protected_Type then
+ Error_Msg_Warn := Error_To_Warning;
+ Error_Msg_N
+ ("<<overriding indicator not allowed for protected "
+ & "subprogram body", Body_Spec);
end if;
elsif Must_Not_Override (Body_Spec) then
("subprogram & overrides predefined operator ",
Body_Spec, Spec_Id);
- -- If this is not a primitive operation or protected subprogram,
- -- then the overriding indicator is altogether illegal.
+ -- Overriding indicators aren't allowed for protected subprogram
+ -- bodies (see the Confirmation in Ada Comment AC95-00213). Change
+ -- this to a warning if -gnatd.E is enabled.
- elsif not Is_Primitive (Spec_Id)
- and then Ekind (Scope (Spec_Id)) /= E_Protected_Type
- then
+ elsif Ekind (Scope (Spec_Id)) = E_Protected_Type then
+ Error_Msg_Warn := Error_To_Warning;
+
+ Error_Msg_N
+ ("<<overriding indicator not allowed " &
+ "for protected subprogram body",
+ Body_Spec);
+
+ -- If this is not a primitive operation, then the overriding
+ -- indicator is altogether illegal.
+
+ elsif not Is_Primitive (Spec_Id) then
Error_Msg_N
("overriding indicator only allowed " &
"if subprogram is primitive",
Body_Spec);
end if;
+ -- If checking the style rule and the operation overrides, then
+ -- issue a warning about a missing overriding_indicator. Protected
+ -- subprogram bodies are excluded from this style checking, since
+ -- they aren't primitives (even though their declarations can
+ -- override) and aren't allowed to have an overriding_indicator.
+
elsif Style_Check
and then Present (Overridden_Operation (Spec_Id))
+ and then Ekind (Scope (Spec_Id)) /= E_Protected_Type
then
pragma Assert (Unit_Declaration_Node (Body_Id) = N);
Style.Missing_Overriding (N, Body_Id);
end if;
end if;
- -- Ada 2012 aspects may appear in a subprogram body, but only if there
- -- is no previous spec. Ditto for a subprogram stub that does not have
- -- a corresponding spec, but for which there may also be a spec_id.
-
- if Has_Aspects (N) then
- if Present (Spec_Id) then
- Error_Msg_N
- ("aspect specifications must appear in subprogram declaration",
- N);
- else
- Analyze_Aspect_Specifications (N, Body_Id);
- end if;
- end if;
-
-- Previously we scanned the body to look for nested subprograms, and
-- rejected an inline directive if nested subprograms were present,
-- because the back-end would generate conflicting symbols for the
and then
(Nkind (Original_Node (Spec_Decl)) =
N_Subprogram_Renaming_Declaration
- or else (Present (Corresponding_Body (Spec_Decl))
- and then
- Nkind (Unit_Declaration_Node
- (Corresponding_Body (Spec_Decl))) =
- N_Subprogram_Renaming_Declaration))
+ or else (Present (Corresponding_Body (Spec_Decl))
+ and then
+ Nkind (Unit_Declaration_Node
+ (Corresponding_Body (Spec_Decl))) =
+ N_Subprogram_Renaming_Declaration))
then
Conformant := True;
Reference_Body_Formals (Spec_Id, Body_Id);
end if;
- if Nkind (N) /= N_Subprogram_Body_Stub then
+ Set_Ekind (Body_Id, E_Subprogram_Body);
+
+ if Nkind (N) = N_Subprogram_Body_Stub then
+ Set_Corresponding_Spec_Of_Stub (N, Spec_Id);
+
+ -- Regular body
+
+ else
Set_Corresponding_Spec (N, Spec_Id);
-- Ada 2005 (AI-345): If the operation is a primitive operation
and then Present (First_Entity (Spec_Id))
and then Ekind (Etype (First_Entity (Spec_Id))) = E_Record_Type
and then Is_Tagged_Type (Etype (First_Entity (Spec_Id)))
- and then
- Present (Interfaces (Etype (First_Entity (Spec_Id))))
- and then
- Present
- (Corresponding_Concurrent_Type
- (Etype (First_Entity (Spec_Id))))
+ and then Present (Interfaces (Etype (First_Entity (Spec_Id))))
+ and then Present (Corresponding_Concurrent_Type
+ (Etype (First_Entity (Spec_Id))))
then
declare
Typ : constant Entity_Id := Etype (First_Entity (Spec_Id));
end if;
Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id);
- Set_Ekind (Body_Id, E_Subprogram_Body);
+ Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Set_Scope (Body_Id, Scope (Spec_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
Generate_Reference
(Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
Install_Formals (Body_Id);
+
Push_Scope (Body_Id);
end if;
Generate_Reference_To_Formals (Body_Id);
end if;
+ -- Set SPARK_Mode from context
+
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
+
-- If the return type is an anonymous access type whose designated type
-- is the limited view of a class-wide type and the non-limited view is
-- available, update the return type accordingly.
if Ekind (Rtyp) = E_Anonymous_Access_Type then
Etyp := Directly_Designated_Type (Rtyp);
- if Is_Class_Wide_Type (Etyp) and then From_With_Type (Etyp) then
+ if Is_Class_Wide_Type (Etyp)
+ and then From_Limited_With (Etyp)
+ then
Set_Directly_Designated_Type
(Etype (Current_Scope), Available_View (Etyp));
end if;
Check_Eliminated (Body_Id);
if Nkind (N) = N_Subprogram_Body_Stub then
+
+ -- Analyze any aspect specifications that appear on the subprogram
+ -- body stub.
+
+ if Has_Aspects (N) then
+ Analyze_Aspects_On_Body_Or_Stub;
+ end if;
+
+ -- Stop the analysis now as the stub cannot be inlined, plus it does
+ -- not have declarative or statement lists.
+
return;
end if;
HSS := Handled_Statement_Sequence (N);
Set_Actual_Subtypes (N, Current_Scope);
- -- Deal with preconditions and postconditions. In formal verification
- -- mode, we keep pre- and postconditions attached to entities rather
- -- than inserted in the code, in order to facilitate a distinct
- -- treatment for them.
-
- if not Alfa_Mode then
- Process_PPCs (N, Spec_Id, Body_Id);
- end if;
-
-- Add a declaration for the Protection object, renaming declarations
-- for discriminals and privals and finally a declaration for the entry
-- family index (if applicable). This form of early expansion is done
-- when the Expander is active because Install_Private_Data_Declarations
-- references entities which were created during regular expansion. The
- -- body may be the rewritting of an expression function, and we need to
- -- verify that the original node is in the source.
+ -- subprogram entity must come from source, and not be an internally
+ -- generated subprogram.
- if Full_Expander_Active
- and then Comes_From_Source (Original_Node (N))
+ if Expander_Active
and then Present (Prot_Typ)
and then Present (Spec_Id)
+ and then Comes_From_Source (Spec_Id)
and then not Is_Eliminated (Spec_Id)
then
Install_Private_Data_Declarations
Exchange_Limited_Views (Spec_Id);
end if;
+ -- Analyze any aspect specifications that appear on the subprogram body
+
+ if Has_Aspects (N) then
+ Analyze_Aspects_On_Body_Or_Stub;
+ end if;
+
+ -- Deal with [refined] preconditions, postconditions, Contract_Cases,
+ -- invariants and predicates associated with the body and its spec.
+ -- Note that this is not pure expansion as Expand_Subprogram_Contract
+ -- prepares the contract assertions for generic subprograms or for ASIS.
+ -- Do not generate contract checks in SPARK mode.
+
+ if not GNATprove_Mode then
+ Expand_Subprogram_Contract (N, Spec_Id, Body_Id);
+ end if;
+
-- Analyze the declarations (this call will analyze the precondition
-- Check pragmas we prepended to the list, as well as the declaration
-- of the _Postconditions procedure).
Analyze_Declarations (Declarations (N));
+ -- After declarations have been analyzed, the body has been set
+ -- its final value of SPARK_Mode. Check that SPARK_Mode for body
+ -- is consistent with SPARK_Mode for spec.
+
+ if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
+ if Present (SPARK_Pragma (Spec_Id)) then
+ if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
+ and then
+ Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+ then
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id));
+ Error_Msg_NE
+ ("\value Off was set for SPARK_Mode on&#", N, Spec_Id);
+ end if;
+
+ elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then
+ null;
+
+ else
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (Spec_Id);
+ Error_Msg_NE ("\no value was set for SPARK_Mode on&#", N, Spec_Id);
+ end if;
+ end if;
+
-- Check completion, and analyze the statements
Check_Completion;
-- the body of the procedure. But first we deal with a special case
-- where we want to modify this check. If the body of the subprogram
-- starts with a raise statement or its equivalent, or if the body
- -- consists entirely of a null statement, then it is pretty obvious
- -- that it is OK to not reference the parameters. For example, this
- -- might be the following common idiom for a stubbed function:
- -- statement of the procedure raises an exception. In particular this
- -- deals with the common idiom of a stubbed function, which might
- -- appear as something like:
+ -- consists entirely of a null statement, then it is pretty obvious that
+ -- it is OK to not reference the parameters. For example, this might be
+ -- the following common idiom for a stubbed function: statement of the
+ -- procedure raises an exception. In particular this deals with the
+ -- common idiom of a stubbed function, which appears something like:
-- function F (A : Integer) return Some_Type;
-- X : Some_Type;
-- Here the purpose of X is simply to satisfy the annoying requirement
-- in Ada that there be at least one return, and we certainly do not
- -- want to go posting warnings on X that it is not initialized! On
+ -- want to go posting warnings on X that it is not initialized. On
-- the other hand, if X is entirely unreferenced that should still
-- get a warning.
end;
end Analyze_Subprogram_Body_Helper;
- ------------------------------------
- -- Analyze_Subprogram_Declaration --
- ------------------------------------
+ ---------------------------------
+ -- Analyze_Subprogram_Contract --
+ ---------------------------------
- procedure Analyze_Subprogram_Declaration (N : Node_Id) is
- Scop : constant Entity_Id := Current_Scope;
- Designator : Entity_Id;
- Is_Completion : Boolean;
- -- Indicates whether a null procedure declaration is a completion
+ procedure Analyze_Subprogram_Contract (Subp : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp);
+ Case_Prag : Node_Id := Empty;
+ Depends : Node_Id := Empty;
+ Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Nam : Name_Id;
+ Post_Prag : Node_Id := Empty;
+ Prag : Node_Id;
+ Seen_In_Case : Boolean := False;
+ Seen_In_Post : Boolean := False;
begin
- -- Null procedures are not allowed in SPARK
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related subprogram body.
- if Nkind (Specification (N)) = N_Procedure_Specification
- and then Null_Present (Specification (N))
- then
- Check_SPARK_Restriction ("null procedure is not allowed", N);
+ Save_SPARK_Mode_And_Set (Subp, Mode);
- if Is_Protected_Type (Current_Scope) then
- Error_Msg_N ("protected operation cannot be a null procedure", N);
- end if;
+ if Present (Items) then
- Analyze_Null_Procedure (N, Is_Completion);
+ -- Analyze pre- and postconditions
- if Is_Completion then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Subp);
- -- The null procedure acts as a body, nothing further is needed.
+ -- Verify whether a postcondition mentions attribute 'Result and
+ -- its expression introduces a post-state.
- return;
- end if;
- end if;
+ if Warn_On_Suspicious_Contract
+ and then Pragma_Name (Prag) = Name_Postcondition
+ then
+ Post_Prag := Prag;
+ Check_Result_And_Post_State (Prag, Seen_In_Post);
+ end if;
- Designator := Analyze_Subprogram_Specification (Specification (N));
+ Prag := Next_Pragma (Prag);
+ end loop;
- -- A reference may already have been generated for the unit name, in
- -- which case the following call is redundant. However it is needed for
- -- declarations that are the rewriting of an expression function.
+ -- Analyze contract-cases and test-cases
- Generate_Definition (Designator);
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ Nam := Pragma_Name (Prag);
- if Debug_Flag_C then
- Write_Str ("==> subprogram spec ");
- Write_Name (Chars (Designator));
- Write_Str (" from ");
- Write_Location (Sloc (N));
- Write_Eol;
- Indent;
- end if;
+ if Nam = Name_Contract_Cases then
+ Analyze_Contract_Cases_In_Decl_Part (Prag);
- Validate_RCI_Subprogram_Declaration (N);
- New_Overloaded_Entity (Designator);
- Check_Delayed_Subprogram (Designator);
+ -- Verify whether contract-cases mention attribute 'Result and
+ -- its expression introduces a post-state. Perform the check
+ -- only when the pragma is legal.
- -- If the type of the first formal of the current subprogram is a
- -- non-generic tagged private type, mark the subprogram as being a
- -- private primitive. Ditto if this is a function with controlling
- -- result, and the return type is currently private. In both cases,
- -- the type of the controlling argument or result must be in the
- -- current scope for the operation to be primitive.
+ if Warn_On_Suspicious_Contract
+ and then not Error_Posted (Prag)
+ then
+ Case_Prag := Prag;
+ Check_Result_And_Post_State (Prag, Seen_In_Case);
+ end if;
- if Has_Controlling_Result (Designator)
- and then Is_Private_Type (Etype (Designator))
- and then Scope (Etype (Designator)) = Current_Scope
- and then not Is_Generic_Actual_Type (Etype (Designator))
+ else
+ pragma Assert (Nam = Name_Test_Case);
+ Analyze_Test_Case_In_Decl_Part (Prag, Subp);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze classification pragmas
+
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Nam := Pragma_Name (Prag);
+
+ if Nam = Name_Depends then
+ Depends := Prag;
+ else pragma Assert (Nam = Name_Global);
+ Global := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Analyze Global first as Depends may mention items classified in
+ -- the global categorization.
+
+ if Present (Global) then
+ Analyze_Global_In_Decl_Part (Global);
+ end if;
+
+ -- Depends must be analyzed after Global in order to see the modes of
+ -- all global items.
+
+ if Present (Depends) then
+ Analyze_Depends_In_Decl_Part (Depends);
+ end if;
+ end if;
+
+ -- Emit an error when neither the postconditions nor the contract-cases
+ -- mention attribute 'Result in the context of a function.
+
+ if Warn_On_Suspicious_Contract
+ and then Ekind_In (Subp, E_Function, E_Generic_Function)
+ then
+ if Present (Case_Prag)
+ and then not Seen_In_Case
+ and then Present (Post_Prag)
+ and then not Seen_In_Post
+ then
+ Error_Msg_N
+ ("neither function postcondition nor contract cases mention "
+ & "result?T?", Post_Prag);
+
+ elsif Present (Case_Prag) and then not Seen_In_Case then
+ Error_Msg_N
+ ("contract cases do not mention result?T?", Case_Prag);
+
+ -- OK if we have at least one IN OUT parameter
+
+ elsif Present (Post_Prag) and then not Seen_In_Post then
+ declare
+ F : Entity_Id;
+ begin
+ F := First_Formal (Subp);
+ while Present (F) loop
+ if Ekind (F) = E_In_Out_Parameter then
+ return;
+ else
+ Next_Formal (F);
+ end if;
+ end loop;
+ end;
+
+ -- If no in-out parameters and no mention of Result, the contract
+ -- is certainly suspicious.
+
+ Error_Msg_N
+ ("function postcondition does not mention result?T?", Post_Prag);
+ end if;
+ end if;
+
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
+ Restore_SPARK_Mode (Mode);
+ end Analyze_Subprogram_Contract;
+
+ ------------------------------------
+ -- Analyze_Subprogram_Declaration --
+ ------------------------------------
+
+ procedure Analyze_Subprogram_Declaration (N : Node_Id) is
+ Scop : constant Entity_Id := Current_Scope;
+ Designator : Entity_Id;
+
+ Is_Completion : Boolean;
+ -- Indicates whether a null procedure declaration is a completion
+
+ begin
+ -- Null procedures are not allowed in SPARK
+
+ if Nkind (Specification (N)) = N_Procedure_Specification
+ and then Null_Present (Specification (N))
+ then
+ Check_SPARK_Restriction ("null procedure is not allowed", N);
+
+ if Is_Protected_Type (Current_Scope) then
+ Error_Msg_N ("protected operation cannot be a null procedure", N);
+ end if;
+
+ Analyze_Null_Procedure (N, Is_Completion);
+
+ if Is_Completion then
+
+ -- The null procedure acts as a body, nothing further is needed.
+
+ return;
+ end if;
+ end if;
+
+ Designator := Analyze_Subprogram_Specification (Specification (N));
+
+ -- A reference may already have been generated for the unit name, in
+ -- which case the following call is redundant. However it is needed for
+ -- declarations that are the rewriting of an expression function.
+
+ Generate_Definition (Designator);
+
+ -- Set SPARK mode from current context (may be overwritten later with
+ -- explicit pragma).
+
+ Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Designator, True);
+
+ if Debug_Flag_C then
+ Write_Str ("==> subprogram spec ");
+ Write_Name (Chars (Designator));
+ Write_Str (" from ");
+ Write_Location (Sloc (N));
+ Write_Eol;
+ Indent;
+ end if;
+
+ Validate_RCI_Subprogram_Declaration (N);
+ New_Overloaded_Entity (Designator);
+ Check_Delayed_Subprogram (Designator);
+
+ -- If the type of the first formal of the current subprogram is a non-
+ -- generic tagged private type, mark the subprogram as being a private
+ -- primitive. Ditto if this is a function with controlling result, and
+ -- the return type is currently private. In both cases, the type of the
+ -- controlling argument or result must be in the current scope for the
+ -- operation to be primitive.
+
+ if Has_Controlling_Result (Designator)
+ and then Is_Private_Type (Etype (Designator))
+ and then Scope (Etype (Designator)) = Current_Scope
+ and then not Is_Generic_Actual_Type (Etype (Designator))
then
Set_Is_Private_Primitive (Designator);
-- Emit a warning if this is a call to a runtime subprogram
-- which is located inside a generic. Previously this call
- -- was silently skipped!
+ -- was silently skipped.
if Is_Generic_Instance (Subp) then
declare
elsif Is_Entity_Name (Orig_Expr)
and then Ekind (Entity (Orig_Expr)) = E_Constant
- and then Is_Static_Expression (Orig_Expr)
+ and then Is_OK_Static_Expression (Orig_Expr)
then
return OK;
else
-- Compiling with optimizations enabled
else
- -- Procedures are never frontend inlined in this case!
+ -- Procedures are never frontend inlined in this case
if Ekind (Subp) /= E_Function then
return False;
Null_Exclusion_Present =>
Null_Exclusion_Present (Parent (Formal)),
Parameter_Type =>
- New_Reference_To (Etype (Formal), Loc),
+ New_Occurrence_Of (Etype (Formal), Loc),
Expression =>
Copy_Separate_Tree (Expression (Parent (Formal)))));
begin
Append_To (Actual_List,
- New_Reference_To (Defining_Identifier (New_Obj), Loc));
+ New_Occurrence_Of (Defining_Identifier (New_Obj), Loc));
Formal := First_Formal (Spec_Id);
while Present (Formal) loop
- Append_To (Actual_List, New_Reference_To (Formal, Loc));
+ Append_To (Actual_List, New_Occurrence_Of (Formal, Loc));
-- Avoid spurious warning on unreferenced formals
Proc_Call :=
Make_Procedure_Call_Statement (Loc,
- Name => New_Reference_To (Proc_Id, Loc),
+ Name => New_Occurrence_Of (Proc_Id, Loc),
Parameter_Associations => Actual_List);
end;
Make_Simple_Return_Statement (Loc,
Expression =>
- New_Reference_To
+ New_Occurrence_Of
(Defining_Identifier (New_Obj), Loc)))));
Rewrite (Ret_Node, Blk_Stmt);
end;
end if;
- -- Build the body to inline only if really needed!
+ -- Build the body to inline only if really needed
if Check_Body_To_Inline (N, Spec_Id)
and then Serious_Errors_Detected = 0
null;
elsif not Conforming_Types (Old_Type, New_Type, Ctype, Get_Inst) then
- Conformance_Error ("\return type does not match!", New_Id);
+ if Ctype >= Subtype_Conformant
+ and then not Predicates_Match (Old_Type, New_Type)
+ then
+ Conformance_Error
+ ("\predicate of return type does not match!", New_Id);
+ else
+ Conformance_Error
+ ("\return type does not match!", New_Id);
+ end if;
+
return;
end if;
-- Note: we use the entity information, rather than going directly
-- to the specification in the tree. This is not only simpler, but
-- absolutely necessary for some cases of conformance tests between
- -- operators, where the declaration tree simply does not exist!
+ -- operators, where the declaration tree simply does not exist.
Old_Formal := First_Formal (Old_Id);
New_Formal := First_Formal (New_Id);
if Errmsg and then Old_Formal_Base = Any_Type then
Conforms := False;
else
- Conformance_Error ("\type of & does not match!", New_Formal);
+ if Ctype >= Subtype_Conformant
+ and then
+ not Predicates_Match (Old_Formal_Base, New_Formal_Base)
+ then
+ Conformance_Error
+ ("\predicate of & does not match!", New_Formal);
+ else
+ Conformance_Error
+ ("\type of & does not match!", New_Formal);
+ end if;
end if;
return;
----------------------
procedure Check_Convention (Op : Entity_Id) is
+ function Convention_Of (Id : Entity_Id) return Convention_Id;
+ -- Given an entity, return its convention. The function treats Ghost
+ -- as convention Ada because the two have the same dynamic semantics.
+
+ -------------------
+ -- Convention_Of --
+ -------------------
+
+ function Convention_Of (Id : Entity_Id) return Convention_Id is
+ Conv : constant Convention_Id := Convention (Id);
+ begin
+ if Conv = Convention_Ghost then
+ return Convention_Ada;
+ else
+ return Conv;
+ end if;
+ end Convention_Of;
+
+ -- Local variables
+
+ Op_Conv : constant Convention_Id := Convention_Of (Op);
+ Iface_Conv : Convention_Id;
Iface_Elmt : Elmt_Id;
Iface_Prim_Elmt : Elmt_Id;
Iface_Prim : Entity_Id;
+ -- Start of processing for Check_Convention
+
begin
Iface_Elmt := First_Elmt (Ifaces_List);
while Present (Iface_Elmt) loop
Iface_Prim_Elmt :=
- First_Elmt (Primitive_Operations (Node (Iface_Elmt)));
+ First_Elmt (Primitive_Operations (Node (Iface_Elmt)));
while Present (Iface_Prim_Elmt) loop
Iface_Prim := Node (Iface_Prim_Elmt);
+ Iface_Conv := Convention_Of (Iface_Prim);
if Is_Interface_Conformant (Typ, Iface_Prim, Op)
- and then Convention (Iface_Prim) /= Convention (Op)
+ and then Iface_Conv /= Op_Conv
then
Error_Msg_N
("inconsistent conventions in primitive operations", Typ);
Error_Msg_Name_1 := Chars (Op);
- Error_Msg_Name_2 := Get_Convention_Name (Convention (Op));
+ Error_Msg_Name_2 := Get_Convention_Name (Op_Conv);
Error_Msg_Sloc := Sloc (Op);
if Comes_From_Source (Op) or else No (Alias (Op)) then
end if;
Error_Msg_Name_1 := Chars (Op);
- Error_Msg_Name_2 :=
- Get_Convention_Name (Convention (Iface_Prim));
- Error_Msg_Sloc := Sloc (Iface_Prim);
+ Error_Msg_Name_2 := Get_Convention_Name (Iface_Conv);
+ Error_Msg_Sloc := Sloc (Iface_Prim);
Error_Msg_N
("\\overridden operation % with " &
"convention % defined #", Typ);
then
Set_Has_Delayed_Freeze (Designator);
- elsif Ekind (T) = E_Incomplete_Type and then From_With_Type (T) then
+ elsif Ekind (T) = E_Incomplete_Type
+ and then From_Limited_With (T)
+ then
Set_Has_Delayed_Freeze (Designator);
-- AI05-0151: In Ada 2012, Incomplete types can appear in the profile
Typ : constant Entity_Id := Etype (Designator);
Utyp : constant Entity_Id := Underlying_Type (Typ);
begin
- if Is_Immutably_Limited_Type (Typ) then
+ if Is_Limited_View (Typ) then
Set_Returns_By_Ref (Designator);
elsif Present (Utyp) and then CW_Or_Has_Controlled_Part (Utyp) then
Set_Returns_By_Ref (Designator);
else
Set_Overridden_Operation (Subp, Overridden_Subp);
end if;
-
- -- Ensure that a ghost function is not overriding another routine
-
- elsif Is_Ghost_Function (Subp) then
- Error_Msg_N ("ghost function & cannot be overriding", Subp);
end if;
end if;
Stm : Node_Id;
Kind : Node_Kind;
+ function Assert_False return Boolean;
+ -- Returns True if Last_Stm is a pragma Assert (False) that has been
+ -- rewritten as a null statement when assertions are off. The assert
+ -- is not active, but it is still enough to kill the warning.
+
+ ------------------
+ -- Assert_False --
+ ------------------
+
+ function Assert_False return Boolean is
+ Orig : constant Node_Id := Original_Node (Last_Stm);
+
+ begin
+ if Nkind (Orig) = N_Pragma
+ and then Pragma_Name (Orig) = Name_Assert
+ and then not Error_Posted (Orig)
+ then
+ declare
+ Arg : constant Node_Id :=
+ First (Pragma_Argument_Associations (Orig));
+ Exp : constant Node_Id := Expression (Arg);
+ begin
+ return Nkind (Exp) = N_Identifier
+ and then Chars (Exp) = Name_False;
+ end;
+
+ else
+ return False;
+ end if;
+ end Assert_False;
+
+ -- Local variables
+
Raise_Exception_Call : Boolean;
-- Set True if statement sequence terminated by Raise_Exception call
-- or a Reraise_Occurrence call.
+ -- Start of processing for Check_Statement_Sequence
+
begin
Raise_Exception_Call := False;
-- Note: if both ECA and DCA are missing the return, then we
-- post only one message, should be enough to fix the bugs.
-- If not we will get a message next time on the DCA when the
- -- ECA is fixed!
+ -- ECA is fixed.
elsif No (Statements (DCA)) then
Last_Stm := DCA;
-- If we fall through, issue appropriate message
if Mode = 'F' then
- if not Raise_Exception_Call then
+
+ -- Kill warning if last statement is a raise exception call,
+ -- or a pragma Assert (False). Note that with assertions enabled,
+ -- such a pragma has been converted into a raise exception call
+ -- already, so the Assert_False is for the assertions off case.
+
+ if not Raise_Exception_Call and then not Assert_False then
+
+ -- In GNATprove mode, it is an error to have a missing return
+
+ Error_Msg_Warn := SPARK_Mode /= On;
+
+ -- Issue error message or warning
+
Error_Msg_N
- ("RETURN statement missing following this statement??!",
+ ("RETURN statement missing following this statement<<!",
Last_Stm);
Error_Msg_N
- ("\Program_Error may be raised at run time??!",
- Last_Stm);
+ ("\Program_Error ]<<!", Last_Stm);
end if;
-- Note: we set Err even though we have not issued a warning
else
if not Raise_Exception_Call then
- Error_Msg_N
- ("implied return after this statement " &
- "will raise Program_Error??",
- Last_Stm);
+ if GNATprove_Mode then
+ Error_Msg_N
+ ("implied return after this statement "
+ & "would have raised Program_Error", Last_Stm);
+ else
+ Error_Msg_N
+ ("implied return after this statement "
+ & "will raise Program_Error??", Last_Stm);
+ end if;
+
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_NE
- ("\procedure & is marked as No_Return??!",
- Last_Stm, Proc);
+ ("\procedure & is marked as No_Return<<!", Last_Stm, Proc);
end if;
declare
end if;
end Check_Returns;
- -------------------------------
- -- Check_Subprogram_Contract --
- -------------------------------
-
- procedure Check_Subprogram_Contract (Spec_Id : Entity_Id) is
+ ----------------------------
+ -- Check_Subprogram_Order --
+ ----------------------------
- -- Code is currently commented out as, in some cases, it causes crashes
- -- because Direct_Primitive_Operations is not available for a private
- -- type. This may cause more warnings to be issued than necessary. See
- -- below for the intended use of this variable. ???
+ procedure Check_Subprogram_Order (N : Node_Id) is
--- Inherited : constant Subprogram_List :=
--- Inherited_Subprograms (Spec_Id);
--- -- List of subprograms inherited by this subprogram
+ function Subprogram_Name_Greater (S1, S2 : String) return Boolean;
+ -- This is used to check if S1 > S2 in the sense required by this test,
+ -- for example nameab < namec, but name2 < name10.
- -- We ignore postconditions "True" or "False" and contract-cases which
- -- have similar consequence expressions, which we call "trivial", when
- -- issuing warnings, since these postconditions and contract-cases
- -- purposedly ignore the post-state.
+ -----------------------------
+ -- Subprogram_Name_Greater --
+ -----------------------------
- Last_Postcondition : Node_Id := Empty;
- -- Last non-trivial postcondition on the subprogram, or else Empty if
- -- either no non-trivial postcondition or only inherited postconditions.
+ function Subprogram_Name_Greater (S1, S2 : String) return Boolean is
+ L1, L2 : Positive;
+ N1, N2 : Natural;
- Last_Contract_Cases : Node_Id := Empty;
- -- Last non-trivial contract-cases on the subprogram, or else Empty
+ begin
+ -- Deal with special case where names are identical except for a
+ -- numerical suffix. These are handled specially, taking the numeric
+ -- ordering from the suffix into account.
- Attribute_Result_Mentioned : Boolean := False;
- -- Whether attribute 'Result is mentioned in a non-trivial postcondition
- -- or contract-cases.
+ L1 := S1'Last;
+ while S1 (L1) in '0' .. '9' loop
+ L1 := L1 - 1;
+ end loop;
- No_Warning_On_Some_Postcondition : Boolean := False;
- -- Whether there exists a non-trivial postcondition or contract-cases
- -- without a corresponding warning.
+ L2 := S2'Last;
+ while S2 (L2) in '0' .. '9' loop
+ L2 := L2 - 1;
+ end loop;
- Post_State_Mentioned : Boolean := False;
- -- Whether some expression mentioned in a postcondition or
- -- contract-cases can have a different value in the post-state than
- -- in the pre-state.
+ -- If non-numeric parts non-equal, do straight compare
- function Check_Attr_Result (N : Node_Id) return Traverse_Result;
- -- Check if N is a reference to the attribute 'Result, and if so set
- -- Attribute_Result_Mentioned and return Abandon. Otherwise return OK.
+ if S1 (S1'First .. L1) /= S2 (S2'First .. L2) then
+ return S1 > S2;
- function Check_Post_State (N : Node_Id) return Traverse_Result;
- -- Check whether the value of evaluating N can be different in the
- -- post-state, compared to the same evaluation in the pre-state, and
- -- if so set Post_State_Mentioned and return Abandon. Return Skip on
- -- reference to attribute 'Old, in order to ignore its prefix, which
- -- is precisely evaluated in the pre-state. Otherwise return OK.
+ -- If non-numeric parts equal, compare suffixed numeric parts. Note
+ -- that a missing suffix is treated as numeric zero in this test.
- function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean;
- -- Return True if node N is trivially "True" or "False", and it comes
- -- from source. In particular, nodes that are statically known "True" or
- -- "False" by the compiler but not written as such in source code are
- -- not considered as trivial.
+ else
+ N1 := 0;
+ while L1 < S1'Last loop
+ L1 := L1 + 1;
+ N1 := N1 * 10 + Character'Pos (S1 (L1)) - Character'Pos ('0');
+ end loop;
- procedure Process_Contract_Cases (Spec : Node_Id);
- -- This processes the Spec_CTC_List from Spec, processing any contract
- -- case from the list. The caller has checked that Spec_CTC_List is
- -- non-Empty.
+ N2 := 0;
+ while L2 < S2'Last loop
+ L2 := L2 + 1;
+ N2 := N2 * 10 + Character'Pos (S2 (L2)) - Character'Pos ('0');
+ end loop;
- procedure Process_Post_Conditions (Spec : Node_Id; Class : Boolean);
- -- This processes the Spec_PPC_List from Spec, processing any
- -- postcondition from the list. If Class is True, then only
- -- postconditions marked with Class_Present are considered. The
- -- caller has checked that Spec_PPC_List is non-Empty.
+ return N1 > N2;
+ end if;
+ end Subprogram_Name_Greater;
- function Find_Attribute_Result is new Traverse_Func (Check_Attr_Result);
+ -- Start of processing for Check_Subprogram_Order
- function Find_Post_State is new Traverse_Func (Check_Post_State);
+ begin
+ -- Check body in alpha order if this is option
- -----------------------
- -- Check_Attr_Result --
- -----------------------
+ if Style_Check
+ and then Style_Check_Order_Subprograms
+ and then Nkind (N) = N_Subprogram_Body
+ and then Comes_From_Source (N)
+ and then In_Extended_Main_Source_Unit (N)
+ then
+ declare
+ LSN : String_Ptr
+ renames Scope_Stack.Table
+ (Scope_Stack.Last).Last_Subprogram_Name;
- function Check_Attr_Result (N : Node_Id) return Traverse_Result is
- begin
- if Nkind (N) = N_Attribute_Reference
- and then Get_Attribute_Id (Attribute_Name (N)) = Attribute_Result
- then
- Attribute_Result_Mentioned := True;
- return Abandon;
- else
- return OK;
- end if;
- end Check_Attr_Result;
+ Body_Id : constant Entity_Id :=
+ Defining_Entity (Specification (N));
- ----------------------
- -- Check_Post_State --
- ----------------------
+ begin
+ Get_Decoded_Name_String (Chars (Body_Id));
- function Check_Post_State (N : Node_Id) return Traverse_Result is
- Found : Boolean := False;
+ if LSN /= null then
+ if Subprogram_Name_Greater
+ (LSN.all, Name_Buffer (1 .. Name_Len))
+ then
+ Style.Subprogram_Not_In_Alpha_Order (Body_Id);
+ end if;
- begin
- case Nkind (N) is
- when N_Function_Call |
- N_Explicit_Dereference =>
- Found := True;
+ Free (LSN);
+ end if;
- when N_Identifier |
- N_Expanded_Name =>
+ LSN := new String'(Name_Buffer (1 .. Name_Len));
+ end;
+ end if;
+ end Check_Subprogram_Order;
- declare
- E : constant Entity_Id := Entity (N);
-
- begin
- -- ???Quantified expressions get analyzed later, so E can
- -- be empty at this point. In this case, we suppress the
- -- warning, just in case E is assignable. It seems better to
- -- have false negatives than false positives. At some point,
- -- we should make the warning more accurate, either by
- -- analyzing quantified expressions earlier, or moving
- -- this processing later.
-
- if No (E)
- or else
- (Is_Entity_Name (N)
- and then Ekind (E) in Assignable_Kind)
- then
- Found := True;
- end if;
- end;
-
- when N_Attribute_Reference =>
- case Get_Attribute_Id (Attribute_Name (N)) is
- when Attribute_Old =>
- return Skip;
- when Attribute_Result =>
- Found := True;
- when others =>
- null;
- end case;
-
- when others =>
- null;
- end case;
-
- if Found then
- Post_State_Mentioned := True;
- return Abandon;
- else
- return OK;
- end if;
- end Check_Post_State;
-
- --------------------------------
- -- Is_Trivial_Post_Or_Ensures --
- --------------------------------
-
- function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean is
- begin
- return Is_Entity_Name (N)
- and then (Entity (N) = Standard_True
- or else
- Entity (N) = Standard_False)
- and then Comes_From_Source (N);
- end Is_Trivial_Post_Or_Ensures;
-
- ----------------------------
- -- Process_Contract_Cases --
- ----------------------------
-
- procedure Process_Contract_Cases (Spec : Node_Id) is
- Prag : Node_Id;
- Aggr : Node_Id;
- Conseq : Node_Id;
- Post_Case : Node_Id;
-
- Ignored : Traverse_Final_Result;
- pragma Unreferenced (Ignored);
-
- begin
- Prag := Spec_CTC_List (Contract (Spec));
- loop
- if Pragma_Name (Prag) = Name_Contract_Cases then
- Aggr :=
- Expression (First (Pragma_Argument_Associations (Prag)));
-
- Post_Case := First (Component_Associations (Aggr));
- while Present (Post_Case) loop
- Conseq := Expression (Post_Case);
-
- -- Ignore trivial contract-cases when consequence is "True"
- -- or "False".
-
- if not Is_Trivial_Post_Or_Ensures (Conseq) then
-
- Last_Contract_Cases := Prag;
-
- -- For functions, look for presence of 'Result in
- -- consequence expression.
-
- if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
- Ignored := Find_Attribute_Result (Conseq);
- end if;
-
- -- For each individual case, look for presence of an
- -- expression that could be evaluated differently in
- -- post-state.
-
- Post_State_Mentioned := False;
- Ignored := Find_Post_State (Conseq);
-
- if Post_State_Mentioned then
- No_Warning_On_Some_Postcondition := True;
- else
- Error_Msg_N
- ("contract case refers only to pre-state?T?",
- Conseq);
- end if;
- end if;
-
- Next (Post_Case);
- end loop;
- end if;
-
- Prag := Next_Pragma (Prag);
- exit when No (Prag);
- end loop;
- end Process_Contract_Cases;
-
- -----------------------------
- -- Process_Post_Conditions --
- -----------------------------
-
- procedure Process_Post_Conditions
- (Spec : Node_Id;
- Class : Boolean)
- is
- Prag : Node_Id;
- Arg : Node_Id;
- Ignored : Traverse_Final_Result;
- pragma Unreferenced (Ignored);
-
- begin
- Prag := Spec_PPC_List (Contract (Spec));
- loop
- Arg := First (Pragma_Argument_Associations (Prag));
-
- -- Ignore trivial postcondition of "True" or "False"
-
- if Pragma_Name (Prag) = Name_Postcondition
- and then not Is_Trivial_Post_Or_Ensures (Expression (Arg))
- then
- -- Since pre- and post-conditions are listed in reverse order,
- -- the first postcondition in the list is last in the source.
-
- if not Class and then No (Last_Postcondition) then
- Last_Postcondition := Prag;
- end if;
-
- -- For functions, look for presence of 'Result in postcondition
-
- if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
- Ignored := Find_Attribute_Result (Arg);
- end if;
-
- -- For each individual non-inherited postcondition, look
- -- for presence of an expression that could be evaluated
- -- differently in post-state.
-
- if not Class then
- Post_State_Mentioned := False;
- Ignored := Find_Post_State (Arg);
-
- if Post_State_Mentioned then
- No_Warning_On_Some_Postcondition := True;
- else
- Error_Msg_N
- ("postcondition refers only to pre-state?T?", Prag);
- end if;
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- exit when No (Prag);
- end loop;
- end Process_Post_Conditions;
-
- -- Start of processing for Check_Subprogram_Contract
-
- begin
- if not Warn_On_Suspicious_Contract then
- return;
- end if;
-
- -- Process spec postconditions
-
- if Present (Spec_PPC_List (Contract (Spec_Id))) then
- Process_Post_Conditions (Spec_Id, Class => False);
- end if;
-
- -- Process inherited postconditions
-
- -- Code is currently commented out as, in some cases, it causes crashes
- -- because Direct_Primitive_Operations is not available for a private
- -- type. This may cause more warnings to be issued than necessary. ???
-
--- for J in Inherited'Range loop
--- if Present (Spec_PPC_List (Contract (Inherited (J)))) then
--- Process_Post_Conditions (Inherited (J), Class => True);
--- end if;
--- end loop;
-
- -- Process contract cases
-
- if Present (Spec_CTC_List (Contract (Spec_Id))) then
- Process_Contract_Cases (Spec_Id);
- end if;
-
- -- Issue warning for functions whose postcondition does not mention
- -- 'Result after all postconditions have been processed, and provided
- -- all postconditions do not already get a warning that they only refer
- -- to pre-state.
-
- if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
- and then (Present (Last_Postcondition)
- or else Present (Last_Contract_Cases))
- and then not Attribute_Result_Mentioned
- and then No_Warning_On_Some_Postcondition
- then
- if Present (Last_Postcondition) then
- if Present (Last_Contract_Cases) then
- Error_Msg_N
- ("neither function postcondition nor "
- & "contract cases mention result?T?", Last_Postcondition);
-
- else
- Error_Msg_N
- ("function postcondition does not mention result?T?",
- Last_Postcondition);
- end if;
- else
- Error_Msg_N
- ("contract cases do not mention result?T?", Last_Contract_Cases);
- end if;
- end if;
- end Check_Subprogram_Contract;
-
- ----------------------------
- -- Check_Subprogram_Order --
- ----------------------------
-
- procedure Check_Subprogram_Order (N : Node_Id) is
-
- function Subprogram_Name_Greater (S1, S2 : String) return Boolean;
- -- This is used to check if S1 > S2 in the sense required by this test,
- -- for example nameab < namec, but name2 < name10.
-
- -----------------------------
- -- Subprogram_Name_Greater --
- -----------------------------
-
- function Subprogram_Name_Greater (S1, S2 : String) return Boolean is
- L1, L2 : Positive;
- N1, N2 : Natural;
-
- begin
- -- Deal with special case where names are identical except for a
- -- numerical suffix. These are handled specially, taking the numeric
- -- ordering from the suffix into account.
-
- L1 := S1'Last;
- while S1 (L1) in '0' .. '9' loop
- L1 := L1 - 1;
- end loop;
-
- L2 := S2'Last;
- while S2 (L2) in '0' .. '9' loop
- L2 := L2 - 1;
- end loop;
-
- -- If non-numeric parts non-equal, do straight compare
-
- if S1 (S1'First .. L1) /= S2 (S2'First .. L2) then
- return S1 > S2;
-
- -- If non-numeric parts equal, compare suffixed numeric parts. Note
- -- that a missing suffix is treated as numeric zero in this test.
-
- else
- N1 := 0;
- while L1 < S1'Last loop
- L1 := L1 + 1;
- N1 := N1 * 10 + Character'Pos (S1 (L1)) - Character'Pos ('0');
- end loop;
-
- N2 := 0;
- while L2 < S2'Last loop
- L2 := L2 + 1;
- N2 := N2 * 10 + Character'Pos (S2 (L2)) - Character'Pos ('0');
- end loop;
-
- return N1 > N2;
- end if;
- end Subprogram_Name_Greater;
-
- -- Start of processing for Check_Subprogram_Order
-
- begin
- -- Check body in alpha order if this is option
-
- if Style_Check
- and then Style_Check_Order_Subprograms
- and then Nkind (N) = N_Subprogram_Body
- and then Comes_From_Source (N)
- and then In_Extended_Main_Source_Unit (N)
- then
- declare
- LSN : String_Ptr
- renames Scope_Stack.Table
- (Scope_Stack.Last).Last_Subprogram_Name;
-
- Body_Id : constant Entity_Id :=
- Defining_Entity (Specification (N));
-
- begin
- Get_Decoded_Name_String (Chars (Body_Id));
-
- if LSN /= null then
- if Subprogram_Name_Greater
- (LSN.all, Name_Buffer (1 .. Name_Len))
- then
- Style.Subprogram_Not_In_Alpha_Order (Body_Id);
- end if;
-
- Free (LSN);
- end if;
-
- LSN := new String'(Name_Buffer (1 .. Name_Len));
- end;
- end if;
- end Check_Subprogram_Order;
-
- ------------------------------
- -- Check_Subtype_Conformant --
- ------------------------------
+ ------------------------------
+ -- Check_Subtype_Conformant --
+ ------------------------------
procedure Check_Subtype_Conformant
(New_Id : Entity_Id;
or else Scope (T1) /= Scope (T2);
-- If T2 is a generic actual type it is declared as the subtype of
- -- the actual. If that actual is itself a subtype we need to use
- -- its own base type to check for compatibility.
+ -- the actual. If that actual is itself a subtype we need to use its
+ -- own base type to check for compatibility.
elsif Ekind (BT2) = Ekind (T2) and then BT1 = Base_Type (BT2) then
return True;
-- access-to-class-wide type in a formal. Both entities designate the
-- same type.
- if From_With_Type (T1) and then T2 = Available_View (T1) then
+ if From_Limited_With (T1) and then T2 = Available_View (T1) then
return True;
- elsif From_With_Type (T2) and then T1 = Available_View (T2) then
+ elsif From_Limited_With (T2) and then T1 = Available_View (T2) then
return True;
- elsif From_With_Type (T1)
- and then From_With_Type (T2)
+ elsif From_Limited_With (T1)
+ and then From_Limited_With (T2)
and then Available_View (T1) = Available_View (T2)
then
return True;
end if;
-- Ada 2005 (AI-254): Anonymous access-to-subprogram types must be
- -- treated recursively because they carry a signature.
+ -- treated recursively because they carry a signature. As far as
+ -- conformance is concerned, convention plays no role, and either
+ -- or both could be access to protected subprograms.
Are_Anonymous_Access_To_Subprogram_Types :=
- Ekind (Type_1) = Ekind (Type_2)
+ Ekind_In (Type_1, E_Anonymous_Access_Subprogram_Type,
+ E_Anonymous_Access_Protected_Subprogram_Type)
and then
- Ekind_In (Type_1, E_Anonymous_Access_Subprogram_Type,
- E_Anonymous_Access_Protected_Subprogram_Type);
+ Ekind_In (Type_2, E_Anonymous_Access_Subprogram_Type,
+ E_Anonymous_Access_Protected_Subprogram_Type);
-- Test anonymous access type case. For this case, static subtype
-- matching is required for mode conformance (RM 6.3.1(15)). We check
-- on discriminants and others do not (and requiring the extra
-- formal would introduce distributed overhead).
+ -- If the type does not have a completion yet, treat as prior to
+ -- Ada 2012 for consistency.
+
if Has_Discriminants (Formal_Type)
and then not Is_Constrained (Formal_Type)
and then not Is_Indefinite_Subtype (Formal_Type)
and then (Ada_Version < Ada_2012
- or else
- not (Is_Tagged_Type (Underlying_Type (Formal_Type))
- and then Is_Limited_Type (Formal_Type)))
+ or else No (Underlying_Type (Formal_Type))
+ or else not
+ (Is_Limited_Type (Formal_Type)
+ and then
+ (Is_Tagged_Type
+ (Underlying_Type (Formal_Type)))))
then
Set_Extra_Constrained
(Formal, Add_Extra_Formal (Formal, Standard_Boolean, E, "O"));
-- the designated type comes from the limited view (for back-end
-- purposes).
- Set_From_With_Type (Formal_Typ, From_With_Type (Result_Subt));
+ Set_From_Limited_With
+ (Formal_Typ, From_Limited_With (Result_Subt));
Layout_Type (Formal_Typ);
Obj_Decl : Node_Id;
begin
- if Nkind (Decl) = N_Subprogram_Declaration
- and then Is_Record_Type (Typ)
- and then not Is_Tagged_Type (Typ)
+ -- This check applies only if we have a subprogram declaration with a
+ -- non-tagged record type.
+
+ if Nkind (Decl) /= N_Subprogram_Declaration
+ or else not Is_Record_Type (Typ)
+ or else Is_Tagged_Type (Typ)
then
- -- If the type is not declared in a package, or if we are in the
- -- body of the package or in some other scope, the new operation is
- -- not primitive, and therefore legal, though suspicious. If the
- -- type is a generic actual (sub)type, the operation is not primitive
- -- either because the base type is declared elsewhere.
-
- if Is_Frozen (Typ) then
- if Ekind (Scope (Typ)) /= E_Package
- or else Scope (Typ) /= Current_Scope
- then
- null;
+ return;
+ end if;
- elsif Is_Generic_Actual_Type (Typ) then
- null;
+ -- In Ada 2012 case, we will output errors or warnings depending on
+ -- the setting of debug flag -gnatd.E.
+
+ if Ada_Version >= Ada_2012 then
+ Error_Msg_Warn := Debug_Flag_Dot_EE;
+
+ -- In earlier versions of Ada, nothing to do unless we are warning on
+ -- Ada 2012 incompatibilities (Warn_On_Ada_2012_Incompatibility set).
+
+ else
+ if not Warn_On_Ada_2012_Compatibility then
+ return;
+ end if;
+ end if;
+
+ -- Cases where the type has already been frozen
+
+ if Is_Frozen (Typ) then
+
+ -- If the type is not declared in a package, or if we are in the body
+ -- of the package or in some other scope, the new operation is not
+ -- primitive, and therefore legal, though suspicious. Should we
+ -- generate a warning in this case ???
+
+ if Ekind (Scope (Typ)) /= E_Package
+ or else Scope (Typ) /= Current_Scope
+ then
+ return;
+
+ -- If the type is a generic actual (sub)type, the operation is not
+ -- primitive either because the base type is declared elsewhere.
+
+ elsif Is_Generic_Actual_Type (Typ) then
+ return;
+
+ -- Here we have a definite error of declaration after freezing
- elsif In_Package_Body (Scope (Typ)) then
+ else
+ if Ada_Version >= Ada_2012 then
Error_Msg_NE
- ("equality operator must be declared "
- & "before type& is frozen", Eq_Op, Typ);
- Error_Msg_N
- ("\move declaration to package spec", Eq_Op);
+ ("equality operator must be declared before type& is "
+ & "frozen (RM 4.5.2 (9.8)) (Ada 2012)<<", Eq_Op, Typ);
+
+ -- In Ada 2012 mode with error turned to warning, output one
+ -- more warning to warn that the equality operation may not
+ -- compose. This is the consequence of ignoring the error.
+
+ if Error_Msg_Warn then
+ Error_Msg_N ("\equality operation may not compose??", Eq_Op);
+ end if;
else
Error_Msg_NE
- ("equality operator must be declared "
- & "before type& is frozen", Eq_Op, Typ);
+ ("equality operator must be declared before type& is "
+ & "frozen (RM 4.5.2 (9.8)) (Ada 2012)?y?", Eq_Op, Typ);
+ end if;
+
+ -- If we are in the package body, we could just move the
+ -- declaration to the package spec, so add a message saying that.
+
+ if In_Package_Body (Scope (Typ)) then
+ if Ada_Version >= Ada_2012 then
+ Error_Msg_N
+ ("\move declaration to package spec<<", Eq_Op);
+ else
+ Error_Msg_N
+ ("\move declaration to package spec (Ada 2012)?y?", Eq_Op);
+ end if;
+ -- Otherwise try to find the freezing point
+
+ else
Obj_Decl := Next (Parent (Typ));
while Present (Obj_Decl) and then Obj_Decl /= Decl loop
if Nkind (Obj_Decl) = N_Object_Declaration
and then Etype (Defining_Identifier (Obj_Decl)) = Typ
then
- Error_Msg_NE
- ("type& is frozen by declaration??", Obj_Decl, Typ);
- Error_Msg_N
- ("\an equality operator cannot be declared after this "
- & "point (RM 4.5.2 (9.8)) (Ada 2012))??", Obj_Decl);
+ -- Freezing point, output warnings
+
+ if Ada_Version >= Ada_2012 then
+ Error_Msg_NE
+ ("type& is frozen by declaration??", Obj_Decl, Typ);
+ Error_Msg_N
+ ("\an equality operator cannot be declared after "
+ & "this point??",
+ Obj_Decl);
+ else
+ Error_Msg_NE
+ ("type& is frozen by declaration (Ada 2012)?y?",
+ Obj_Decl, Typ);
+ Error_Msg_N
+ ("\an equality operator cannot be declared after "
+ & "this point (Ada 2012)?y?",
+ Obj_Decl);
+ end if;
+
exit;
end if;
Next (Obj_Decl);
end loop;
end if;
+ end if;
- elsif not In_Same_List (Parent (Typ), Decl)
- and then not Is_Limited_Type (Typ)
- then
+ -- Here if type is not frozen yet. It is illegal to have a primitive
+ -- equality declared in the private part if the type is visible.
- -- This makes it illegal to have a primitive equality declared in
- -- the private part if the type is visible.
+ elsif not In_Same_List (Parent (Typ), Decl)
+ and then not Is_Limited_Type (Typ)
+ then
+ -- Shouldn't we give an RM reference here???
- Error_Msg_N ("equality operator appears too late", Eq_Op);
- end if;
+ if Ada_Version >= Ada_2012 then
+ Error_Msg_N
+ ("equality operator appears too late<<", Eq_Op);
+ else
+ Error_Msg_N
+ ("equality operator appears too late (Ada 2012)?y?", Eq_Op);
+ end if;
+
+ -- No error detected
+
+ else
+ return;
end if;
end Check_Untagged_Equality;
function Different_Generic_Profile (E : Entity_Id) return Boolean is
F1, F2 : Entity_Id;
+ function Same_Generic_Actual (T1, T2 : Entity_Id) return Boolean;
+ -- Check that the types of corresponding formals have the same
+ -- generic actual if any. We have to account for subtypes of a
+ -- generic formal, declared between a spec and a body, which may
+ -- appear distinct in an instance but matched in the generic.
+
+ -------------------------
+ -- Same_Generic_Actual --
+ -------------------------
+
+ function Same_Generic_Actual (T1, T2 : Entity_Id) return Boolean is
+ begin
+ return Is_Generic_Actual_Type (T1) = Is_Generic_Actual_Type (T2)
+ or else
+ (Present (Parent (T1))
+ and then Comes_From_Source (Parent (T1))
+ and then Nkind (Parent (T1)) = N_Subtype_Declaration
+ and then Is_Entity_Name (Subtype_Indication (Parent (T1)))
+ and then Entity (Subtype_Indication (Parent (T1))) = T2);
+ end Same_Generic_Actual;
+
+ -- Start of processing for Different_Generic_Profile
+
begin
- if Ekind (E) = E_Function
- and then Is_Generic_Actual_Type (Etype (E)) /=
- Is_Generic_Actual_Type (Etype (Designator))
+ if not In_Instance then
+ return False;
+
+ elsif Ekind (E) = E_Function
+ and then not Same_Generic_Actual (Etype (E), Etype (Designator))
then
return True;
end if;
F1 := First_Formal (Designator);
F2 := First_Formal (E);
while Present (F1) loop
- if Is_Generic_Actual_Type (Etype (F1)) /=
- Is_Generic_Actual_Type (Etype (F2))
- then
+ if not Same_Generic_Actual (Etype (F1), Etype (F2)) then
return True;
end if;
-- If E is an internal function with a controlling result that
-- was created for an operation inherited by a null extension,
-- it may be overridden by a body without a previous spec (one
- -- more reason why these should be shunned). In that case
+ -- more reason why these should be shunned). In that case we
-- remove the generated body if present, because the current
-- one is the explicit overriding.
end if;
-- Compare two lists, skipping rewrite insertions (we want to compare
- -- the original trees, not the expanded versions!)
+ -- the original trees, not the expanded versions).
loop
if Is_Rewrite_Insertion (N1) then
begin
-- Non-conformant 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!
+ -- parentheses, they will be treated with the respect they deserve.
if Paren_Count (E1) /= Paren_Count (E2) then
return False;
-- All other node types cannot appear in this context. Strictly
-- we should raise a fatal internal error. Instead we just ignore
-- the nodes. This means that if anyone makes a mistake in the
- -- expander and mucks an expression tree irretrievably, the
- -- result will be a failure to detect a (probably very obscure)
- -- case of non-conformance, which is better than bombing on some
+ -- expander and mucks an expression tree irretrievably, the result
+ -- will be a failure to detect a (probably very obscure) case
+ -- of non-conformance, which is better than bombing on some
-- case where two expressions do in fact conform.
when others =>
Iface_Prim : Entity_Id;
Prim : Entity_Id) return Boolean
is
- Iface : constant Entity_Id := Find_Dispatching_Type (Iface_Prim);
+ -- The operation may in fact be an inherited (implicit) operation
+ -- rather than the original interface primitive, so retrieve the
+ -- ultimate ancestor.
+
+ Iface : constant Entity_Id :=
+ Find_Dispatching_Type (Ultimate_Alias (Iface_Prim));
Typ : constant Entity_Id := Find_Dispatching_Type (Prim);
function Controlling_Formal (Prim : Entity_Id) return Entity_Id;
------------------------
function Controlling_Formal (Prim : Entity_Id) return Entity_Id is
- E : Entity_Id := First_Entity (Prim);
+ E : Entity_Id;
begin
+ E := First_Entity (Prim);
while Present (E) loop
if Is_Formal (E) and then Is_Controlling_Formal (E) then
return E;
-- The mode of the controlling formals must match
elsif Present (Iface_Ctrl_F)
- and then Present (Prim_Ctrl_F)
- and then Ekind (Iface_Ctrl_F) /= Ekind (Prim_Ctrl_F)
+ and then Present (Prim_Ctrl_F)
+ and then Ekind (Iface_Ctrl_F) /= Ekind (Prim_Ctrl_F)
then
return False;
return Type_Conformant
(Iface_Prim, Prim, Skip_Controlling_Formals => True);
- -- Case of a function returning an interface, or an access to one.
- -- Check that the return types correspond.
+ -- Case of a function returning an interface, or an access to one. Check
+ -- that the return types correspond.
elsif Implements_Interface (Typ, Iface) then
if (Ekind (Etype (Prim)) = E_Anonymous_Access_Type)
return False;
else
return
- Type_Conformant (Prim, Iface_Prim,
+ Type_Conformant (Prim, Ultimate_Alias (Iface_Prim),
Skip_Controlling_Formals => True);
end if;
Next_Elmt (Prim_Elt);
end loop;
- -- If no match found, then the new subprogram does not
- -- override in the generic (nor in the instance).
+ -- If no match found, then the new subprogram does not override
+ -- in the generic (nor in the instance).
-- If the type in question is not abstract, and the subprogram
-- is, this will be an error if the new operation is in the
begin
for J in Inherited'Range loop
- P := Spec_PPC_List (Contract (Inherited (J)));
+ P := Pre_Post_Conditions (Contract (Inherited (J)));
while Present (P) loop
Error_Msg_Sloc := Sloc (P);
Make_Parameter_Specification (Loc,
Defining_Identifier => A,
Parameter_Type =>
- New_Reference_To (Etype (First_Formal (S)),
+ New_Occurrence_Of (Etype (First_Formal (S)),
Sloc (Etype (First_Formal (S))))),
Make_Parameter_Specification (Loc,
Defining_Identifier => B,
Parameter_Type =>
- New_Reference_To (Etype (Next_Formal (First_Formal (S))),
+ New_Occurrence_Of (Etype (Next_Formal (First_Formal (S))),
Sloc (Etype (Next_Formal (First_Formal (S)))))));
Decl :=
Defining_Unit_Name => Op_Name,
Parameter_Specifications => Formals,
Result_Definition =>
- New_Reference_To (Standard_Boolean, Loc)));
+ New_Occurrence_Of (Standard_Boolean, Loc)));
-- Insert inequality right after equality if it is explicit or after
-- the derived type when implicit. These entities are created only
- -- for visibility purposes, and eventually replaced in the course of
- -- expansion, so they do not need to be attached to the tree and seen
- -- by the back-end. Keeping them internal also avoids spurious
+ -- for visibility purposes, and eventually replaced in the course
+ -- of expansion, so they do not need to be attached to the tree and
+ -- seen by the back-end. Keeping them internal also avoids spurious
-- freezing problems. The declaration is inserted in the tree for
-- analysis, and removed afterwards. If the equality operator comes
-- from an explicit declaration, attach the inequality immediately
New_E : Entity_Id) return Boolean;
-- Check whether new subprogram and old subprogram are both inherited
-- from subprograms that have distinct dispatch table entries. This can
- -- occur with derivations from instances with accidental homonyms.
- -- The function is conservative given that the converse is only true
- -- within instances that contain accidental overloadings.
+ -- occur with derivations from instances with accidental homonyms. The
+ -- function is conservative given that the converse is only true within
+ -- instances that contain accidental overloadings.
------------------------------------
-- Check_For_Primitive_Subprogram --
and then In_Private_Part (Current_Scope)
then
Priv_Decls :=
- Private_Declarations
- (Specification (Unit_Declaration_Node (Current_Scope)));
+ Private_Declarations (Package_Specification (Current_Scope));
return In_Package_Body (Current_Scope)
or else
Check_Dispatching_Operation (S, Empty);
Check_For_Primitive_Subprogram (Is_Primitive_Subp);
- -- If subprogram has an explicit declaration, check whether it
- -- has an overriding indicator.
+ -- If subprogram has an explicit declaration, check whether it has an
+ -- overriding indicator.
if Comes_From_Source (S) then
Check_Synchronized_Overriding (S, Overridden_Subp);
if Scope (E) /= Current_Scope then
null;
- -- Ada 2012 (AI05-0165): For internally generated bodies of
- -- null procedures locate the internally generated spec. We
- -- enforce mode conformance since a tagged type may inherit
- -- from interfaces several null primitives which differ only
- -- in the mode of the formals.
+ -- A function can overload the name of an abstract state. The
+ -- state can be viewed as a function with a profile that cannot
+ -- be matched by anything.
+
+ elsif Ekind (S) = E_Function
+ and then Ekind (E) = E_Abstract_State
+ then
+ Enter_Overloaded_Entity (S);
+ return;
+
+ -- Ada 2012 (AI05-0165): For internally generated bodies of null
+ -- procedures locate the internally generated spec. We enforce
+ -- mode conformance since a tagged type may inherit from
+ -- interfaces several null primitives which differ only in
+ -- the mode of the formals.
elsif not Comes_From_Source (S)
and then Is_Null_Procedure (S)
and then not Is_Dispatching_Operation (S)
then
Make_Inequality_Operator (S);
-
- if Ada_Version >= Ada_2012 then
- Check_Untagged_Equality (S);
- end if;
+ Check_Untagged_Equality (S);
end if;
end New_Overloaded_Entity;
First_Out_Param : Entity_Id := Empty;
-- Used for setting Is_Only_Out_Parameter
- function Designates_From_With_Type (Typ : Entity_Id) return Boolean;
+ function Designates_From_Limited_With (Typ : Entity_Id) return Boolean;
-- Determine whether an access type designates a type coming from a
-- limited view.
-- default has the type of the formal, so we must also check explicitly
-- for an access attribute.
- -------------------------------
- -- Designates_From_With_Type --
- -------------------------------
+ ----------------------------------
+ -- Designates_From_Limited_With --
+ ----------------------------------
- function Designates_From_With_Type (Typ : Entity_Id) return Boolean is
+ function Designates_From_Limited_With (Typ : Entity_Id) return Boolean is
Desig : Entity_Id := Typ;
begin
end if;
return
- Ekind (Desig) = E_Incomplete_Type and then From_With_Type (Desig);
- end Designates_From_With_Type;
+ Ekind (Desig) = E_Incomplete_Type
+ and then From_Limited_With (Desig);
+ end Designates_From_Limited_With;
---------------------------
-- Is_Class_Wide_Default --
-- Ada 2012: tagged incomplete types are allowed as generic
-- formal types. They do not introduce dependencies and the
-- corresponding generic subprogram does not have a delayed
- -- freeze, because it does not need a freeze node.
-
- if Is_Tagged_Type (Formal_Type) then
+ -- freeze, because it does not need a freeze node. However,
+ -- it is still the case that untagged incomplete types cannot
+ -- be Taft-amendment types and must be completed in private
+ -- part, so the subprogram must appear in the list of private
+ -- dependents of the type.
+
+ if Is_Tagged_Type (Formal_Type)
+ or else Ada_Version >= Ada_2012
+ then
if Ekind (Scope (Current_Scope)) = E_Package
- and then not From_With_Type (Formal_Type)
+ and then not From_Limited_With (Formal_Type)
and then not Is_Generic_Type (Formal_Type)
and then not Is_Class_Wide_Type (Formal_Type)
then
-- is also class-wide.
if Ekind (Formal_Type) = E_Anonymous_Access_Type
- and then not Designates_From_With_Type (Formal_Type)
+ and then not Designates_From_Limited_With (Formal_Type)
and then Is_Class_Wide_Default (Default)
and then not Is_Class_Wide_Type (Designated_Type (Formal_Type))
then
Null_Exclusion_Static_Checks (Param_Spec);
end if;
+ -- The following checks are relevant when SPARK_Mode is on as these
+ -- are not standard Ada legality rules.
+
+ if SPARK_Mode = On then
+ if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then
+
+ -- A function cannot have a parameter of mode IN OUT or OUT
+ -- (SPARK RM 6.1).
+
+ if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+ Error_Msg_N
+ ("function cannot have parameter of mode `OUT` or "
+ & "`IN OUT`", Formal);
+
+ -- A function cannot have a volatile formal parameter
+ -- (SPARK RM 7.1.3(10)).
+
+ elsif Is_SPARK_Volatile (Formal) then
+ Error_Msg_N
+ ("function cannot have a volatile formal parameter",
+ Formal);
+ end if;
+
+ -- A procedure cannot have a formal parameter of mode IN because
+ -- it behaves as a constant (SPARK RM 7.1.3(6)).
+
+ elsif Ekind (Scope (Formal)) = E_Procedure
+ and then Ekind (Formal) = E_In_Parameter
+ and then Is_SPARK_Volatile (Formal)
+ then
+ Error_Msg_N
+ ("formal parameter of mode `IN` cannot be volatile", Formal);
+ end if;
+ end if;
+
<<Continue>>
Next (Param_Spec);
end loop;
if Convention (Formal_Type) = Convention_Ada_Pass_By_Copy then
Error_Msg_N
- ("cannot pass aliased parameter & by copy?", Formal);
+ ("cannot pass aliased parameter & by copy??", Formal);
end if;
-- Force mechanism if type has Convention Ada_Pass_By_Ref/Copy
end if;
end Process_Formals;
- ------------------
- -- Process_PPCs --
- ------------------
-
- procedure Process_PPCs
- (N : Node_Id;
- Spec_Id : Entity_Id;
- Body_Id : Entity_Id)
- is
- Loc : constant Source_Ptr := Sloc (N);
- Prag : Node_Id;
- Parms : List_Id;
-
- Designator : Entity_Id;
- -- Subprogram designator, set from Spec_Id if present, else Body_Id
-
- Precond : Node_Id := Empty;
- -- Set non-Empty if we prepend precondition to the declarations. This
- -- is used to hook up inherited preconditions (adding the condition
- -- expression with OR ELSE, and adding the message).
-
- Inherited_Precond : Node_Id;
- -- Precondition inherited from parent subprogram
-
- Inherited : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
- -- List of subprograms inherited by this subprogram
-
- Plist : List_Id := No_List;
- -- List of generated postconditions
-
- procedure Check_Access_Invariants (E : Entity_Id);
- -- If the subprogram returns an access to a type with invariants, or
- -- has access parameters whose designated type has an invariant, then
- -- under the same visibility conditions as for other invariant checks,
- -- the type invariant must be applied to the returned value.
-
- procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id);
- -- Given pragma Contract_Cases CCs, create the circuitry needed to
- -- evaluate case guards and trigger consequence expressions. Subp_Id
- -- denotes the related subprogram.
-
- function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
- -- Prag contains an analyzed precondition or postcondition pragma. This
- -- function copies the pragma, changes it to the corresponding Check
- -- pragma and returns the Check pragma as the result. If Pspec is non-
- -- empty, this is the case of inheriting a PPC, where we must change
- -- references to parameters of the inherited subprogram to point to the
- -- corresponding parameters of the current subprogram.
-
- procedure Insert_After_Last_Declaration (Nod : Node_Id);
- -- Insert node Nod after the last declaration of the context
-
- function Invariants_Or_Predicates_Present return Boolean;
- -- Determines if any invariants or predicates are present for any OUT
- -- or IN OUT parameters of the subprogram, or (for a function) if the
- -- return value has an invariant.
-
- function Is_Public_Subprogram_For (T : Entity_Id) return Boolean;
- -- T is the entity for a private type for which invariants are defined.
- -- This function returns True if the procedure corresponding to the
- -- value of Designator is a public procedure from the point of view of
- -- this type (i.e. its spec is in the visible part of the package that
- -- contains the declaration of the private type). A True value means
- -- that an invariant check is required (for an IN OUT parameter, or
- -- the returned value of a function.
-
- -----------------------------
- -- Check_Access_Invariants --
- -----------------------------
-
- procedure Check_Access_Invariants (E : Entity_Id) is
- Call : Node_Id;
- Obj : Node_Id;
- Typ : Entity_Id;
-
- begin
- if Is_Access_Type (Etype (E))
- and then not Is_Access_Constant (Etype (E))
- then
- Typ := Designated_Type (Etype (E));
-
- if Has_Invariants (Typ)
- and then Present (Invariant_Procedure (Typ))
- and then Is_Public_Subprogram_For (Typ)
- then
- Obj :=
- Make_Explicit_Dereference (Loc,
- Prefix => New_Occurrence_Of (E, Loc));
- Set_Etype (Obj, Typ);
-
- Call := Make_Invariant_Call (Obj);
-
- Append_To (Plist,
- Make_If_Statement (Loc,
- Condition =>
- Make_Op_Ne (Loc,
- Left_Opnd => Make_Null (Loc),
- Right_Opnd => New_Occurrence_Of (E, Loc)),
- Then_Statements => New_List (Call)));
- end if;
- end if;
- end Check_Access_Invariants;
-
- ---------------------------
- -- Expand_Contract_Cases --
- ---------------------------
-
- -- Pragma Contract_Cases is expanded in the following manner:
-
- -- subprogram S is
- -- Flag_1 : Boolean := False;
- -- . . .
- -- Flag_N : Boolean := False;
- -- Flag_N+1 : Boolean := False; -- when "others" present
- -- Count : Natural := 0;
-
- -- <preconditions (if any)>
-
- -- if Case_Guard_1 then
- -- Flag_1 := True;
- -- Count := Count + 1;
- -- end if;
- -- . . .
- -- if Case_Guard_N then
- -- Flag_N := True;
- -- Count := Count + 1;
- -- end if;
-
- -- if Count = 0 then
- -- raise Assertion_Error with "contract cases incomplete";
- -- <or>
- -- Flag_N+1 := True; -- when "others" present
-
- -- elsif Count > 1 then
- -- declare
- -- Str0 : constant String :=
- -- "contract cases overlap for subprogram ABC";
- -- Str1 : constant String :=
- -- (if Flag_1 then
- -- Str0 & "case guard at xxx evaluates to True"
- -- else Str0);
- -- StrN : constant String :=
- -- (if Flag_N then
- -- StrN-1 & "case guard at xxx evaluates to True"
- -- else StrN-1);
- -- begin
- -- raise Assertion_Error with StrN;
- -- end;
- -- end if;
-
- -- procedure _Postconditions is
- -- begin
- -- <postconditions (if any)>
-
- -- if Flag_1 and then not Consequence_1 then
- -- raise Assertion_Error with "failed contract case at xxx";
- -- end if;
- -- . . .
- -- if Flag_N[+1] and then not Consequence_N[+1] then
- -- raise Assertion_Error with "failed contract case at xxx";
- -- end if;
- -- end _Postconditions;
- -- begin
- -- . . .
- -- end S;
-
- procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id) is
- Loc : constant Source_Ptr := Sloc (CCs);
-
- procedure Case_Guard_Error
- (Decls : List_Id;
- Flag : Entity_Id;
- Error_Loc : Source_Ptr;
- Msg : in out Entity_Id);
- -- Given a declarative list Decls, status flag Flag, the location of
- -- the error and a string Msg, construct the following check:
- -- Msg : constant String :=
- -- (if Flag then
- -- Msg & "case guard at Error_Loc evaluates to True"
- -- else Msg);
- -- The resulting code is added to Decls
-
- procedure Consequence_Error
- (Checks : in out Node_Id;
- Flag : Entity_Id;
- Conseq : Node_Id);
- -- Given an if statement Checks, status flag Flag and a consequence
- -- Conseq, construct the following check:
- -- [els]if Flag and then not Conseq then
- -- raise Assertion_Error
- -- with "failed contract case at Sloc (Conseq)";
- -- [end if;]
- -- The resulting code is added to Checks
-
- function Declaration_Of (Id : Entity_Id) return Node_Id;
- -- Given the entity Id of a boolean flag, generate:
- -- Id : Boolean := False;
-
- function Increment (Id : Entity_Id) return Node_Id;
- -- Given the entity Id of a numerical variable, generate:
- -- Id := Id + 1;
-
- function Set (Id : Entity_Id) return Node_Id;
- -- Given the entity Id of a boolean variable, generate:
- -- Id := True;
-
- ----------------------
- -- Case_Guard_Error --
- ----------------------
-
- procedure Case_Guard_Error
- (Decls : List_Id;
- Flag : Entity_Id;
- Error_Loc : Source_Ptr;
- Msg : in out Entity_Id)
- is
- New_Line : constant Character := Character'Val (10);
- New_Msg : constant Entity_Id := Make_Temporary (Loc, 'S');
-
- begin
- Start_String;
- Store_String_Char (New_Line);
- Store_String_Chars (" case guard at ");
- Store_String_Chars (Build_Location_String (Error_Loc));
- Store_String_Chars (" evaluates to True");
-
- -- Generate:
- -- New_Msg : constant String :=
- -- (if Flag then
- -- Msg & "case guard at Error_Loc evaluates to True"
- -- else Msg);
-
- Append_To (Decls,
- Make_Object_Declaration (Loc,
- Defining_Identifier => New_Msg,
- Constant_Present => True,
- Object_Definition => New_Reference_To (Standard_String, Loc),
- Expression =>
- Make_If_Expression (Loc,
- Expressions => New_List (
- New_Reference_To (Flag, Loc),
-
- Make_Op_Concat (Loc,
- Left_Opnd => New_Reference_To (Msg, Loc),
- Right_Opnd => Make_String_Literal (Loc, End_String)),
-
- New_Reference_To (Msg, Loc)))));
-
- Msg := New_Msg;
- end Case_Guard_Error;
-
- -----------------------
- -- Consequence_Error --
- -----------------------
-
- procedure Consequence_Error
- (Checks : in out Node_Id;
- Flag : Entity_Id;
- Conseq : Node_Id)
- is
- Cond : Node_Id;
- Error : Node_Id;
-
- begin
- -- Generate:
- -- Flag and then not Conseq
-
- Cond :=
- Make_And_Then (Loc,
- Left_Opnd => New_Reference_To (Flag, Loc),
- Right_Opnd =>
- Make_Op_Not (Loc,
- Right_Opnd => Relocate_Node (Conseq)));
-
- -- Generate:
- -- raise Assertion_Error
- -- with "failed contract case at Sloc (Conseq)";
-
- Start_String;
- Store_String_Chars ("failed contract case at ");
- Store_String_Chars (Build_Location_String (Sloc (Conseq)));
-
- Error :=
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc),
- Parameter_Associations => New_List (
- Make_String_Literal (Loc, End_String)));
-
- if No (Checks) then
- Checks :=
- Make_If_Statement (Loc,
- Condition => Cond,
- Then_Statements => New_List (Error));
-
- else
- if No (Elsif_Parts (Checks)) then
- Set_Elsif_Parts (Checks, New_List);
- end if;
-
- Append_To (Elsif_Parts (Checks),
- Make_Elsif_Part (Loc,
- Condition => Cond,
- Then_Statements => New_List (Error)));
- end if;
- end Consequence_Error;
-
- --------------------
- -- Declaration_Of --
- --------------------
-
- function Declaration_Of (Id : Entity_Id) return Node_Id is
- begin
- return
- Make_Object_Declaration (Loc,
- Defining_Identifier => Id,
- Object_Definition =>
- New_Reference_To (Standard_Boolean, Loc),
- Expression =>
- New_Reference_To (Standard_False, Loc));
- end Declaration_Of;
-
- ---------------
- -- Increment --
- ---------------
-
- function Increment (Id : Entity_Id) return Node_Id is
- begin
- return
- Make_Assignment_Statement (Loc,
- Name => New_Reference_To (Id, Loc),
- Expression =>
- Make_Op_Add (Loc,
- Left_Opnd => New_Reference_To (Id, Loc),
- Right_Opnd => Make_Integer_Literal (Loc, 1)));
- end Increment;
-
- ---------
- -- Set --
- ---------
-
- function Set (Id : Entity_Id) return Node_Id is
- begin
- return
- Make_Assignment_Statement (Loc,
- Name => New_Reference_To (Id, Loc),
- Expression => New_Reference_To (Standard_True, Loc));
- end Set;
-
- -- Local variables
-
- Aggr : constant Node_Id :=
- Expression (First
- (Pragma_Argument_Associations (CCs)));
- Decls : constant List_Id := Declarations (N);
- Multiple_PCs : constant Boolean :=
- List_Length (Component_Associations (Aggr)) > 1;
- Case_Guard : Node_Id;
- CG_Checks : Node_Id;
- CG_Stmts : List_Id;
- Conseq : Node_Id;
- Conseq_Checks : Node_Id := Empty;
- Count : Entity_Id;
- Error_Decls : List_Id;
- Flag : Entity_Id;
- Msg_Str : Entity_Id;
- Others_Flag : Entity_Id := Empty;
- Post_Case : Node_Id;
-
- -- Start of processing for Expand_Contract_Cases
-
- begin
- -- Create the counter which tracks the number of case guards that
- -- evaluate to True.
-
- -- Count : Natural := 0;
-
- Count := Make_Temporary (Loc, 'C');
-
- Prepend_To (Decls,
- Make_Object_Declaration (Loc,
- Defining_Identifier => Count,
- Object_Definition => New_Reference_To (Standard_Natural, Loc),
- Expression => Make_Integer_Literal (Loc, 0)));
-
- -- Create the base error message for multiple overlapping case
- -- guards.
-
- -- Msg_Str : constant String :=
- -- "contract cases overlap for subprogram Subp_Id";
-
- if Multiple_PCs then
- Msg_Str := Make_Temporary (Loc, 'S');
-
- Start_String;
- Store_String_Chars ("contract cases overlap for subprogram ");
- Store_String_Chars (Get_Name_String (Chars (Subp_Id)));
-
- Error_Decls := New_List (
- Make_Object_Declaration (Loc,
- Defining_Identifier => Msg_Str,
- Constant_Present => True,
- Object_Definition => New_Reference_To (Standard_String, Loc),
- Expression => Make_String_Literal (Loc, End_String)));
- end if;
-
- -- Process individual post cases
-
- Post_Case := First (Component_Associations (Aggr));
- while Present (Post_Case) loop
- Case_Guard := First (Choices (Post_Case));
- Conseq := Expression (Post_Case);
-
- -- The "others" choice requires special processing
-
- if Nkind (Case_Guard) = N_Others_Choice then
- Others_Flag := Make_Temporary (Loc, 'F');
- Prepend_To (Decls, Declaration_Of (Others_Flag));
-
- -- Check possible overlap between a case guard and "others"
-
- if Multiple_PCs then
- Case_Guard_Error
- (Decls => Error_Decls,
- Flag => Others_Flag,
- Error_Loc => Sloc (Case_Guard),
- Msg => Msg_Str);
- end if;
-
- -- Check the corresponding consequence of "others"
-
- Consequence_Error
- (Checks => Conseq_Checks,
- Flag => Others_Flag,
- Conseq => Conseq);
-
- -- Regular post case
-
- else
- -- Create the flag which tracks the state of its associated
- -- case guard.
-
- Flag := Make_Temporary (Loc, 'F');
- Prepend_To (Decls, Declaration_Of (Flag));
-
- -- The flag is set when the case guard is evaluated to True
- -- if Case_Guard then
- -- Flag := True;
- -- Count := Count + 1;
- -- end if;
-
- Append_To (Decls,
- Make_If_Statement (Loc,
- Condition => Relocate_Node (Case_Guard),
- Then_Statements => New_List (
- Set (Flag),
- Increment (Count))));
-
- -- Check whether this case guard overlaps with another case
- -- guard.
-
- if Multiple_PCs then
- Case_Guard_Error
- (Decls => Error_Decls,
- Flag => Flag,
- Error_Loc => Sloc (Case_Guard),
- Msg => Msg_Str);
- end if;
-
- -- The corresponding consequence of the case guard which
- -- evaluated to True must hold on exit from the subprogram.
-
- Consequence_Error (Conseq_Checks, Flag, Conseq);
- end if;
-
- Next (Post_Case);
- end loop;
-
- -- Raise Assertion_Error when none of the case guards evaluate to
- -- True. The only exception is when we have "others", in which case
- -- there is no error because "others" acts as a default True.
-
- -- Generate:
- -- Flag := True;
-
- if Present (Others_Flag) then
- CG_Stmts := New_List (Set (Others_Flag));
-
- -- Generate:
- -- raise Assetion_Error with "contract cases incomplete";
-
- else
- Start_String;
- Store_String_Chars ("contract cases incomplete");
-
- CG_Stmts := New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Reference_To (RTE (RE_Raise_Assert_Failure), Loc),
- Parameter_Associations => New_List (
- Make_String_Literal (Loc, End_String))));
- end if;
-
- CG_Checks :=
- Make_If_Statement (Loc,
- Condition =>
- Make_Op_Eq (Loc,
- Left_Opnd => New_Reference_To (Count, Loc),
- Right_Opnd => Make_Integer_Literal (Loc, 0)),
- Then_Statements => CG_Stmts);
-
- -- Detect a possible failure due to several case guards evaluating to
- -- True.
-
- -- Generate:
- -- elsif Count > 0 then
- -- declare
- -- <Error_Decls>
- -- begin
- -- raise Assertion_Error with <Msg_Str>;
- -- end if;
-
- if Multiple_PCs then
- Set_Elsif_Parts (CG_Checks, New_List (
- Make_Elsif_Part (Loc,
- Condition =>
- Make_Op_Gt (Loc,
- Left_Opnd => New_Reference_To (Count, Loc),
- Right_Opnd => Make_Integer_Literal (Loc, 1)),
-
- Then_Statements => New_List (
- Make_Block_Statement (Loc,
- Declarations => Error_Decls,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Reference_To
- (RTE (RE_Raise_Assert_Failure), Loc),
- Parameter_Associations => New_List (
- New_Reference_To (Msg_Str, Loc))))))))));
- end if;
-
- Append_To (Decls, CG_Checks);
-
- -- Raise Assertion_Error when the corresponding consequence of a case
- -- guard that evaluated to True fails.
-
- if No (Plist) then
- Plist := New_List;
- end if;
-
- Append_To (Plist, Conseq_Checks);
- end Expand_Contract_Cases;
-
- --------------
- -- Grab_PPC --
- --------------
-
- function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id is
- Nam : constant Name_Id := Pragma_Name (Prag);
- Map : Elist_Id;
- CP : Node_Id;
-
- Ename : Name_Id;
- -- Effective name of pragma (maybe Pre/Post rather than Precondition/
- -- Postcodition if the pragma came from a Pre/Post aspect). We need
- -- the name right when we generate the Check pragma, since we want
- -- the right set of check policies to apply.
-
- begin
- -- Prepare map if this is the case where we have to map entities of
- -- arguments in the overridden subprogram to corresponding entities
- -- of the current subprogram.
-
- if No (Pspec) then
- Map := No_Elist;
-
- else
- declare
- PF : Entity_Id;
- CF : Entity_Id;
-
- begin
- Map := New_Elmt_List;
- PF := First_Formal (Pspec);
- CF := First_Formal (Designator);
- while Present (PF) loop
- Append_Elmt (PF, Map);
- Append_Elmt (CF, Map);
- Next_Formal (PF);
- Next_Formal (CF);
- end loop;
- end;
- end if;
-
- -- Now we can copy the tree, doing any required substitutions
-
- CP := New_Copy_Tree (Prag, Map => Map, New_Scope => Current_Scope);
-
- -- Set Analyzed to false, since we want to reanalyze the check
- -- procedure. Note that it is only at the outer level that we
- -- do this fiddling, for the spec cases, the already preanalyzed
- -- parameters are not affected.
-
- Set_Analyzed (CP, False);
-
- -- We also make sure Comes_From_Source is False for the copy
-
- Set_Comes_From_Source (CP, False);
-
- -- For a postcondition pragma within a generic, preserve the pragma
- -- for later expansion. This is also used when an error was detected,
- -- thus setting Expander_Active to False.
-
- if Nam = Name_Postcondition
- and then not Expander_Active
- then
- return CP;
- end if;
-
- -- Get effective name of aspect
-
- if Present (Corresponding_Aspect (Prag)) then
- Ename := Chars (Identifier (Corresponding_Aspect (Prag)));
- else
- Ename := Nam;
- end if;
-
- -- Change copy of pragma into corresponding pragma Check
-
- Prepend_To (Pragma_Argument_Associations (CP),
- Make_Pragma_Argument_Association (Sloc (Prag),
- Expression => Make_Identifier (Loc, Ename)));
- Set_Pragma_Identifier (CP, Make_Identifier (Sloc (Prag), Name_Check));
-
- -- If this is inherited case and the current message starts with
- -- "failed p", we change it to "failed inherited p...".
-
- if Present (Pspec) then
- declare
- Msg : constant Node_Id :=
- Last (Pragma_Argument_Associations (CP));
-
- begin
- if Chars (Msg) = Name_Message then
- String_To_Name_Buffer (Strval (Expression (Msg)));
-
- if Name_Buffer (1 .. 8) = "failed p" then
- Insert_Str_In_Name_Buffer ("inherited ", 8);
- Set_Strval
- (Expression (Last (Pragma_Argument_Associations (CP))),
- String_From_Name_Buffer);
- end if;
- end if;
- end;
- end if;
-
- -- Return the check pragma
-
- return CP;
- end Grab_PPC;
-
- -----------------------------------
- -- Insert_After_Last_Declaration --
- -----------------------------------
-
- procedure Insert_After_Last_Declaration (Nod : Node_Id) is
- Decls : constant List_Id := Declarations (N);
-
- begin
- if No (Decls) then
- Set_Declarations (N, New_List (Nod));
- else
- Append_To (Decls, Nod);
- end if;
- end Insert_After_Last_Declaration;
-
- --------------------------------------
- -- Invariants_Or_Predicates_Present --
- --------------------------------------
-
- function Invariants_Or_Predicates_Present return Boolean is
- Formal : Entity_Id;
-
- begin
- -- Check function return result. If result is an access type there
- -- may be invariants on the designated type.
-
- if Ekind (Designator) /= E_Procedure
- and then Has_Invariants (Etype (Designator))
- then
- return True;
-
- elsif Ekind (Designator) /= E_Procedure
- and then Is_Access_Type (Etype (Designator))
- and then Has_Invariants (Designated_Type (Etype (Designator)))
- then
- return True;
- end if;
-
- -- Check parameters
-
- Formal := First_Formal (Designator);
- while Present (Formal) loop
- if Ekind (Formal) /= E_In_Parameter
- and then (Has_Invariants (Etype (Formal))
- or else Present (Predicate_Function (Etype (Formal))))
- then
- return True;
-
- elsif Is_Access_Type (Etype (Formal))
- and then Has_Invariants (Designated_Type (Etype (Formal)))
- then
- return True;
- end if;
-
- Next_Formal (Formal);
- end loop;
-
- return False;
- end Invariants_Or_Predicates_Present;
-
- ------------------------------
- -- Is_Public_Subprogram_For --
- ------------------------------
-
- -- The type T is a private type, its declaration is therefore in
- -- the list of public declarations of some package. The test for a
- -- public subprogram is that its declaration is in this same list
- -- of declarations for the same package (note that all the public
- -- declarations are in one list, and all the private declarations
- -- in another, so this deals with the public/private distinction).
-
- function Is_Public_Subprogram_For (T : Entity_Id) return Boolean is
- DD : constant Node_Id := Unit_Declaration_Node (Designator);
- -- The subprogram declaration for the subprogram in question
-
- TL : constant List_Id :=
- Visible_Declarations
- (Specification (Unit_Declaration_Node (Scope (T))));
- -- The list of declarations containing the private declaration of
- -- the type. We know it is a private type, so we know its scope is
- -- the package in question, and we know it must be in the visible
- -- declarations of this package.
-
- begin
- -- If the subprogram declaration is not a list member, it must be
- -- an Init_Proc, in which case we want to consider it to be a
- -- public subprogram, since we do get initializations to deal with.
- -- Other internally generated subprograms are not public.
-
- if not Is_List_Member (DD)
- and then Is_Init_Proc (Defining_Entity (DD))
- then
- return True;
-
- -- The declaration may have been generated for an expression function
- -- so check whether that function comes from source.
-
- elsif not Comes_From_Source (DD)
- and then
- (Nkind (Original_Node (DD)) /= N_Expression_Function
- or else not Comes_From_Source (Defining_Entity (DD)))
- then
- return False;
-
- -- Otherwise we test whether the subprogram is declared in the
- -- visible declarations of the package containing the type.
-
- else
- return TL = List_Containing (DD);
- end if;
- end Is_Public_Subprogram_For;
-
- -- Start of processing for Process_PPCs
-
- begin
- -- Capture designator from spec if present, else from body
-
- if Present (Spec_Id) then
- Designator := Spec_Id;
- else
- Designator := Body_Id;
- end if;
-
- -- Internally generated subprograms, such as type-specific functions,
- -- don't get assertion checks.
-
- if Get_TSS_Name (Designator) /= TSS_Null then
- return;
- end if;
-
- -- Grab preconditions from spec
-
- if Present (Spec_Id) then
-
- -- Loop through PPC pragmas from spec. Note that preconditions from
- -- the body will be analyzed and converted when we scan the body
- -- declarations below.
-
- Prag := Spec_PPC_List (Contract (Spec_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition then
-
- -- For Pre (or Precondition pragma), we simply prepend the
- -- pragma to the list of declarations right away so that it
- -- will be executed at the start of the procedure. Note that
- -- this processing reverses the order of the list, which is
- -- what we want since new entries were chained to the head of
- -- the list. There can be more than one precondition when we
- -- use pragma Precondition.
-
- if not Class_Present (Prag) then
- Prepend (Grab_PPC, Declarations (N));
-
- -- For Pre'Class there can only be one pragma, and we save
- -- it in Precond for now. We will add inherited Pre'Class
- -- stuff before inserting this pragma in the declarations.
- else
- Precond := Grab_PPC;
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Now deal with inherited preconditions
-
- for J in Inherited'Range loop
- Prag := Spec_PPC_List (Contract (Inherited (J)));
-
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Class_Present (Prag)
- then
- Inherited_Precond := Grab_PPC (Inherited (J));
-
- -- No precondition so far, so establish this as the first
-
- if No (Precond) then
- Precond := Inherited_Precond;
-
- -- Here we already have a precondition, add inherited one
-
- else
- -- Add new precondition to old one using OR ELSE
-
- declare
- New_Expr : constant Node_Id :=
- Get_Pragma_Arg
- (Next
- (First
- (Pragma_Argument_Associations
- (Inherited_Precond))));
- Old_Expr : constant Node_Id :=
- Get_Pragma_Arg
- (Next
- (First
- (Pragma_Argument_Associations
- (Precond))));
-
- begin
- if Paren_Count (Old_Expr) = 0 then
- Set_Paren_Count (Old_Expr, 1);
- end if;
-
- if Paren_Count (New_Expr) = 0 then
- Set_Paren_Count (New_Expr, 1);
- end if;
-
- Rewrite (Old_Expr,
- Make_Or_Else (Sloc (Old_Expr),
- Left_Opnd => Relocate_Node (Old_Expr),
- Right_Opnd => New_Expr));
- end;
-
- -- Add new message in the form:
-
- -- failed precondition from bla
- -- also failed inherited precondition from bla
- -- ...
-
- -- Skip this if exception locations are suppressed
-
- if not Exception_Locations_Suppressed then
- declare
- New_Msg : constant Node_Id :=
- Get_Pragma_Arg
- (Last
- (Pragma_Argument_Associations
- (Inherited_Precond)));
- Old_Msg : constant Node_Id :=
- Get_Pragma_Arg
- (Last
- (Pragma_Argument_Associations
- (Precond)));
- begin
- Start_String (Strval (Old_Msg));
- Store_String_Chars (ASCII.LF & " also ");
- Store_String_Chars (Strval (New_Msg));
- Set_Strval (Old_Msg, End_String);
- end;
- end if;
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end loop;
-
- -- If we have built a precondition for Pre'Class (including any
- -- Pre'Class aspects inherited from parent subprograms), then we
- -- insert this composite precondition at this stage.
-
- if Present (Precond) then
- Prepend (Precond, Declarations (N));
- end if;
- end if;
-
- -- Build postconditions procedure if needed and prepend the following
- -- declaration to the start of the declarations for the subprogram.
-
- -- procedure _postconditions [(_Result : resulttype)] is
- -- begin
- -- pragma Check (Postcondition, condition [,message]);
- -- pragma Check (Postcondition, condition [,message]);
- -- ...
- -- Invariant_Procedure (_Result) ...
- -- Invariant_Procedure (Arg1)
- -- ...
- -- end;
-
- -- First we deal with the postconditions in the body
-
- if Is_Non_Empty_List (Declarations (N)) then
-
- -- Loop through declarations
-
- Prag := First (Declarations (N));
- while Present (Prag) loop
- if Nkind (Prag) = N_Pragma then
- Check_Applicable_Policy (Prag);
-
- -- If pragma, capture if postconditions enabled, else ignore
-
- if Pragma_Name (Prag) = Name_Postcondition
- and then not Is_Ignored (Prag)
- then
- if Plist = No_List then
- Plist := Empty_List;
- end if;
-
- Analyze (Prag);
-
- -- If expansion is disabled, as in a generic unit, save
- -- pragma for later expansion.
-
- if not Expander_Active then
- Prepend (Grab_PPC, Declarations (N));
- else
- Append (Grab_PPC, Plist);
- end if;
- end if;
-
- Next (Prag);
-
- -- Not a pragma, if comes from source, then end scan
-
- elsif Comes_From_Source (Prag) then
- exit;
-
- -- Skip stuff not coming from source
-
- else
- Next (Prag);
- end if;
- end loop;
- end if;
-
- -- Now deal with any postconditions from the spec
-
- if Present (Spec_Id) then
- Spec_Postconditions : declare
- procedure Process_Contract_Cases (Spec : Node_Id);
- -- This processes the Spec_CTC_List from Spec, processing any
- -- contract-cases from the list. The caller has checked that
- -- Spec_CTC_List is non-Empty.
-
- procedure Process_Post_Conditions
- (Spec : Node_Id;
- Class : Boolean);
- -- This processes the Spec_PPC_List from Spec, processing any
- -- postconditions from the list. If Class is True, then only
- -- postconditions marked with Class_Present are considered.
- -- The caller has checked that Spec_PPC_List is non-Empty.
-
- ----------------------------
- -- Process_Contract_Cases --
- ----------------------------
-
- procedure Process_Contract_Cases (Spec : Node_Id) is
- begin
- -- Loop through Contract_Cases pragmas from spec
-
- Prag := Spec_CTC_List (Contract (Spec));
- loop
- if Pragma_Name (Prag) = Name_Contract_Cases then
- Expand_Contract_Cases (Prag, Spec_Id);
- end if;
-
- Prag := Next_Pragma (Prag);
- exit when No (Prag);
- end loop;
- end Process_Contract_Cases;
-
- -----------------------------
- -- Process_Post_Conditions --
- -----------------------------
-
- procedure Process_Post_Conditions
- (Spec : Node_Id;
- Class : Boolean)
- is
- Pspec : Node_Id;
-
- begin
- if Class then
- Pspec := Spec;
- else
- Pspec := Empty;
- end if;
-
- -- Loop through PPC pragmas from spec
-
- Prag := Spec_PPC_List (Contract (Spec));
- loop
- if Pragma_Name (Prag) = Name_Postcondition
- and then (not Class or else Class_Present (Prag))
- then
- if Plist = No_List then
- Plist := Empty_List;
- end if;
-
- if not Expander_Active then
- Prepend
- (Grab_PPC (Pspec), Declarations (N));
- else
- Append (Grab_PPC (Pspec), Plist);
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- exit when No (Prag);
- end loop;
- end Process_Post_Conditions;
-
- -- Start of processing for Spec_Postconditions
-
- begin
- -- Process postconditions expressed as contract-cases
-
- if Present (Spec_CTC_List (Contract (Spec_Id))) then
- Process_Contract_Cases (Spec_Id);
- end if;
-
- -- Process spec postconditions
-
- if Present (Spec_PPC_List (Contract (Spec_Id))) then
- Process_Post_Conditions (Spec_Id, Class => False);
- end if;
-
- -- Process inherited postconditions
-
- for J in Inherited'Range loop
- if Present (Spec_PPC_List (Contract (Inherited (J)))) then
- Process_Post_Conditions (Inherited (J), Class => True);
- end if;
- end loop;
- end Spec_Postconditions;
- end if;
-
- -- If we had any postconditions and expansion is enabled, or if the
- -- subprogram has invariants, then build the _Postconditions procedure.
-
- if (Present (Plist) or else Invariants_Or_Predicates_Present)
- and then Expander_Active
- then
- if No (Plist) then
- Plist := Empty_List;
- end if;
-
- -- Special processing for function return
-
- if Ekind (Designator) /= E_Procedure then
- declare
- Rent : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_uResult);
- Ftyp : constant Entity_Id := Etype (Designator);
-
- begin
- Set_Etype (Rent, Ftyp);
-
- -- Add argument for return
-
- Parms :=
- New_List (
- Make_Parameter_Specification (Loc,
- Parameter_Type => New_Occurrence_Of (Ftyp, Loc),
- Defining_Identifier => Rent));
-
- -- Add invariant call if returning type with invariants and
- -- this is a public function, i.e. a function declared in the
- -- visible part of the package defining the private type.
-
- if Has_Invariants (Etype (Rent))
- and then Present (Invariant_Procedure (Etype (Rent)))
- and then Is_Public_Subprogram_For (Etype (Rent))
- then
- Append_To (Plist,
- Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
- end if;
-
- -- Same if return value is an access to type with invariants
-
- Check_Access_Invariants (Rent);
- end;
-
- -- Procedure rather than a function
-
- else
- Parms := No_List;
- end if;
-
- -- Add invariant calls and predicate calls for parameters. Note that
- -- this is done for functions as well, since in Ada 2012 they can
- -- have IN OUT args.
-
- declare
- Formal : Entity_Id;
- Ftype : Entity_Id;
-
- begin
- Formal := First_Formal (Designator);
- while Present (Formal) loop
- if Ekind (Formal) /= E_In_Parameter
- or else Is_Access_Type (Etype (Formal))
- then
- Ftype := Etype (Formal);
-
- if Has_Invariants (Ftype)
- and then Present (Invariant_Procedure (Ftype))
- and then Is_Public_Subprogram_For (Ftype)
- then
- Append_To (Plist,
- Make_Invariant_Call
- (New_Occurrence_Of (Formal, Loc)));
- end if;
-
- Check_Access_Invariants (Formal);
-
- if Present (Predicate_Function (Ftype)) then
- Append_To (Plist,
- Make_Predicate_Check
- (Ftype, New_Occurrence_Of (Formal, Loc)));
- end if;
- end if;
-
- Next_Formal (Formal);
- end loop;
- end;
-
- -- Build and insert postcondition procedure
-
- declare
- Post_Proc : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => Name_uPostconditions);
- -- The entity for the _Postconditions procedure
-
- begin
- -- Insert the corresponding body of a post condition pragma after
- -- the last declaration of the context. This ensures that the body
- -- will not cause any premature freezing as it may mention types:
-
- -- procedure Proc (Obj : Array_Typ) is
- -- procedure _postconditions is
- -- begin
- -- ... Obj ...
- -- end _postconditions;
-
- -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
- -- begin
-
- -- In the example above, Obj is of type T but the incorrect
- -- placement of _postconditions will cause a crash in gigi due to
- -- an out of order reference. The body of _postconditions must be
- -- placed after the declaration of Temp to preserve correct
- -- visibility.
-
- Insert_After_Last_Declaration (
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Post_Proc,
- Parameter_Specifications => Parms),
-
- Declarations => Empty_List,
-
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Plist)));
-
- Set_Ekind (Post_Proc, E_Procedure);
-
- -- If this is a procedure, set the Postcondition_Proc attribute on
- -- the proper defining entity for the subprogram.
-
- if Ekind (Designator) = E_Procedure then
- Set_Postcondition_Proc (Designator, Post_Proc);
- end if;
- end;
-
- Set_Has_Postconditions (Designator);
- end if;
- end Process_PPCs;
-
----------------------------
-- Reference_Body_Formals --
----------------------------
AS_Needed := False;
-- If we have unknown discriminants, then we do not need an actual
- -- subtype, or more accurately we cannot figure it out! Note that
+ -- subtype, or more accurately we cannot figure it out. Note that
-- all class-wide types have unknown discriminants.
elsif Has_Unknown_Discriminants (T) then
-- parameter block, and it is this local variable that may
-- require an actual subtype.
- if Full_Expander_Active then
+ if Expander_Active then
Decl := Build_Actual_Subtype (T, Renamed_Object (Formal));
else
Decl := Build_Actual_Subtype (T, Formal);
if Present (First_Stmt) then
Insert_List_Before_And_Analyze (First_Stmt,
Freeze_Entity (Defining_Identifier (Decl), N));
+
+ -- Ditto if the type has a dynamic predicate, because the
+ -- generated function will mention the actual subtype.
+
+ elsif Has_Dynamic_Predicate_Aspect (T) then
+ Insert_List_Before_And_Analyze (Decl,
+ Freeze_Entity (Defining_Identifier (Decl), N));
end if;
if Nkind (N) = N_Accept_Statement
- and then Full_Expander_Active
+ and then Expander_Active
then
Set_Actual_Subtype (Renamed_Object (Formal),
Defining_Identifier (Decl));
-- point of the call.
if Out_Present (Spec) then
- if Ekind (Scope (Formal_Id)) = E_Function
- or else Ekind (Scope (Formal_Id)) = E_Generic_Function
- then
+ if Ekind_In (Scope (Formal_Id), E_Function, E_Generic_Function) then
+
-- [IN] OUT parameters allowed for functions in Ada 2012
if Ada_Version >= Ada_2012 then
Set_Ekind (Formal_Id, E_Out_Parameter);
end if;
+ Set_Has_Out_Or_In_Out_Parameter (Scope (Formal_Id), True);
+
-- But not in earlier versions of Ada
else
Error_Msg_N
("default values not allowed for operator parameters",
Parent (F));
+
+ -- For function instantiations that are operators, we must check
+ -- separately that the corresponding generic only has in-parameters.
+ -- For subprogram declarations this is done in Set_Formal_Mode.
+ -- Such an error could not arise in earlier versions of the language.
+
+ elsif Ekind (F) /= E_In_Parameter then
+ Error_Msg_N
+ ("operators can only have IN parameters", F);
end if;
Next_Formal (F);
projects / gcc.git / blobdiff