+2015-10-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * inline.adb (Is_Expression_Function): Removed.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): An internally
+ generated subprogram body that completes an expression function
+ inherits the SPARK_Mode from the spec.
+ * sem_res.adb (Resolve_Call): Update all calls to
+ Is_Expression_Function.
+ * sem_util.ads, sem_util.adb (Is_Expression_Function): Reimplemented.
+ (Is_Expression_Function_Or_Completion): New routine.
+
2015-10-27 Hristian Kirtchev <kirtchev@adacore.com>
* lib-xref-spark_specific.adb, a-dirval-mingw.adb, exp_ch6.adb,
-- Returns True if subprogram Id is defined in the visible part of a
-- package specification.
- function Is_Expression_Function (Id : Entity_Id) return Boolean;
- -- Returns True if subprogram Id was defined originally as an expression
- -- function.
-
---------------------------------------------------
-- Has_Formal_With_Discriminant_Dependent_Fields --
---------------------------------------------------
and then List_Containing (Decl) = Visible_Declarations (P);
end In_Package_Visible_Spec;
- ----------------------------
- -- Is_Expression_Function --
- ----------------------------
-
- function Is_Expression_Function (Id : Entity_Id) return Boolean is
- Decl : Node_Id := Parent (Parent (Id));
- begin
- if Nkind (Parent (Id)) = N_Defining_Program_Unit_Name then
- Decl := Parent (Decl);
- end if;
-
- return Nkind (Original_Node (Decl)) = N_Expression_Function;
- end Is_Expression_Function;
-
------------------------
-- Is_Unit_Subprogram --
------------------------
Generate_Reference_To_Formals (Body_Id);
end if;
- -- Set the SPARK_Mode from the current context (may be overwritten later
- -- with explicit pragma). This is not done for entry barrier functions
- -- because they are generated outside the protected type and should not
- -- carry the mode of the enclosing context.
+ -- Entry barrier functions are generated outside the protected type and
+ -- should not carry the SPARK_Mode of the enclosing context.
if Nkind (N) = N_Subprogram_Body
and then Is_Entry_Barrier_Function (N)
then
null;
+
+ -- The body is generated as part of expression function expansion. When
+ -- the expression function appears in the visible declarations of a
+ -- package, the body is added to the private declarations. Since both
+ -- declarative lists may be subject to a different SPARK_Mode, inherit
+ -- the mode of the spec.
+
+ -- package P with SPARK_Mode is
+ -- function Expr_Func ... is (...); -- original
+ -- [function Expr_Func ...;] -- generated spec
+ -- -- mode is ON
+ -- private
+ -- pragma SPARK_Mode (Off);
+ -- [function Expr_Func ... is return ...;] -- generated body
+ -- end P; -- mode is ON
+
+ elsif not Comes_From_Source (N)
+ and then Present (Prev_Id)
+ and then Is_Expression_Function (Prev_Id)
+ then
+ Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Prev_Id));
+ Set_SPARK_Pragma_Inherited
+ (Body_Id, SPARK_Pragma_Inherited (Prev_Id));
+
+ -- Set the SPARK_Mode from the current context (may be overwritten later
+ -- with explicit pragma).
+
else
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id);
-- is frozen in the usual fashion, by the appearance of a real body,
-- or at the end of a declarative part.
- if Is_Entity_Name (Subp) and then not In_Spec_Expression
- and then not Is_Expression_Function (Current_Scope)
+ if Is_Entity_Name (Subp)
+ and then not In_Spec_Expression
+ and then not Is_Expression_Function_Or_Completion (Current_Scope)
and then
- (not Is_Expression_Function (Entity (Subp))
+ (not Is_Expression_Function_Or_Completion (Entity (Subp))
or else Scope (Entity (Subp)) = Current_Scope)
then
Freeze_Expression (Subp);
(Is_Concurrent_Type (Scope (Discriminal_Link (E)))
or else
Is_Concurrent_Record_Type (Scope (Discriminal_Link (E)))));
-
end Denotes_Discriminant;
-------------------------
----------------------------
function Is_Expression_Function (Subp : Entity_Id) return Boolean is
- Decl : Node_Id;
-
begin
- if Ekind (Subp) /= E_Function then
+ if Ekind_In (Subp, E_Function, E_Subprogram_Body) then
+ return
+ Nkind (Original_Node (Unit_Declaration_Node (Subp))) =
+ N_Expression_Function;
+ else
return False;
+ end if;
+ end Is_Expression_Function;
+
+ ------------------------------------------
+ -- Is_Expression_Function_Or_Completion --
+ ------------------------------------------
+
+ function Is_Expression_Function_Or_Completion
+ (Subp : Entity_Id) return Boolean
+ is
+ Subp_Decl : Node_Id;
+
+ begin
+ if Ekind (Subp) = E_Function then
+ Subp_Decl := Unit_Declaration_Node (Subp);
+
+ -- The function declaration is either an expression function or is
+ -- completed by an expression function body.
+
+ return
+ Is_Expression_Function (Subp)
+ or else (Nkind (Subp_Decl) = N_Subprogram_Declaration
+ and then Present (Corresponding_Body (Subp_Decl))
+ and then Is_Expression_Function
+ (Corresponding_Body (Subp_Decl)));
+
+ elsif Ekind (Subp) = E_Subprogram_Body then
+ return Is_Expression_Function (Subp);
else
- Decl := Unit_Declaration_Node (Subp);
- return Nkind (Decl) = N_Subprogram_Declaration
- and then
- (Nkind (Original_Node (Decl)) = N_Expression_Function
- or else
- (Present (Corresponding_Body (Decl))
- and then
- Nkind (Original_Node
- (Unit_Declaration_Node
- (Corresponding_Body (Decl)))) =
- N_Expression_Function));
+ return False;
end if;
- end Is_Expression_Function;
+ end Is_Expression_Function_Or_Completion;
-----------------------
-- Is_EVF_Expression --
-- Determine whether entity Id is the spec entity of an entry [family]
function Is_Expression_Function (Subp : Entity_Id) return Boolean;
- -- Predicate to determine whether a scope entity comes from a rewritten
- -- expression function call, and should be inlined unconditionally. Also
- -- used to determine that such a call does not constitute a freeze point.
+ -- Determine whether subprogram [body] Subp denotes an expression function
+
+ function Is_Expression_Function_Or_Completion
+ (Subp : Entity_Id) return Boolean;
+ -- Determine whether subprogram [body] Subp denotes an expression function
+ -- or is completed by an expression function body.
function Is_EVF_Expression (N : Node_Id) return Boolean;
-- Determine whether node N denotes a reference to a formal parameter of
projects / gcc.git / commitdiff