-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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 Sem_Ch8; use Sem_Ch8;
with Sem_Ch10; use Sem_Ch10;
with Sem_Ch12; use Sem_Ch12;
+with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Dist; use Sem_Dist;
with Sem_Elim; use Sem_Elim;
-- If proper warnings are enabled and the subprogram contains a construct
-- that cannot be inlined, the offending construct is flagged accordingly.
+ function Can_Override_Operator (Subp : Entity_Id) return Boolean;
+ -- Returns true if Subp can override a predefined operator.
+
procedure Check_Conformance
(New_Id : Entity_Id;
Old_Id : Entity_Id;
-- entity with that name.
procedure Install_Entity (E : Entity_Id);
- -- Make single entity visible. Used for generic formals as well
+ -- Make single entity visible (used for generic formals as well)
function Is_Non_Overriding_Operation
(Prev_E : Entity_Id;
-- 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).
+ -- 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
-- the kind of parameter and the validity checking mode.
- ------------------------------
- -- Analyze_Return_Statement --
- ------------------------------
-
- procedure Analyze_Return_Statement (N : Node_Id) is
-
- pragma Assert (Nkind_In (N, N_Simple_Return_Statement,
- N_Extended_Return_Statement));
-
- Returns_Object : constant Boolean :=
- Nkind (N) = N_Extended_Return_Statement
- or else
- (Nkind (N) = N_Simple_Return_Statement
- and then Present (Expression (N)));
- -- True if we're returning something; that is, "return <expression>;"
- -- or "return Result : T [:= ...]". False for "return;". Used for error
- -- checking: If Returns_Object is True, N should apply to a function
- -- body; otherwise N should apply to a procedure body, entry body,
- -- accept statement, or extended return statement.
-
- function Find_What_It_Applies_To return Entity_Id;
- -- Find the entity representing the innermost enclosing body, accept
- -- statement, or extended return statement. If the result is a callable
- -- construct or extended return statement, then this will be the value
- -- of the Return_Applies_To attribute. Otherwise, the program is
- -- illegal. See RM-6.5(4/2).
-
- -----------------------------
- -- Find_What_It_Applies_To --
- -----------------------------
-
- function Find_What_It_Applies_To return Entity_Id is
- Result : Entity_Id := Empty;
-
- begin
- -- Loop outward through the Scope_Stack, skipping blocks and loops
-
- for J in reverse 0 .. Scope_Stack.Last loop
- Result := Scope_Stack.Table (J).Entity;
- exit when Ekind (Result) /= E_Block and then
- Ekind (Result) /= E_Loop;
- end loop;
-
- pragma Assert (Present (Result));
- return Result;
- end Find_What_It_Applies_To;
-
- -- Local declarations
-
- Scope_Id : constant Entity_Id := Find_What_It_Applies_To;
- Kind : constant Entity_Kind := Ekind (Scope_Id);
- Loc : constant Source_Ptr := Sloc (N);
- Stm_Entity : constant Entity_Id :=
- New_Internal_Entity
- (E_Return_Statement, Current_Scope, Loc, 'R');
-
- -- Start of processing for Analyze_Return_Statement
-
- begin
- Set_Return_Statement_Entity (N, Stm_Entity);
-
- Set_Etype (Stm_Entity, Standard_Void_Type);
- Set_Return_Applies_To (Stm_Entity, Scope_Id);
-
- -- Place Return entity on scope stack, to simplify enforcement of 6.5
- -- (4/2): an inner return statement will apply to this extended return.
-
- if Nkind (N) = N_Extended_Return_Statement then
- Push_Scope (Stm_Entity);
- end if;
-
- -- Check that pragma No_Return is obeyed. Don't complain about the
- -- implicitly-generated return that is placed at the end.
-
- if No_Return (Scope_Id) and then Comes_From_Source (N) then
- Error_Msg_N ("RETURN statement not allowed (No_Return)", N);
- end if;
-
- -- Warn on any unassigned OUT parameters if in procedure
-
- if Ekind (Scope_Id) = E_Procedure then
- Warn_On_Unassigned_Out_Parameter (N, Scope_Id);
- end if;
-
- -- Check that functions return objects, and other things do not
-
- if Kind = E_Function or else Kind = E_Generic_Function then
- if not Returns_Object then
- Error_Msg_N ("missing expression in return from function", N);
- end if;
-
- elsif Kind = E_Procedure or else Kind = E_Generic_Procedure then
- if Returns_Object then
- Error_Msg_N ("procedure cannot return value (use function)", N);
- end if;
-
- elsif Kind = E_Entry or else Kind = E_Entry_Family then
- if Returns_Object then
- if Is_Protected_Type (Scope (Scope_Id)) then
- Error_Msg_N ("entry body cannot return value", N);
- else
- Error_Msg_N ("accept statement cannot return value", N);
- end if;
- end if;
-
- elsif Kind = E_Return_Statement then
-
- -- We are nested within another return statement, which must be an
- -- extended_return_statement.
-
- if Returns_Object then
- Error_Msg_N
- ("extended_return_statement cannot return value; " &
- "use `""RETURN;""`", N);
- end if;
-
- else
- Error_Msg_N ("illegal context for return statement", N);
- end if;
-
- if Kind = E_Function or else Kind = E_Generic_Function then
- Analyze_Function_Return (N);
- end if;
-
- if Nkind (N) = N_Extended_Return_Statement then
- End_Scope;
- end if;
-
- Kill_Current_Values (Last_Assignment_Only => True);
- Check_Unreachable_Code (N);
- end Analyze_Return_Statement;
-
---------------------------------------------
-- Analyze_Abstract_Subprogram_Declaration --
---------------------------------------------
Scop : constant Entity_Id := Current_Scope;
begin
+ Check_SPARK_Restriction ("abstract subprogram is not allowed", N);
+
Generate_Definition (Designator);
+ Set_Contract (Designator, Make_Contract (Sloc (Designator)));
Set_Is_Abstract_Subprogram (Designator);
New_Overloaded_Entity (Designator);
Check_Delayed_Subprogram (Designator);
elsif Warn_On_Redundant_Constructs
and then not Is_Dispatching_Operation (Designator)
- and then not Is_Overriding_Operation (Designator)
+ and then not Present (Overridden_Operation (Designator))
and then (not Is_Operator_Symbol_Name (Chars (Designator))
or else Scop /= Scope (Etype (First_Formal (Designator))))
then
Generate_Reference_To_Formals (Designator);
Check_Eliminated (Designator);
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Designator);
+ end if;
end Analyze_Abstract_Subprogram_Declaration;
+ ---------------------------------
+ -- Analyze_Expression_Function --
+ ---------------------------------
+
+ procedure Analyze_Expression_Function (N : Node_Id) is
+ Loc : constant Source_Ptr := Sloc (N);
+ LocX : constant Source_Ptr := Sloc (Expression (N));
+ Def_Id : constant Entity_Id := Defining_Entity (Specification (N));
+ New_Body : Node_Id;
+ New_Decl : Node_Id;
+
+ Prev : constant Entity_Id := Current_Entity_In_Scope (Def_Id);
+ -- If the expression is a completion, Prev is the entity whose
+ -- declaration is completed.
+
+ begin
+ -- This is one of the occasions on which we transform the tree during
+ -- semantic analysis. If this is a completion, transform the expression
+ -- function into an equivalent subprogram body, and analyze it.
+
+ -- Expression functions are inlined unconditionally. The back-end will
+ -- determine whether this is possible.
+
+ Inline_Processing_Required := True;
+
+ New_Body :=
+ Make_Subprogram_Body (Loc,
+ Specification => Specification (N),
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (LocX,
+ Statements => New_List (
+ Make_Simple_Return_Statement (LocX,
+ Expression => Expression (N)))));
+
+ if Present (Prev)
+ and then Ekind (Prev) = E_Generic_Function
+ then
+ -- 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.
+
+ Insert_After (N, New_Body);
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
+ Analyze (New_Body);
+ Set_Is_Inlined (Prev);
+
+ elsif Present (Prev) then
+ Rewrite (N, New_Body);
+ Set_Is_Inlined (Prev);
+ Analyze (N);
+
+ -- If this is not a completion, create both a declaration and a body,
+ -- so that the expression can be inlined whenever possible.
+
+ else
+ New_Decl :=
+ Make_Subprogram_Declaration (Loc,
+ Specification => Specification (N));
+ Rewrite (N, New_Decl);
+ Analyze (N);
+ Set_Is_Inlined (Defining_Entity (New_Decl));
+
+ -- Create new set of formals for specification in body.
+
+ Set_Specification (New_Body,
+ Make_Function_Specification (Loc,
+ Defining_Unit_Name =>
+ Make_Defining_Identifier (Loc, Chars (Defining_Entity (N))),
+ Parameter_Specifications =>
+ Copy_Parameter_List (Defining_Entity (New_Decl)),
+ Result_Definition =>
+ New_Copy_Tree (Result_Definition (Specification (New_Decl)))));
+
+ Insert_After (N, New_Body);
+ Analyze (New_Body);
+ end if;
+ end Analyze_Expression_Function;
+
----------------------------------------
-- Analyze_Extended_Return_Statement --
----------------------------------------
----------------------------
procedure Analyze_Function_Call (N : Node_Id) is
- P : constant Node_Id := Name (N);
- L : constant List_Id := Parameter_Associations (N);
- Actual : Node_Id;
+ P : constant Node_Id := Name (N);
+ Actuals : constant List_Id := Parameter_Associations (N);
+ Actual : Node_Id;
begin
Analyze (P);
-- Otherwise analyze the parameters
- if Present (L) then
- Actual := First (L);
+ if Present (Actuals) then
+ Actual := First (Actuals);
while Present (Actual) loop
Analyze (Actual);
Check_Parameterless_Call (Actual);
if Nkind (N) = N_Simple_Return_Statement then
Expr := Expression (N);
- Analyze_And_Resolve (Expr, R_Type);
- Check_Limited_Return (Expr);
+
+ -- Guard against a malformed expression. The parser may have tried to
+ -- recover but the node is not analyzable.
+
+ if Nkind (Expr) = N_Error then
+ Set_Etype (Expr, Any_Type);
+ Expander_Mode_Save_And_Set (False);
+ return;
+
+ else
+ -- The resolution of a controlled [extension] aggregate associated
+ -- with a return statement creates a temporary which needs to be
+ -- finalized on function exit. Wrap the return statement inside a
+ -- block so that the finalization machinery can detect this case.
+ -- This early expansion is done only when the return statement is
+ -- not part of a handled sequence of statements.
+
+ if Nkind_In (Expr, N_Aggregate,
+ N_Extension_Aggregate)
+ and then Needs_Finalization (R_Type)
+ and then Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements
+ then
+ Rewrite (N,
+ Make_Block_Statement (Loc,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (Relocate_Node (N)))));
+
+ Analyze (N);
+ return;
+ end if;
+
+ Analyze_And_Resolve (Expr, R_Type);
+ Check_Limited_Return (Expr);
+ end if;
+
+ -- RETURN only allowed in SPARK as the last statement in function
+
+ if Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements
+ and then
+ (Nkind (Parent (Parent (N))) /= N_Subprogram_Body
+ or else Present (Next (N)))
+ then
+ Check_SPARK_Restriction
+ ("RETURN should be the last statement in function", N);
+ end if;
else
+ Check_SPARK_Restriction ("extended RETURN is not allowed", N);
+
-- Analyze parts specific to extended_return_statement:
declare
end if;
-- Apply checks suggested by AI05-0144 (dangerous order dependence)
- -- (Disabled for now)
- -- Check_Order_Dependence;
+ Check_Order_Dependence;
end if;
end Analyze_Function_Return;
end if;
Set_Actual_Subtypes (N, Current_Scope);
- Process_PPCs (N, Gen_Id, Body_Id);
+
+ -- 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, Gen_Id, Body_Id);
+ end if;
-- If the generic unit carries pre- or post-conditions, copy them
-- to the original generic tree, so that they are properly added
Analyze (Explicit_Actual_Parameter (N));
end Analyze_Parameter_Association;
- --------------------------------------
- -- Analyze_Parameterized_Expression --
- --------------------------------------
-
- procedure Analyze_Parameterized_Expression (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- LocX : constant Source_Ptr := Sloc (Expression (N));
-
- begin
- -- This is one of the occasions on which we write things during semantic
- -- analysis. Transform the parameterized expression into an equivalent
- -- subprogram body, and then analyze that.
-
- Rewrite (N,
- Make_Subprogram_Body (Loc,
- Specification => Specification (N),
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (LocX,
- Statements => New_List (
- Make_Simple_Return_Statement (LocX,
- Expression => Expression (N))))));
- Analyze (N);
- end Analyze_Parameterized_Expression;
-
----------------------------
-- Analyze_Procedure_Call --
----------------------------
Analyze_Call (N);
Resolve (N, Standard_Void_Type);
- -- Apply checks suggested by AI05-0144 (Disabled for now)
+ -- Apply checks suggested by AI05-0144
- -- Check_Order_Dependence;
+ Check_Order_Dependence;
else
Analyze (N);
end loop;
end if;
- -- Special processing for Elab_Spec and Elab_Body calls
+ -- Special processing for Elab_Spec, Elab_Body and Elab_Subp_Body calls
if Nkind (P) = N_Attribute_Reference
and then (Attribute_Name (P) = Name_Elab_Spec
- or else Attribute_Name (P) = Name_Elab_Body)
+ or else Attribute_Name (P) = Name_Elab_Body
+ or else Attribute_Name (P) = Name_Elab_Subp_Body)
then
if Present (Actuals) then
Error_Msg_N
Set_Parameter_Associations (N, No_List);
Analyze_Call_And_Resolve;
- -- For the case of a reference to an element of an entry family, P is
- -- an indexed component whose prefix is a selected component (task and
- -- entry family), and whose index is the entry family index.
+ -- For the case of a reference to an element of an entry family, P is
+ -- an indexed component whose prefix is a selected component (task and
+ -- entry family), and whose index is the entry family index.
+
+ elsif Nkind (P) = N_Indexed_Component
+ and then Nkind (Prefix (P)) = N_Selected_Component
+ and then Ekind (Entity (Selector_Name (Prefix (P)))) = E_Entry_Family
+ then
+ Analyze_Call_And_Resolve;
+
+ -- If the prefix is the name of an entry family, it is a call from
+ -- within the task body itself.
+
+ elsif Nkind (P) = N_Indexed_Component
+ and then Nkind (Prefix (P)) = N_Identifier
+ and then Ekind (Entity (Prefix (P))) = E_Entry_Family
+ then
+ New_N :=
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Scope (Entity (Prefix (P))), Loc),
+ Selector_Name => New_Occurrence_Of (Entity (Prefix (P)), Loc));
+ Rewrite (Prefix (P), New_N);
+ Analyze (P);
+ Analyze_Call_And_Resolve;
+
+ -- Anything else is an error
+
+ else
+ Error_Msg_N ("invalid procedure or entry call", N);
+ end if;
+ end Analyze_Procedure_Call;
+
+ ------------------------------
+ -- Analyze_Return_Statement --
+ ------------------------------
+
+ procedure Analyze_Return_Statement (N : Node_Id) is
+
+ pragma Assert (Nkind_In (N, N_Simple_Return_Statement,
+ N_Extended_Return_Statement));
+
+ Returns_Object : constant Boolean :=
+ Nkind (N) = N_Extended_Return_Statement
+ or else
+ (Nkind (N) = N_Simple_Return_Statement
+ and then Present (Expression (N)));
+ -- True if we're returning something; that is, "return <expression>;"
+ -- or "return Result : T [:= ...]". False for "return;". Used for error
+ -- checking: If Returns_Object is True, N should apply to a function
+ -- body; otherwise N should apply to a procedure body, entry body,
+ -- accept statement, or extended return statement.
+
+ function Find_What_It_Applies_To return Entity_Id;
+ -- Find the entity representing the innermost enclosing body, accept
+ -- statement, or extended return statement. If the result is a callable
+ -- construct or extended return statement, then this will be the value
+ -- of the Return_Applies_To attribute. Otherwise, the program is
+ -- illegal. See RM-6.5(4/2).
+
+ -----------------------------
+ -- Find_What_It_Applies_To --
+ -----------------------------
+
+ function Find_What_It_Applies_To return Entity_Id is
+ Result : Entity_Id := Empty;
+
+ begin
+ -- Loop outward through the Scope_Stack, skipping blocks and loops
+
+ for J in reverse 0 .. Scope_Stack.Last loop
+ Result := Scope_Stack.Table (J).Entity;
+ exit when Ekind (Result) /= E_Block and then
+ Ekind (Result) /= E_Loop;
+ end loop;
+
+ pragma Assert (Present (Result));
+ return Result;
+ end Find_What_It_Applies_To;
+
+ -- Local declarations
+
+ Scope_Id : constant Entity_Id := Find_What_It_Applies_To;
+ Kind : constant Entity_Kind := Ekind (Scope_Id);
+ Loc : constant Source_Ptr := Sloc (N);
+ Stm_Entity : constant Entity_Id :=
+ New_Internal_Entity
+ (E_Return_Statement, Current_Scope, Loc, 'R');
+
+ -- Start of processing for Analyze_Return_Statement
+
+ begin
+ Set_Return_Statement_Entity (N, Stm_Entity);
+
+ Set_Etype (Stm_Entity, Standard_Void_Type);
+ Set_Return_Applies_To (Stm_Entity, Scope_Id);
+
+ -- Place Return entity on scope stack, to simplify enforcement of 6.5
+ -- (4/2): an inner return statement will apply to this extended return.
+
+ if Nkind (N) = N_Extended_Return_Statement then
+ Push_Scope (Stm_Entity);
+ end if;
+
+ -- Check that pragma No_Return is obeyed. Don't complain about the
+ -- implicitly-generated return that is placed at the end.
+
+ if No_Return (Scope_Id) and then Comes_From_Source (N) then
+ Error_Msg_N ("RETURN statement not allowed (No_Return)", N);
+ end if;
+
+ -- Warn on any unassigned OUT parameters if in procedure
+
+ if Ekind (Scope_Id) = E_Procedure then
+ Warn_On_Unassigned_Out_Parameter (N, Scope_Id);
+ end if;
+
+ -- Check that functions return objects, and other things do not
+
+ if Kind = E_Function or else Kind = E_Generic_Function then
+ if not Returns_Object then
+ Error_Msg_N ("missing expression in return from function", N);
+ end if;
+
+ elsif Kind = E_Procedure or else Kind = E_Generic_Procedure then
+ if Returns_Object then
+ Error_Msg_N ("procedure cannot return value (use function)", N);
+ end if;
+
+ elsif Kind = E_Entry or else Kind = E_Entry_Family then
+ if Returns_Object then
+ if Is_Protected_Type (Scope (Scope_Id)) then
+ Error_Msg_N ("entry body cannot return value", N);
+ else
+ Error_Msg_N ("accept statement cannot return value", N);
+ end if;
+ end if;
+
+ elsif Kind = E_Return_Statement then
- elsif Nkind (P) = N_Indexed_Component
- and then Nkind (Prefix (P)) = N_Selected_Component
- and then Ekind (Entity (Selector_Name (Prefix (P)))) = E_Entry_Family
- then
- Analyze_Call_And_Resolve;
+ -- We are nested within another return statement, which must be an
+ -- extended_return_statement.
- -- If the prefix is the name of an entry family, it is a call from
- -- within the task body itself.
+ if Returns_Object then
+ Error_Msg_N
+ ("extended_return_statement cannot return value; " &
+ "use `""RETURN;""`", N);
+ end if;
- elsif Nkind (P) = N_Indexed_Component
- and then Nkind (Prefix (P)) = N_Identifier
- and then Ekind (Entity (Prefix (P))) = E_Entry_Family
- then
- New_N :=
- Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Scope (Entity (Prefix (P))), Loc),
- Selector_Name => New_Occurrence_Of (Entity (Prefix (P)), Loc));
- Rewrite (Prefix (P), New_N);
- Analyze (P);
- Analyze_Call_And_Resolve;
+ else
+ Error_Msg_N ("illegal context for return statement", N);
+ end if;
- -- Anything else is an error
+ if Ekind_In (Kind, E_Function, E_Generic_Function) then
+ Analyze_Function_Return (N);
- else
- Error_Msg_N ("invalid procedure or entry call", N);
+ elsif Ekind_In (Kind, E_Procedure, E_Generic_Procedure) then
+ Set_Return_Present (Scope_Id);
end if;
- end Analyze_Procedure_Call;
+
+ if Nkind (N) = N_Extended_Return_Statement then
+ End_Scope;
+ end if;
+
+ Kill_Current_Values (Last_Assignment_Only => True);
+ Check_Unreachable_Code (N);
+ end Analyze_Return_Statement;
-------------------------------------
-- Analyze_Simple_Return_Statement --
if Result_Definition (N) /= Error then
if Nkind (Result_Definition (N)) = N_Access_Definition then
+ Check_SPARK_Restriction
+ ("access result is not allowed", Result_Definition (N));
-- Ada 2005 (AI-254): Handle anonymous access to subprograms
Typ := Entity (Result_Definition (N));
Set_Etype (Designator, Typ);
+ -- Unconstrained array as result is not allowed in SPARK
+
+ if Is_Array_Type (Typ)
+ and then not Is_Constrained (Typ)
+ then
+ Check_SPARK_Restriction
+ ("returning an unconstrained array is not allowed",
+ Result_Definition (N));
+ end if;
+
-- Ada 2005 (AI-231): Ensure proper usage of null exclusion
Null_Exclusion_Static_Checks (N);
and then
Ekind (Root_Type (Typ)) = E_Incomplete_Type)
then
- Error_Msg_NE
- ("invalid use of incomplete type&", Designator, Typ);
+ -- AI05-0151: Tagged incomplete types are allowed in all formal
+ -- parts. Untagged incomplete types are not allowed in bodies.
+
+ if Ada_Version >= Ada_2012 then
+ if Is_Tagged_Type (Typ) then
+ null;
+
+ elsif Nkind_In (Parent (Parent (N)),
+ N_Accept_Statement,
+ N_Entry_Body,
+ N_Subprogram_Body)
+ then
+ Error_Msg_NE
+ ("invalid use of untagged incomplete type&",
+ Designator, Typ);
+ end if;
+
+ else
+ Error_Msg_NE
+ ("invalid use of incomplete type&", Designator, Typ);
+ end if;
end if;
end if;
procedure Check_Missing_Return;
-- Checks for a function with a no return statements, and also performs
- -- the warning checks implemented by Check_Returns.
+ -- the warning checks implemented by Check_Returns. In formal mode, also
+ -- verify that a function ends with a RETURN and that a procedure does
+ -- not contain any RETURN.
function Disambiguate_Spec return Entity_Id;
-- When a primitive is declared between the private view and the full
then
Check_Returns (HSS, 'P', Missing_Ret, Spec_Id);
end if;
+
+ -- Special checks in SPARK mode
+
+ if Nkind (Body_Spec) = N_Function_Specification then
+
+ -- In SPARK mode, last statement of a function should be a return
+
+ declare
+ Stat : constant Node_Id := Last_Source_Statement (HSS);
+ begin
+ if Present (Stat)
+ and then not Nkind_In (Stat, N_Simple_Return_Statement,
+ N_Extended_Return_Statement)
+ then
+ Check_SPARK_Restriction
+ ("last statement in function should be RETURN", Stat);
+ end if;
+ end;
+
+ -- In SPARK mode, verify that a procedure has no return
+
+ elsif Nkind (Body_Spec) = N_Procedure_Specification then
+ if Present (Spec_Id) then
+ Id := Spec_Id;
+ else
+ Id := Body_Id;
+ end if;
+
+ -- Would be nice to point to return statement here, can we
+ -- borrow the Check_Returns procedure here ???
+
+ if Return_Present (Id) then
+ Check_SPARK_Restriction
+ ("procedure should not have RETURN", N);
+ end if;
+ end if;
end Check_Missing_Return;
-----------------------
while Present (Formal) loop
Formal_Typ := Etype (Formal);
+ if Is_Class_Wide_Type (Formal_Typ) then
+ Formal_Typ := Root_Type (Formal_Typ);
+ end if;
+
-- From concurrent type to corresponding record
if To_Corresponding then
Formal_Typ := Etype (First_Formal (Subp_Id));
if Is_Concurrent_Record_Type (Formal_Typ) then
+ if Is_Class_Wide_Type (Formal_Typ) then
+ Formal_Typ := Root_Type (Formal_Typ);
+ end if;
+
Formal_Typ := Corresponding_Concurrent_Type (Formal_Typ);
end if;
then
null;
- elsif not Is_Overriding_Operation (Spec_Id) then
+ elsif not Present (Overridden_Operation (Spec_Id)) then
Error_Msg_NE
("subprogram& is not overriding", Body_Spec, Spec_Id);
end if;
elsif Must_Not_Override (Body_Spec) then
- if Is_Overriding_Operation (Spec_Id) then
+ if Present (Overridden_Operation (Spec_Id)) then
Error_Msg_NE
("subprogram& overrides inherited operation",
Body_Spec, Spec_Id);
Body_Spec);
end if;
- elsif Style_Check -- ??? incorrect use of Style_Check!
- and then Is_Overriding_Operation (Spec_Id)
+ elsif Style_Check
+ and then Present (Overridden_Operation (Spec_Id))
+ then
+ pragma Assert (Unit_Declaration_Node (Body_Id) = N);
+ Style.Missing_Overriding (N, Body_Id);
+
+ elsif Style_Check
+ and then Can_Override_Operator (Spec_Id)
+ and then not Is_Predefined_File_Name
+ (Unit_File_Name (Get_Source_Unit (Spec_Id)))
then
pragma Assert (Unit_Declaration_Node (Body_Id) = N);
Style.Missing_Overriding (N, Body_Id);
-- In general, the spec will be frozen when we start analyzing the
-- body. However, for internally generated operations, such as
-- wrapper functions for inherited operations with controlling
- -- results, the spec may not have been frozen by the time we
- -- expand the freeze actions that include the bodies. In particular,
- -- extra formals for accessibility or for return-in-place may need
- -- to be generated. Freeze nodes, if any, are inserted before the
- -- current body.
+ -- results, the spec may not have been frozen by the time we expand
+ -- the freeze actions that include the bodies. In particular, extra
+ -- formals for accessibility or for return-in-place may need to be
+ -- generated. Freeze nodes, if any, are inserted before the current
+ -- body. These freeze actions are also needed in ASIS mode to enable
+ -- the proper back-annotations.
if not Is_Frozen (Spec_Id)
- and then Expander_Active
+ and then (Expander_Active or ASIS_Mode)
then
-- Force the generation of its freezing node to ensure proper
-- management of access types in the backend.
-- why, to be investigated further???
Set_Has_Delayed_Freeze (Spec_Id);
- Insert_Actions (N, Freeze_Entity (Spec_Id, Loc));
+ Freeze_Before (N, Spec_Id);
end if;
end if;
-- Case of subprogram body with no previous spec
else
+ -- Check for style warning required
+
if Style_Check
+
+ -- Only apply check for source level subprograms for which checks
+ -- have not been suppressed.
+
and then Comes_From_Source (Body_Id)
and then not Suppress_Style_Checks (Body_Id)
+
+ -- No warnings within an instance
+
and then not In_Instance
+
+ -- No warnings for expression functions
+
+ and then Nkind (Original_Node (N)) /= N_Expression_Function
then
Style.Body_With_No_Spec (N);
end if;
if Nkind (N) /= N_Subprogram_Body_Stub then
Set_Acts_As_Spec (N);
Generate_Definition (Body_Id);
+ Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Generate_Reference
(Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
Generate_Reference_To_Formals (Body_Id);
HSS := Handled_Statement_Sequence (N);
Set_Actual_Subtypes (N, Current_Scope);
- -- Deal with preconditions and postconditions
+ -- 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.
- Process_PPCs (N, Spec_Id, Body_Id);
+ 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
-- raises an exception, but in any case it is not coming
-- back here, so turn on the flag.
- if Ekind (Ent) = E_Procedure
+ if Present (Ent)
+ and then Ekind (Ent) = E_Procedure
and then No_Return (Ent)
then
Set_Trivial_Subprogram (Stm);
procedure Analyze_Subprogram_Declaration (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
+ Scop : constant Entity_Id := Current_Scope;
Designator : Entity_Id;
Form : Node_Id;
- Scop : constant Entity_Id := Current_Scope;
Null_Body : Node_Id := Empty;
-- Start of processing for Analyze_Subprogram_Declaration
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);
+ end if;
+
-- For a null procedure, capture the profile before analysis, for
- -- expansion at the freeze point and at each point of call.
- -- The body will only be used if the procedure has preconditions.
- -- In that case the body is analyzed at the freeze point.
+ -- expansion at the freeze point and at each point of call. The body
+ -- will only be used if the procedure has preconditions. In that case
+ -- the body is analyzed at the freeze point.
if Nkind (Specification (N)) = N_Procedure_Specification
and then Null_Present (Specification (N))
Set_Defining_Identifier (Form,
Make_Defining_Identifier (Loc,
Chars (Defining_Identifier (Form))));
+
+ -- Resolve the types of the formals now, because the freeze point
+ -- may appear in a different context, e.g. an instantiation.
+
+ if Nkind (Parameter_Type (Form)) /= N_Access_Definition then
+ Find_Type (Parameter_Type (Form));
+
+ elsif
+ No (Access_To_Subprogram_Definition (Parameter_Type (Form)))
+ then
+ Find_Type (Subtype_Mark (Parameter_Type (Form)));
+
+ else
+
+ -- the case of a null procedure with a formal that is an
+ -- access_to_subprogram type, and that is used as an actual
+ -- in an instantiation is left to the enthusiastic reader.
+
+ null;
+ end if;
+
Next (Form);
end loop;
end if;
end if;
- Designator := Analyze_Subprogram_Specification (Specification (N));
+ Designator := Analyze_Subprogram_Specification (Specification (N));
Generate_Definition (Designator);
+ -- ??? why this call, already in Analyze_Subprogram_Specification
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Location (Sloc (N));
Write_Eol;
end if;
+
+ if Is_Protected_Type (Current_Scope) then
+
+ -- Indicate that this is a protected operation, because it may be
+ -- used in subsequent declarations within the protected type.
+
+ Set_Convention (Designator, Convention_Protected);
+ end if;
+
+ List_Inherited_Pre_Post_Aspects (Designator);
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Designator);
+ end if;
end Analyze_Subprogram_Declaration;
--------------------------------------
-- Start of processing for Analyze_Subprogram_Specification
begin
+ -- User-defined operator is not allowed in SPARK, except as a renaming
+
+ if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
+ and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
+ then
+ Check_SPARK_Restriction ("user-defined operator is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
Generate_Definition (Designator);
+ Set_Contract (Designator, Make_Contract (Sloc (Designator)));
if Nkind (N) = N_Function_Specification then
Set_Ekind (Designator, E_Function);
Set_Mechanism (Designator, Default_Mechanism);
-
else
Set_Ekind (Designator, E_Procedure);
Set_Etype (Designator, Standard_Void_Type);
elsif Nkind (N) = N_Function_Specification then
Push_Scope (Designator);
-
Analyze_Return_Type (N);
-
End_Scope;
end if;
+ -- Function case
+
if Nkind (N) = N_Function_Specification then
+
+ -- Deal with operator symbol case
+
if Nkind (Designator) = N_Defining_Operator_Symbol then
Valid_Operator_Definition (Designator);
end if;
Error_Msg_N
("function that returns abstract type must be abstract", N);
- -- Ada 2012 (AI-0073): extend this test to subprograms with an
+ -- Ada 2012 (AI-0073): Extend this test to subprograms with an
-- access result whose designated type is abstract.
elsif Nkind (Result_Definition (N)) = N_Access_Definition
-- Ada 2005 (AI-231): In case of anonymous access types check
-- the null-exclusion and access-to-constant attributes must
- -- match.
+ -- match. For null exclusion, we test the types rather than the
+ -- formals themselves, since the attribute is only set reliably
+ -- on the formals in the Ada 95 case, and we exclude the case
+ -- where Old_Formal is marked as controlling, to avoid errors
+ -- when matching completing bodies with dispatching declarations
+ -- (access formals in the bodies aren't marked Can_Never_Be_Null).
if Ada_Version >= Ada_2005
and then Ekind (Etype (Old_Formal)) = E_Anonymous_Access_Type
and then Ekind (Etype (New_Formal)) = E_Anonymous_Access_Type
and then
- (Can_Never_Be_Null (Old_Formal) /=
- Can_Never_Be_Null (New_Formal)
+ ((Can_Never_Be_Null (Etype (Old_Formal)) /=
+ Can_Never_Be_Null (Etype (New_Formal))
+ and then
+ not Is_Controlling_Formal (Old_Formal))
or else
Is_Access_Constant (Etype (Old_Formal)) /=
Is_Access_Constant (Etype (New_Formal)))
Error_Msg_Sloc := Sloc (Op);
if Comes_From_Source (Op) or else No (Alias (Op)) then
- if not Is_Overriding_Operation (Op) then
+ if not Present (Overridden_Operation (Op)) then
Error_Msg_N ("\\primitive % defined #", Typ);
else
Error_Msg_N
elsif Ekind (T) = E_Incomplete_Type and then From_With_Type (T) then
Set_Has_Delayed_Freeze (Designator);
+
+ -- AI05-0151: In Ada 2012, Incomplete types can appear in the profile
+ -- of a subprogram or entry declaration.
+
+ elsif Ekind (T) = E_Incomplete_Type
+ and then Ada_Version >= Ada_2012
+ then
+ Set_Has_Delayed_Freeze (Designator);
end if;
end Possible_Freeze;
-- Start of processing for Check_Delayed_Subprogram
begin
- -- Never need to freeze abstract subprogram
-
- if Ekind (Designator) /= E_Subprogram_Type
- and then Is_Abstract_Subprogram (Designator)
- then
- null;
- else
- -- Need delayed freeze if return type itself needs a delayed
- -- freeze and is not yet frozen.
+ -- All subprograms, including abstract subprograms, may need a freeze
+ -- node if some formal type or the return type needs one.
- Possible_Freeze (Etype (Designator));
- Possible_Freeze (Base_Type (Etype (Designator))); -- needed ???
+ Possible_Freeze (Etype (Designator));
+ Possible_Freeze (Base_Type (Etype (Designator))); -- needed ???
- -- Need delayed freeze if any of the formal types themselves need
- -- a delayed freeze and are not yet frozen.
+ -- Need delayed freeze if any of the formal types themselves need
+ -- a delayed freeze and are not yet frozen.
- F := First_Formal (Designator);
- while Present (F) loop
- Possible_Freeze (Etype (F));
- Possible_Freeze (Base_Type (Etype (F))); -- needed ???
- Next_Formal (F);
- end loop;
- end if;
+ F := First_Formal (Designator);
+ while Present (F) loop
+ Possible_Freeze (Etype (F));
+ Possible_Freeze (Base_Type (Etype (F))); -- needed ???
+ Next_Formal (F);
+ end loop;
-- Mark functions that return by reference. Note that it cannot be
-- done for delayed_freeze subprograms because the underlying
-- Grouping (use of comma in param lists) must be the same
-- This is where we catch a misconformance like:
- -- A,B : Integer
+ -- A, B : Integer
-- A : Integer; B : Integer
-- which are represented identically in the tree except
and then (not Is_Hidden (Overridden_Subp)
or else
((Chars (Overridden_Subp) = Name_Initialize
- or else Chars (Overridden_Subp) = Name_Adjust
- or else Chars (Overridden_Subp) = Name_Finalize)
- and then Present (Alias (Overridden_Subp))
- and then not Is_Hidden (Alias (Overridden_Subp))))
+ or else
+ Chars (Overridden_Subp) = Name_Adjust
+ or else
+ Chars (Overridden_Subp) = Name_Finalize)
+ and then Present (Alias (Overridden_Subp))
+ and then not Is_Hidden (Alias (Overridden_Subp))))
then
if Must_Not_Override (Spec) then
Error_Msg_Sloc := Sloc (Overridden_Subp);
end if;
elsif Is_Subprogram (Subp) then
- Set_Is_Overriding_Operation (Subp);
+ if Is_Init_Proc (Subp) then
+ null;
+
+ elsif No (Overridden_Operation (Subp)) then
+
+ -- For entities generated by Derive_Subprograms the overridden
+ -- operation is the inherited primitive (which is available
+ -- through the attribute alias)
+
+ if (Is_Dispatching_Operation (Subp)
+ or else Is_Dispatching_Operation (Overridden_Subp))
+ and then not Comes_From_Source (Overridden_Subp)
+ and then Find_Dispatching_Type (Overridden_Subp) =
+ Find_Dispatching_Type (Subp)
+ and then Present (Alias (Overridden_Subp))
+ and then Comes_From_Source (Alias (Overridden_Subp))
+ then
+ Set_Overridden_Operation (Subp, Alias (Overridden_Subp));
+
+ else
+ Set_Overridden_Operation (Subp, Overridden_Subp);
+ end if;
+ end if;
end if;
-- If primitive flag is set or this is a protected operation, then
-- explicit overridden operation.
elsif Nkind (Subp) = N_Defining_Operator_Symbol then
- declare
- Typ : constant Entity_Id :=
- Base_Type (Etype (First_Formal (Subp)));
-
- Can_Override : constant Boolean :=
- Operator_Matches_Spec (Subp, Subp)
- and then Scope (Subp) = Scope (Typ)
- and then not Is_Class_Wide_Type (Typ);
-
- begin
- if Must_Not_Override (Spec) then
-
- -- If this is not a primitive or a protected subprogram, then
- -- "not overriding" is illegal.
-
- if not Is_Primitive
- and then Ekind (Scope (Subp)) /= E_Protected_Type
- then
- Error_Msg_N
- ("overriding indicator only allowed "
- & "if subprogram is primitive", Subp);
+ if Must_Not_Override (Spec) then
- elsif Can_Override then
- Error_Msg_NE
- ("subprogram& overrides predefined operator ", Spec, Subp);
- end if;
+ -- If this is not a primitive or a protected subprogram, then
+ -- "not overriding" is illegal.
- elsif Must_Override (Spec) then
- if Is_Overriding_Operation (Subp) then
- null;
+ if not Is_Primitive
+ and then Ekind (Scope (Subp)) /= E_Protected_Type
+ then
+ Error_Msg_N
+ ("overriding indicator only allowed "
+ & "if subprogram is primitive", Subp);
- elsif not Can_Override then
- Error_Msg_NE ("subprogram & is not overriding", Spec, Subp);
- end if;
+ elsif Can_Override_Operator (Subp) then
+ Error_Msg_NE
+ ("subprogram& overrides predefined operator ", Spec, Subp);
+ end if;
- elsif not Error_Posted (Subp)
- and then Style_Check
- and then Can_Override
- and then
- not Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Subp)))
+ elsif Must_Override (Spec) then
+ if No (Overridden_Operation (Subp))
+ and then not Can_Override_Operator (Subp)
then
- Set_Is_Overriding_Operation (Subp);
+ Error_Msg_NE ("subprogram & is not overriding", Spec, Subp);
+ end if;
- -- If style checks are enabled, indicate that the indicator is
- -- missing. However, at the point of declaration, the type of
- -- which this is a primitive operation may be private, in which
- -- case the indicator would be premature.
+ elsif not Error_Posted (Subp)
+ and then Style_Check
+ and then Can_Override_Operator (Subp)
+ and then
+ not Is_Predefined_File_Name
+ (Unit_File_Name (Get_Source_Unit (Subp)))
+ then
+ -- If style checks are enabled, indicate that the indicator is
+ -- missing. However, at the point of declaration, the type of
+ -- which this is a primitive operation may be private, in which
+ -- case the indicator would be premature.
- if Has_Private_Declaration (Etype (Subp))
- or else Has_Private_Declaration (Etype (First_Formal (Subp)))
- then
- null;
- else
- Style.Missing_Overriding (Decl, Subp);
- end if;
+ if Has_Private_Declaration (Etype (Subp))
+ or else Has_Private_Declaration (Etype (First_Formal (Subp)))
+ then
+ null;
+ else
+ Style.Missing_Overriding (Decl, Subp);
end if;
- end;
+ end if;
elsif Must_Override (Spec) then
if Ekind (Subp) = E_Entry then
(New_Id, Old_Id, Type_Conformant, True, Result, Err_Loc);
end Check_Type_Conformant;
+ ---------------------------
+ -- Can_Override_Operator --
+ ---------------------------
+
+ function Can_Override_Operator (Subp : Entity_Id) return Boolean is
+ Typ : Entity_Id;
+ begin
+ if Nkind (Subp) /= N_Defining_Operator_Symbol then
+ return False;
+
+ else
+ Typ := Base_Type (Etype (First_Formal (Subp)));
+
+ return Operator_Matches_Spec (Subp, Subp)
+ and then Scope (Subp) = Scope (Typ)
+ and then not Is_Class_Wide_Type (Typ);
+ end if;
+ end Can_Override_Operator;
+
----------------------
-- Conforming_Types --
----------------------
end if;
Desig_1 := Find_Designated_Type (Type_1);
-
Desig_2 := Find_Designated_Type (Type_2);
-- If the context is an instance association for a formal
-- of an incomplete Class_Wide_Type are illegal.
if Is_Class_Wide_Type (Desig_1)
- and then Is_Class_Wide_Type (Desig_2)
+ and then
+ Is_Class_Wide_Type (Desig_2)
then
return
Conforming_Types
Formal_Type := Underlying_Type (Formal_Type);
end if;
+ -- Suppress the extra formal if formal's subtype is constrained or
+ -- indefinite, or we're compiling for Ada 2012 and the underlying
+ -- type is tagged and limited. In Ada 2012, a limited tagged type
+ -- can have defaulted discriminants, but 'Constrained is required
+ -- to return True, so the formal is never needed (see AI05-0214).
+ -- Note that this ensures consistency of calling sequences for
+ -- dispatching operations when some types in a class have defaults
+ -- on discriminants and others do not (and requiring the extra
+ -- formal would introduce distributed overhead).
+
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)))
then
Set_Extra_Constrained
(Formal, Add_Extra_Formal (Formal, Standard_Boolean, E, "O"));
E, BIP_Formal_Suffix (BIP_Alloc_Form));
end if;
- -- For functions whose result type has controlled parts, we have
- -- an extra formal of type System.Finalization_Implementation.
- -- Finalizable_Ptr_Ptr. That is, we are passing a pointer to a
- -- finalization list (which is itself a pointer). This extra
- -- formal is then passed along to Move_Final_List in case of
- -- successful completion of a return statement. We cannot pass an
- -- 'in out' parameter, because we need to update the finalization
- -- list during an abort-deferred region, rather than using
- -- copy-back after the function returns. This is true even if we
- -- are able to get away with having 'in out' parameters, which are
- -- normally illegal for functions. This formal is also needed when
- -- the function has a tagged result.
-
- if Needs_BIP_Final_List (E) then
+ -- In the case of functions whose result type needs finalization,
+ -- add an extra formal which represents the finalization master.
+
+ if Needs_BIP_Finalization_Master (E) then
Discard :=
Add_Extra_Formal
- (E, RTE (RE_Finalizable_Ptr_Ptr),
- E, BIP_Formal_Suffix (BIP_Final_List));
+ (E, RTE (RE_Finalization_Master_Ptr),
+ E, BIP_Formal_Suffix (BIP_Finalization_Master));
end if;
-- If the result type contains tasks, we have two extra formals:
E := Homonym (E);
exit when No (E);
- -- Warn unless genuine overloading
+ -- Warn unless genuine overloading. Do not emit warning on
+ -- hiding predefined operators in Standard (these are either an
+ -- (artifact of our implicit declarations, or simple noise) but
+ -- keep warning on a operator defined on a local subtype, because
+ -- of the real danger that different operators may be applied in
+ -- various parts of the program.
- if (not Is_Overloadable (E) or else Subtype_Conformant (E, S))
+ -- Note that if E and S have the same scope, there is never any
+ -- hiding. Either the two conflict, and the program is illegal,
+ -- or S is overriding an implicit inherited subprogram.
+
+ if Scope (E) /= Scope (S)
+ and then (not Is_Overloadable (E)
+ or else Subtype_Conformant (E, S))
and then (Is_Immediately_Visible (E)
or else
Is_Potentially_Use_Visible (S))
then
- Error_Msg_Sloc := Sloc (E);
- Error_Msg_N ("declaration of & hides one#?", S);
+ if Scope (E) /= Standard_Standard then
+ Error_Msg_Sloc := Sloc (E);
+ Error_Msg_N ("declaration of & hides one#?", S);
+
+ elsif Nkind (S) = N_Defining_Operator_Symbol
+ and then
+ Scope (Base_Type (Etype (First_Formal (S)))) /= Scope (S)
+ then
+ Error_Msg_N
+ ("declaration of & hides predefined operator?", S);
+ end if;
end if;
end loop;
end if;
and then Is_Record_Type (Typ)
and then not 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
- Error_Msg_NE
- ("equality operator must be declared "
- & "before type& is frozen", Eq_Op, Typ);
+ if Ekind (Scope (Typ)) /= E_Package
+ or else Scope (Typ) /= Current_Scope
+ then
+ null;
- 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 ('R'M 4.5.2 (9.8)) (Ada 2012))?", Obj_Decl);
- exit;
- end if;
+ elsif Is_Generic_Actual_Type (Typ) then
+ null;
- Next (Obj_Decl);
- end loop;
+ elsif In_Package_Body (Scope (Typ)) 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);
+
+ else
+ Error_Msg_NE
+ ("equality operator must be declared "
+ & "before type& is frozen", Eq_Op, Typ);
+
+ 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);
+ exit;
+ end if;
+
+ Next (Obj_Decl);
+ end loop;
+ end if;
elsif not In_Same_List (Parent (Typ), Decl)
and then not Is_Limited_Type (Typ)
then
+
+ -- This makes it illegal to have a primitive equality declared in
+ -- the private part if the type is visible.
+
Error_Msg_N ("equality operator appears too late", Eq_Op);
end if;
end if;
if In_Instance then
Set_Convention (Designator, Convention (E));
- if Nkind (N) = N_Subprogram_Body
+ -- Skip past subprogram bodies and subprogram renamings that
+ -- may appear to have a matching spec, but that aren't fully
+ -- conformant with it. That can occur in cases where an
+ -- actual type causes unrelated homographs in the instance.
+
+ if Nkind_In (N, N_Subprogram_Body,
+ N_Subprogram_Renaming_Declaration)
and then Present (Homonym (E))
- and then not Fully_Conformant (E, Designator)
+ and then not Fully_Conformant (Designator, E)
then
goto Next_Entity;
- elsif not Subtype_Conformant (E, Designator) then
+ elsif not Subtype_Conformant (Designator, E) then
goto Next_Entity;
end if;
end if;
- if not Has_Completion (E) then
+ -- 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.
+
+ if not (Comes_From_Source (E))
+ and then Is_Null_Procedure (E)
+ and then not Mode_Conformant (Designator, E)
+ then
+ null;
+
+ elsif not Has_Completion (E) then
if Nkind (N) /= N_Subprogram_Body_Stub then
Set_Corresponding_Spec (N, E);
end if;
-- If the body already exists, then this is an error unless
-- the previous declaration is the implicit declaration of a
- -- derived subprogram, or this is a spurious overloading in an
- -- instance.
+ -- derived subprogram. It is also legal for an instance to
+ -- contain type conformant overloadable declarations (but the
+ -- generic declaration may not), per 8.3(26/2).
elsif No (Alias (E))
and then not Is_Intrinsic_Subprogram (E)
and then
FCE (Expression (E1), Expression (E2));
+ when N_Quantified_Expression =>
+ if not FCE (Condition (E1), Condition (E2)) then
+ return False;
+ end if;
+
+ if Present (Loop_Parameter_Specification (E1))
+ and then Present (Loop_Parameter_Specification (E2))
+ then
+ declare
+ L1 : constant Node_Id :=
+ Loop_Parameter_Specification (E1);
+ L2 : constant Node_Id :=
+ Loop_Parameter_Specification (E2);
+
+ begin
+ return
+ Reverse_Present (L1) = Reverse_Present (L2)
+ and then
+ FCE (Defining_Identifier (L1),
+ Defining_Identifier (L2))
+ and then
+ FCE (Discrete_Subtype_Definition (L1),
+ Discrete_Subtype_Definition (L2));
+ end;
+
+ else -- quantified expression with an iterator
+ declare
+ I1 : constant Node_Id := Iterator_Specification (E1);
+ I2 : constant Node_Id := Iterator_Specification (E2);
+
+ begin
+ return
+ FCE (Defining_Identifier (I1),
+ Defining_Identifier (I2))
+ and then
+ Of_Present (I1) = Of_Present (I2)
+ and then
+ Reverse_Present (I1) = Reverse_Present (I2)
+ and then FCE (Name (I1), Name (I2))
+ and then FCE (Subtype_Indication (I1),
+ Subtype_Indication (I2));
+ end;
+ end if;
+
when N_Range =>
return
FCE (Low_Bound (E1), Low_Bound (E2))
Iface : constant Entity_Id := Find_Dispatching_Type (Iface_Prim);
Typ : constant Entity_Id := Find_Dispatching_Type (Prim);
+ function Controlling_Formal (Prim : Entity_Id) return Entity_Id;
+ -- Return the controlling formal of Prim
+
+ ------------------------
+ -- Controlling_Formal --
+ ------------------------
+
+ function Controlling_Formal (Prim : Entity_Id) return Entity_Id is
+ E : Entity_Id := First_Entity (Prim);
+
+ begin
+ while Present (E) loop
+ if Is_Formal (E) and then Is_Controlling_Formal (E) then
+ return E;
+ end if;
+
+ Next_Entity (E);
+ end loop;
+
+ return Empty;
+ end Controlling_Formal;
+
+ -- Local variables
+
+ Iface_Ctrl_F : constant Entity_Id := Controlling_Formal (Iface_Prim);
+ Prim_Ctrl_F : constant Entity_Id := Controlling_Formal (Prim);
+
+ -- Start of processing for Is_Interface_Conformant
+
begin
pragma Assert (Is_Subprogram (Iface_Prim)
and then Is_Subprogram (Prim)
then
return False;
- -- Case of a procedure, or a function that does not have a controlling
- -- result (I or access I).
+ -- 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)
+ then
+ return False;
+
+ -- Case of a procedure, or a function whose result type matches the
+ -- result type of the interface primitive, or a function that has no
+ -- controlling result (I or access I).
elsif Ekind (Iface_Prim) = E_Procedure
or else Etype (Prim) = Etype (Iface_Prim)
end if;
end Is_Non_Overriding_Operation;
+ -------------------------------------
+ -- List_Inherited_Pre_Post_Aspects --
+ -------------------------------------
+
+ procedure List_Inherited_Pre_Post_Aspects (E : Entity_Id) is
+ begin
+ if Opt.List_Inherited_Aspects
+ and then (Is_Subprogram (E) or else Is_Generic_Subprogram (E))
+ then
+ declare
+ Inherited : constant Subprogram_List :=
+ Inherited_Subprograms (E);
+ P : Node_Id;
+
+ begin
+ for J in Inherited'Range loop
+ P := Spec_PPC_List (Contract (Inherited (J)));
+
+ while Present (P) loop
+ Error_Msg_Sloc := Sloc (P);
+
+ if Class_Present (P) and then not Split_PPC (P) then
+ if Pragma_Name (P) = Name_Precondition then
+ Error_Msg_N
+ ("?info: & inherits `Pre''Class` aspect from #", E);
+ else
+ Error_Msg_N
+ ("?info: & inherits `Post''Class` aspect from #", E);
+ end if;
+ end if;
+
+ P := Next_Pragma (P);
+ end loop;
+ end loop;
+ end;
+ end if;
+ end List_Inherited_Pre_Post_Aspects;
+
------------------------------
-- Make_Inequality_Operator --
------------------------------
In_Scope := True;
-- The enclosing scope is not a synchronized type and the subprogram
- -- has no formals
+ -- has no formals.
elsif No (First_Formal (Def_Id)) then
return;
-- The subprogram has formals and hence it may be a primitive of a
- -- concurrent type
+ -- concurrent type.
else
Typ := Etype (First_Formal (Def_Id));
Subp : Entity_Id := Empty;
begin
- -- Traverse the homonym chain, looking at a potentially
+ -- Traverse the homonym chain, looking for a potentially
-- overridden subprogram that belongs to an implemented
-- interface.
null;
-- Entries and procedures can override abstract or null
- -- interface procedures
+ -- interface procedures.
elsif (Ekind (Def_Id) = E_Procedure
or else Ekind (Def_Id) = E_Entry)
Hom := Homonym (Hom);
end loop;
- -- After examining all candidates for overriding, we are
- -- left with the best match which is a mode incompatible
- -- interface routine. Do not emit an error if the Expander
- -- is active since this error will be detected later on
- -- after all concurrent types are expanded and all wrappers
- -- are built. This check is meant for spec-only
- -- compilations.
+ -- After examining all candidates for overriding, we are left with
+ -- the best match which is a mode incompatible interface routine.
+ -- Do not emit an error if the Expander is active since this error
+ -- will be detected later on after all concurrent types are
+ -- expanded and all wrappers are built. This check is meant for
+ -- spec-only compilations.
- if Present (Candidate)
- and then not Expander_Active
- then
+ if Present (Candidate) and then not Expander_Active then
Iface_Typ :=
Find_Parameter_Type (Parent (First_Formal (Candidate)));
- -- Def_Id is primitive of a protected type, declared
- -- inside the type, and the candidate is primitive of a
- -- limited or synchronized interface.
+ -- Def_Id is primitive of a protected type, declared inside the
+ -- type, and the candidate is primitive of a limited or
+ -- synchronized interface.
if In_Scope
and then Is_Protected_Type (Typ)
or else Is_Synchronized_Interface (Iface_Typ)
or else Is_Task_Interface (Iface_Typ))
then
- -- Must reword this message, comma before to in -gnatj
- -- mode ???
-
Error_Msg_NE
("first formal of & must be of mode `OUT`, `IN OUT`"
& " or access-to-variable", Typ, Candidate);
Error_Msg_N
- ("\to be overridden by protected procedure or entry "
- & "(RM 9.4(11.9/2))", Typ);
+ ("\in order to be overridden by protected procedure or "
+ & "entry (RM 9.4(11.9/2))", Typ);
end if;
end if;
-- Inside_Freeze_Actions is non zero when S corresponds with an
-- internal entity that links an interface primitive with its
-- covering primitive through attribute Interface_Alias (see
- -- Add_Internal_Interface_Entities)
+ -- Add_Internal_Interface_Entities).
if Inside_Freezing_Actions = 0
and then Is_Package_Or_Generic_Package (Current_Scope)
if Comes_From_Source (S) then
Check_Synchronized_Overriding (S, Overridden_Subp);
+
+ -- (Ada 2012: AI05-0125-1): If S is a dispatching operation then
+ -- it may have overridden some hidden inherited primitive. Update
+ -- Overridden_Subp to avoid spurious errors when checking the
+ -- overriding indicator.
+
+ if Ada_Version >= Ada_2012
+ and then No (Overridden_Subp)
+ and then Is_Dispatching_Operation (S)
+ and then Present (Overridden_Operation (S))
+ then
+ Overridden_Subp := Overridden_Operation (S);
+ end if;
+
Check_Overriding_Indicator
(S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
end if;
-- dispatch table anyway, because it can be dispatched to even if it
-- cannot be called directly.
- elsif Present (Alias (S))
- and then not Comes_From_Source (S)
- then
+ elsif Present (Alias (S)) and then not Comes_From_Source (S) then
Set_Scope (S, Current_Scope);
if Is_Dispatching_Operation (Alias (S)) then
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.
+
+ elsif not Comes_From_Source (S)
+ and then Is_Null_Procedure (S)
+ and then not Mode_Conformant (E, S)
+ then
+ null;
+
-- Check if we have type conformance
elsif Type_Conformant (E, S) then
Check_Operation_From_Private_View (S, E);
end if;
- -- In any case the implicit operation remains hidden by
- -- the existing declaration, which is overriding.
+ -- In any case the implicit operation remains hidden by the
+ -- existing declaration, which is overriding. Indicate that
+ -- E overrides the operation from which S is inherited.
- Set_Is_Overriding_Operation (E);
+ if Present (Alias (S)) then
+ Set_Overridden_Operation (E, Alias (S));
+ else
+ Set_Overridden_Operation (E, S);
+ end if;
if Comes_From_Source (E) then
Check_Overriding_Indicator (E, S, Is_Primitive => False);
-
- -- Indicate that E overrides the operation from which
- -- S is inherited.
-
- if Present (Alias (S)) then
- Set_Overridden_Operation (E, Alias (S));
- else
- Set_Overridden_Operation (E, S);
- end if;
end if;
return;
if No (Next_Entity (Prev)) then
Set_Last_Entity (Current_Scope, Prev);
end if;
-
end if;
end if;
Enter_Overloaded_Entity (S);
- Set_Is_Overriding_Operation (S);
+
+ -- For entities generated by Derive_Subprograms the
+ -- overridden operation is the inherited primitive
+ -- (which is available through the attribute alias).
+
+ if not (Comes_From_Source (E))
+ and then Is_Dispatching_Operation (E)
+ and then Find_Dispatching_Type (E) =
+ Find_Dispatching_Type (S)
+ and then Present (Alias (E))
+ and then Comes_From_Source (Alias (E))
+ then
+ Set_Overridden_Operation (S, Alias (E));
+
+ -- Normal case of setting entity as overridden
+
+ -- Note: Static_Initialization and Overridden_Operation
+ -- attributes use the same field in subprogram entities.
+ -- Static_Initialization is only defined for internal
+ -- initialization procedures, where Overridden_Operation
+ -- is irrelevant. Therefore the setting of this attribute
+ -- must check whether the target is an init_proc.
+
+ elsif not Is_Init_Proc (S) then
+ Set_Overridden_Operation (S, E);
+ end if;
+
Check_Overriding_Indicator (S, E, Is_Primitive => True);
-- If S is a user-defined subprogram or a null procedure
- -- expanded to override an inherited null procedure, then
- -- indicate that E overrides the operation from which S
- -- is inherited. It seems odd that Overridden_Operation
- -- isn't set in all cases where Is_Overriding_Operation
- -- is true, but doing so causes infinite loops in the
- -- compiler for implicit overriding subprograms. ???
+ -- expanded to override an inherited null procedure, or a
+ -- predefined dispatching primitive then indicate that E
+ -- overrides the operation from which S is inherited.
if Comes_From_Source (S)
or else
Nkind (Parent (S)) = N_Procedure_Specification
and then
Null_Present (Parent (S)))
+ or else
+ (Present (Alias (E))
+ and then
+ Is_Predefined_Dispatching_Operation (Alias (E)))
then
if Present (Alias (E)) then
Set_Overridden_Operation (S, Alias (E));
- else
- Set_Overridden_Operation (S, E);
end if;
end if;
if Is_Dispatching_Operation (E) then
-- An overriding dispatching subprogram inherits the
- -- convention of the overridden subprogram (by
- -- AI-117).
+ -- convention of the overridden subprogram (AI-117).
Set_Convention (S, Convention (E));
Check_Dispatching_Operation (S, E);
Check_Overriding_Indicator
(S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
+ -- Overloading is not allowed in SPARK, except for operators
+
+ if Nkind (S) /= N_Defining_Operator_Symbol then
+ Error_Msg_Sloc := Sloc (Homonym (S));
+ Check_SPARK_Restriction
+ ("overloading not allowed with entity#", S);
+ end if;
+
-- If S is a derived operation for an untagged type then by
-- definition it's not a dispatching operation (even if the parent
- -- operation was dispatching), so we don't call
- -- Check_Dispatching_Operation in that case.
+ -- operation was dispatching), so Check_Dispatching_Operation is not
+ -- called in that case.
if No (Derived_Type)
or else Is_Tagged_Type (Derived_Type)
begin
return Is_Class_Wide_Type (Designated_Type (Etype (D)))
or else (Nkind (D) = N_Attribute_Reference
- and then Attribute_Name (D) = Name_Access
- and then Is_Class_Wide_Type (Etype (Prefix (D))));
+ and then Attribute_Name (D) = Name_Access
+ and then Is_Class_Wide_Type (Etype (Prefix (D))));
end Is_Class_Wide_Default;
-- Start of processing for Process_Formals
if Is_Tagged_Type (Formal_Type) then
if Ekind (Scope (Current_Scope)) = E_Package
- and then In_Private_Part (Scope (Current_Scope))
and then not From_With_Type (Formal_Type)
and then not Is_Class_Wide_Type (Formal_Type)
then
Append_Elmt
(Current_Scope,
Private_Dependents (Base_Type (Formal_Type)));
+
+ -- Freezing is delayed to ensure that Register_Prim
+ -- will get called for this operation, which is needed
+ -- in cases where static dispatch tables aren't built.
+ -- (Note that the same is done for controlling access
+ -- parameter cases in function Access_Definition.)
+
+ Set_Has_Delayed_Freeze (Current_Scope);
end if;
end if;
elsif not Nkind_In (Parent (T), N_Access_Function_Definition,
N_Access_Procedure_Definition)
then
- Error_Msg_NE
- ("invalid use of incomplete type&",
- Param_Spec, Formal_Type);
- -- Further checks on the legality of incomplete types
- -- in formal parts must be delayed until the freeze point
- -- of the enclosing subprogram or access to subprogram.
+ -- AI05-0151: Tagged incomplete types are allowed in all
+ -- formal parts. Untagged incomplete types are not allowed
+ -- in bodies.
+
+ if Ada_Version >= Ada_2012 then
+ if Is_Tagged_Type (Formal_Type) then
+ null;
+
+ elsif Nkind_In (Parent (Parent (T)), N_Accept_Statement,
+ N_Entry_Body,
+ N_Subprogram_Body)
+ then
+ Error_Msg_NE
+ ("invalid use of untagged incomplete type&",
+ Ptype, Formal_Type);
+ end if;
+
+ else
+ Error_Msg_NE
+ ("invalid use of incomplete type&",
+ Param_Spec, Formal_Type);
+
+ -- Further checks on the legality of incomplete types
+ -- in formal parts are delayed until the freeze point
+ -- of the enclosing subprogram or access to subprogram.
+ end if;
end if;
elsif Ekind (Formal_Type) = E_Void then
- Error_Msg_NE ("premature use of&",
- Parameter_Type (Param_Spec), Formal_Type);
+ Error_Msg_NE
+ ("premature use of&",
+ Parameter_Type (Param_Spec), Formal_Type);
end if;
-- Ada 2005 (AI-231): Create and decorate an internal subtype
then
Error_Msg_NE
("`NOT NULL` not allowed (& already excludes null)",
- Param_Spec,
- Formal_Type);
+ Param_Spec, Formal_Type);
end if;
Formal_Type :=
end if;
Set_Etype (Formal, Formal_Type);
+
Default := Expression (Param_Spec);
if Present (Default) then
+ Check_SPARK_Restriction
+ ("default expression is not allowed", Default);
+
if Out_Present (Param_Spec) then
Error_Msg_N
("default initialization only allowed for IN parameters",
-- Now set the kind (mode) of each formal
Param_Spec := First (T);
-
while Present (Param_Spec) loop
Formal := Defining_Identifier (Param_Spec);
Set_Formal_Mode (Formal);
is
Loc : constant Source_Ptr := Sloc (N);
Prag : Node_Id;
- Plist : List_Id := No_List;
- Subp : Entity_Id;
Parms : List_Id;
- function Grab_PPC (Nam : Name_Id) 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. The
- -- argument Nam is either Name_Precondition or Name_Postcondition.
+ 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
+
+ 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.
+
+ 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.
--------------
-- Grab_PPC --
--------------
- function Grab_PPC (Nam : Name_Id) return Node_Id is
- CP : constant Node_Id := New_Copy_Tree (Prag);
+ function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id is
+ Nam : constant Name_Id := Pragma_Name (Prag);
+ Map : Elist_Id;
+ CP : Node_Id;
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.
- Set_Analyzed (CP, False);
-
if Nam = Name_Postcondition
and then not Expander_Active
then
return CP;
end if;
- -- Change pragma into corresponding pragma Check
+ -- Change copy of pragma into corresponding pragma Check
Prepend_To (Pragma_Argument_Associations (CP),
Make_Pragma_Argument_Association (Sloc (Prag),
- Expression =>
- Make_Identifier (Loc,
- Chars => Nam)));
- Set_Pragma_Identifier (CP,
- Make_Identifier (Sloc (Prag),
- Chars => Name_Check));
+ Expression => Make_Identifier (Loc, Nam)));
+ 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;
+ --------------------------------------
+ -- Invariants_Or_Predicates_Present --
+ --------------------------------------
+
+ function Invariants_Or_Predicates_Present return Boolean is
+ Formal : Entity_Id;
+
+ begin
+ -- Check function return result
+
+ if Ekind (Designator) /= E_Procedure
+ and then Has_Invariants (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;
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+
+ return False;
+ end Invariants_Or_Predicates_Present;
+
-- Start of processing for Process_PPCs
begin
- -- Nothing to do if we are not generating code
+ -- Capture designator from spec if present, else from body
- if Operating_Mode /= Generate_Code then
- return;
+ if Present (Spec_Id) then
+ Designator := Spec_Id;
+ else
+ Designator := Body_Id;
end if;
-- Grab preconditions from spec
-- the body will be analyzed and converted when we scan the body
-- declarations below.
- Prag := Spec_PPC_List (Spec_Id);
+ Prag := Spec_PPC_List (Contract (Spec_Id));
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Pragma_Enabled (Prag)
- then
- -- Add pragma Check at the start of the declarations of N.
- -- 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.
-
- Prepend (Grab_PPC (Name_Precondition), Declarations (N));
+ 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
-- 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
Analyze (Prag);
- -- If expansion is disabled, as in a generic unit,
- -- save pragma for later expansion.
+ -- If expansion is disabled, as in a generic unit, save
+ -- pragma for later expansion.
if not Expander_Active then
- Prepend (Grab_PPC (Name_Postcondition), Declarations (N));
+ Prepend (Grab_PPC, Declarations (N));
else
- Append (Grab_PPC (Name_Postcondition), Plist);
+ Append (Grab_PPC, Plist);
end if;
end if;
-- Now deal with any postconditions from the spec
if Present (Spec_Id) then
+ Spec_Postconditions : declare
+ 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_Post_Conditions --
+ -----------------------------
+
+ procedure Process_Post_Conditions
+ (Spec : Node_Id;
+ Class : Boolean)
+ is
+ Pspec : Node_Id;
- -- Loop through PPC pragmas from spec
-
- Prag := Spec_PPC_List (Spec_Id);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Postcondition
- and then Pragma_Enabled (Prag)
- then
- if Plist = No_List then
- Plist := Empty_List;
- end if;
-
- if not Expander_Active then
- Prepend (Grab_PPC (Name_Postcondition), Declarations (N));
+ begin
+ if Class then
+ Pspec := Spec;
else
- Append (Grab_PPC (Name_Postcondition), Plist);
+ 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
+ if Present (Spec_PPC_List (Contract (Spec_Id))) then
+ Process_Post_Conditions (Spec_Id, Class => False);
end if;
- Prag := Next_Pragma (Prag);
- end loop;
+ -- 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, build
- -- the _Postconditions procedure.
+ -- If we had any postconditions and expansion is enabled, or if the
+ -- procedure has invariants, then build the _Postconditions procedure.
- if Present (Plist)
+ if (Present (Plist) or else Invariants_Or_Predicates_Present)
and then Expander_Active
then
- Subp := Defining_Entity (N);
+ if No (Plist) then
+ Plist := Empty_List;
+ end if;
+
+ -- Special processing for function case
+
+ if Ekind (Designator) /= E_Procedure then
+ declare
+ Rent : constant Entity_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => 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
+
+ if Has_Invariants (Etype (Rent))
+ and then Present (Invariant_Procedure (Etype (Rent)))
+ then
+ Append_To (Plist,
+ Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
+ end if;
+ end;
+
+ -- Procedure rather than a function
- if Etype (Subp) /= Standard_Void_Type then
- Parms := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc,
- Chars => Name_uResult),
- Parameter_Type => New_Occurrence_Of (Etype (Subp), Loc)));
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 then
+ Ftype := Etype (Formal);
+
+ if Has_Invariants (Ftype)
+ and then Present (Invariant_Procedure (Ftype))
+ then
+ Append_To (Plist,
+ Make_Invariant_Call
+ (New_Occurrence_Of (Formal, Loc)));
+ end if;
+
+ 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);
+ Make_Defining_Identifier (Loc,
+ Chars => Name_uPostconditions);
-- The entity for the _Postconditions procedure
+
begin
Prepend_To (Declarations (N),
Make_Subprogram_Body (Loc,
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 Etype (Subp) = Standard_Void_Type then
- if Present (Spec_Id) then
- Set_Postcondition_Proc (Spec_Id, Post_Proc);
- else
- Set_Postcondition_Proc (Body_Id, Post_Proc);
- end if;
+ if Ekind (Designator) = E_Procedure then
+ Set_Postcondition_Proc (Designator, Post_Proc);
end if;
end;
- if Present (Spec_Id) then
- Set_Has_Postconditions (Spec_Id);
- else
- Set_Has_Postconditions (Body_Id);
- end if;
+ Set_Has_Postconditions (Designator);
end if;
end Process_PPCs;
-------------------------
procedure Set_Actual_Subtypes (N : Node_Id; Subp : Entity_Id) is
- Loc : constant Source_Ptr := Sloc (N);
Decl : Node_Id;
Formal : Entity_Id;
T : Entity_Id;
if Present (First_Stmt) then
Insert_List_Before_And_Analyze (First_Stmt,
- Freeze_Entity (Defining_Identifier (Decl), Loc));
+ Freeze_Entity (Defining_Identifier (Decl), N));
end if;
if Nkind (N) = N_Accept_Statement
if Ekind (Scope (Formal_Id)) = E_Function
or else Ekind (Scope (Formal_Id)) = E_Generic_Function
then
- Error_Msg_N ("functions can only have IN parameters", Spec);
- Set_Ekind (Formal_Id, E_In_Parameter);
+ -- [IN] OUT parameters allowed for functions in Ada 2012
+
+ if Ada_Version >= Ada_2012 then
+ if In_Present (Spec) then
+ Set_Ekind (Formal_Id, E_In_Out_Parameter);
+ else
+ Set_Ekind (Formal_Id, E_Out_Parameter);
+ end if;
+
+ -- But not in earlier versions of Ada
+
+ else
+ Error_Msg_N ("functions can only have IN parameters", Spec);
+ Set_Ekind (Formal_Id, E_In_Parameter);
+ end if;
elsif In_Present (Spec) then
Set_Ekind (Formal_Id, E_In_Out_Parameter);
projects / gcc.git / blobdiff