-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2019, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2020, 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- --
Analyze_Subprogram_Specification (Specification (N));
begin
- Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
-
Generate_Definition (Subp_Id);
-- Set the SPARK mode from the current context (may be overwritten later
-- Once the aspects of the generated body have been analyzed, create
-- a copy for ASIS purposes and associate it with the original node.
+ -- Is this still needed???
if Has_Aspects (N) then
Set_Aspect_Specifications (Orig_N,
-- Once the aspects of the generated spec have been analyzed, create
-- a copy for ASIS purposes and associate it with the original node.
+ -- Is this still needed???
if Has_Aspects (N) then
Set_Aspect_Specifications (Orig_N,
R_Type : constant Entity_Id := Etype (Scope_Id);
-- Function result subtype
- procedure Check_Return_Obj_Accessibility (Return_Stmt : Node_Id);
+ procedure Check_Return_Construct_Accessibility (Return_Stmt : Node_Id);
-- Apply legality rule of 6.5 (5.9) to the access discriminants of an
-- aggregate in a return statement.
-- Check that the return_subtype_indication properly matches the result
-- subtype of the function, as required by RM-6.5(5.1/2-5.3/2).
- ------------------------------------
- -- Check_Return_Obj_Accessibility --
- ------------------------------------
+ ------------------------------------------
+ -- Check_Return_Construct_Accessibility --
+ ------------------------------------------
- procedure Check_Return_Obj_Accessibility (Return_Stmt : Node_Id) is
+ procedure Check_Return_Construct_Accessibility (Return_Stmt : Node_Id) is
Assoc : Node_Id;
Agg : Node_Id := Empty;
Discr : Entity_Id;
Expr : Node_Id;
Obj : Node_Id;
Process_Exprs : Boolean := False;
- Return_Obj : Node_Id;
+ Return_Con : Node_Id;
begin
- -- Only perform checks on record types with access discriminants
+ -- Only perform checks on record types with access discriminants and
+ -- non-internally generated functions.
if not Is_Record_Type (R_Type)
or else not Has_Discriminants (R_Type)
+ or else not Comes_From_Source (Return_Stmt)
then
return;
end if;
-- simple return statement the expression is part of the node.
if Nkind (Return_Stmt) = N_Extended_Return_Statement then
- Return_Obj := Last (Return_Object_Declarations (Return_Stmt));
+ -- Obtain the object definition from the expanded extended return
- -- We could be looking at something that's been expanded with
- -- an initialzation procedure which we can safely ignore.
+ Return_Con := First (Return_Object_Declarations (Return_Stmt));
+ while Present (Return_Con) loop
+ -- Inspect the original node to avoid object declarations
+ -- expanded into renamings.
- if Nkind (Return_Obj) /= N_Object_Declaration then
- return;
- end if;
+ if Nkind (Original_Node (Return_Con)) = N_Object_Declaration
+ and then Comes_From_Source (Original_Node (Return_Con))
+ then
+ exit;
+ end if;
+
+ Nlists.Next (Return_Con);
+ end loop;
+
+ pragma Assert (Present (Return_Con));
+
+ -- Could be dealing with a renaming
+
+ Return_Con := Original_Node (Return_Con);
else
- Return_Obj := Return_Stmt;
+ Return_Con := Return_Stmt;
end if;
-- We may need to check an aggregate or a subtype indication
-- depending on how the discriminants were specified and whether
-- we are looking at an extended return statement.
- if Nkind (Return_Obj) = N_Object_Declaration
- and then Nkind (Object_Definition (Return_Obj))
+ if Nkind (Return_Con) = N_Object_Declaration
+ and then Nkind (Object_Definition (Return_Con))
= N_Subtype_Indication
then
- Assoc := First (Constraints
- (Constraint (Object_Definition (Return_Obj))));
+ Assoc := Original_Node
+ (First
+ (Constraints
+ (Constraint (Object_Definition (Return_Con)))));
else
-- Qualified expressions may be nested
- Agg := Original_Node (Expression (Return_Obj));
+ Agg := Original_Node (Expression (Return_Con));
while Nkind (Agg) = N_Qualified_Expression loop
Agg := Original_Node (Expression (Agg));
end loop;
N_Discriminant_Association)
then
Expr := Expression (Assoc);
+ else
+ Expr := Empty;
end if;
-- This anonymous access discriminant has an associated
-- expression which needs checking.
- if Nkind (Expr) = N_Attribute_Reference
+ if Present (Expr)
+ and then Nkind (Expr) = N_Attribute_Reference
and then Attribute_Name (Expr) /= Name_Unrestricted_Access
then
-- Obtain the object to perform static checks on by moving
-- up the prefixes in the expression taking into account
- -- named access types.
+ -- named access types and renamed objects within the
+ -- expression.
- Obj := Prefix (Expr);
- while Nkind_In (Obj, N_Indexed_Component,
- N_Selected_Component)
+ Obj := Original_Node (Prefix (Expr));
loop
- -- When we encounter a named access type then we can
- -- ignore accessibility checks on the dereference.
+ while Nkind_In (Obj, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component)
+ loop
+ -- When we encounter a named access type then we can
+ -- ignore accessibility checks on the dereference.
- if Ekind (Etype (Prefix (Obj)))
- in E_Access_Type ..
- E_Access_Protected_Subprogram_Type
- then
- if Nkind (Obj) = N_Selected_Component then
- Obj := Selector_Name (Obj);
+ if Ekind (Etype (Original_Node (Prefix (Obj))))
+ in E_Access_Type ..
+ E_Access_Protected_Subprogram_Type
+ then
+ if Nkind (Obj) = N_Selected_Component then
+ Obj := Selector_Name (Obj);
+ else
+ Obj := Original_Node (Prefix (Obj));
+ end if;
+ exit;
end if;
- exit;
- end if;
- -- Skip over the explicit dereference
+ Obj := Original_Node (Prefix (Obj));
+ end loop;
- if Nkind (Prefix (Obj)) = N_Explicit_Dereference then
- Obj := Prefix (Prefix (Obj));
+ if Nkind (Obj) = N_Selected_Component then
+ Obj := Selector_Name (Obj);
+ end if;
+
+ -- Check for renamings
- -- Otherwise move up to the next prefix
+ pragma Assert (Is_Entity_Name (Obj));
+ if Present (Renamed_Object (Entity (Obj))) then
+ Obj := Renamed_Object (Entity (Obj));
else
- Obj := Prefix (Obj);
+ exit;
end if;
end loop;
-- Do not check aliased formals or function calls. A
-- run-time check may still be needed ???
- if Is_Entity_Name (Obj)
- and then Comes_From_Source (Obj)
+ if Is_Formal (Entity (Obj))
+ and then Is_Aliased (Entity (Obj))
then
- -- Explicitly aliased formals are allowed
-
- if Is_Formal (Entity (Obj))
- and then Is_Aliased (Entity (Obj))
- then
- null;
+ null;
- elsif Object_Access_Level (Obj) >
- Scope_Depth (Scope (Scope_Id))
- then
- Error_Msg_N
- ("access discriminant in return aggregate would "
- & "be a dangling reference", Obj);
- end if;
+ elsif Object_Access_Level (Obj) >
+ Scope_Depth (Scope (Scope_Id))
+ then
+ Error_Msg_N
+ ("access discriminant in return aggregate would "
+ & "be a dangling reference", Obj);
end if;
end if;
end if;
end if;
end if;
end loop;
- end Check_Return_Obj_Accessibility;
+ end Check_Return_Construct_Accessibility;
-------------------------------------
-- Check_Return_Subtype_Indication --
Resolve (Expr, R_Type);
Check_Limited_Return (N, Expr, R_Type);
- Check_Return_Obj_Accessibility (N);
- 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_05_Restriction
- ("RETURN should be the last statement in function", N);
+ Check_Return_Construct_Accessibility (N);
end if;
-
else
- Check_SPARK_05_Restriction ("extended RETURN is not allowed", N);
Obj_Decl := Last (Return_Object_Declarations (N));
-- Analyze parts specific to extended_return_statement:
Check_References (Stm_Entity);
- Check_Return_Obj_Accessibility (N);
+ Check_Return_Construct_Accessibility (N);
-- Check RM 6.5 (5.9/3)
if Result_Definition (N) /= Error then
if Nkind (Result_Definition (N)) = N_Access_Definition then
- Check_SPARK_05_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_05_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);
Check_Returns (HSS, 'P', Missing_Ret, Id);
end if;
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_05_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_05_Restriction
- ("procedure should not have RETURN", N);
- end if;
- end if;
end Check_Missing_Return;
-----------------------
-- 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 and in
- -- Compile_Only mode to enable the proper back-end type annotations.
+ -- body. These freeze actions are also needed in Compile_Only mode to
+ -- enable the proper back-end type annotations.
-- They are necessary in any case to ensure proper elaboration order
-- in gigi.
and then not Has_Completion (Spec_Id)
and then Serious_Errors_Detected = 0
and then (Expander_Active
- or else ASIS_Mode
or else Operating_Mode = Check_Semantics
or else Is_Ignored_Ghost_Entity (Spec_Id))
then
-- Within an instance, add local renaming declarations so that
-- gdb can retrieve the values of actuals more easily. This is
- -- only relevant if generating code (and indeed we definitely
- -- do not want these definitions -gnatc mode, because that would
- -- confuse ASIS).
+ -- only relevant if generating code.
if Is_Generic_Instance (Spec_Id)
and then Is_Wrapper_Package (Current_Scope)
-- Legacy implementation (relying on front-end inlining)
if not Back_End_Inlining then
- if (Has_Pragma_Inline_Always (Spec_Id)
- and then not Opt.Disable_FE_Inline_Always)
+ if Has_Pragma_Inline_Always (Spec_Id)
or else (Front_End_Inlining
and then not Opt.Disable_FE_Inline)
then
elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then
null;
+ -- SPARK_Mode Off could complete no SPARK_Mode in a generic, either
+ -- as specified in source code, or because SPARK_Mode On is ignored
+ -- in an instance where the context is SPARK_Mode Off/Auto.
+
+ elsif Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = Off
+ and then (Is_Generic_Unit (Spec_Id) or else In_Instance)
+ then
+ null;
+
else
Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
Error_Msg_N ("incorrect application of SPARK_Mode #", N);
if Nkind (Specification (N)) = N_Procedure_Specification
and then Null_Present (Specification (N))
then
- Check_SPARK_05_Restriction ("null procedure is not allowed", N);
-
-- Null procedures are allowed in protected types, following the
-- recent AI12-0147.
-- 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_05_Restriction
- ("user-defined operator is not allowed", N);
- end if;
-
-- Proceed with analysis. Do not emit a cross-reference entry if the
-- specification comes from an expression function, because it may be
-- the completion of a previous declaration. If it is not, the cross-
Inherit_Subprogram_Contract (E, S);
end if;
+ -- When a dispatching operation overrides an inherited
+ -- subprogram, it shall be subtype conformant with the
+ -- inherited subprogram (RM 3.9.2 (10.2)).
+
+ if Comes_From_Source (E)
+ and then Is_Dispatching_Operation (E)
+ and then Find_Dispatching_Type (S)
+ = Find_Dispatching_Type (E)
+ then
+ Check_Subtype_Conformant (E, S);
+ end if;
+
if Comes_From_Source (E) then
Check_Overriding_Indicator (E, S, Is_Primitive => False);
Check_Ghost_Overriding (S, Overridden_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_05_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 Check_Dispatching_Operation is not
Default := Expression (Param_Spec);
if Present (Default) then
- Check_SPARK_05_Restriction
- ("default expression is not allowed", Default);
-
if Out_Present (Param_Spec) then
Error_Msg_N
("default initialization only allowed for IN parameters",
projects / gcc.git / blobdiff