[Ada] Pragma SPARK_Mode and expression functions
Arnaud Charlet
charlet@adacore.com
Tue Oct 27 11:50:00 GMT 2015
This patch ensures that an internally generated subprogram body that completes
an expression function inherits the SPARK_Mode from the expression function
spec.
------------
-- Source --
------------
-- expr_funcs.ads
package Expr_Funcs with SPARK_Mode is
function F1 return Boolean is (True); -- F1 spec has mode ON
function F2 return Boolean; -- F2 spec has mode ON
function F3 return Boolean; -- F3 spec has mode ON
private
pragma SPARK_Mode (Off);
-- function F1 return Boolean is -- F1 body has mode ON
-- begin
-- return True;
-- end F1;
function F2 return Boolean is (True); -- F2 body has mode OFF
function F3 return Boolean is (True) -- F3 body attempts mdoe ON
with SPARK_Mode; -- Error
end Expr_Funcs;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c expr_funcs.ads
expr_funcs.ads:16:11: cannot change SPARK_Mode from Off to On
expr_funcs.ads:16:11: SPARK_Mode was set to Off at line 7
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
-------------- next part --------------
Index: inline.adb
===================================================================
--- inline.adb (revision 229413)
+++ inline.adb (working copy)
@@ -1357,10 +1357,6 @@
-- 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 --
---------------------------------------------------
@@ -1472,20 +1468,6 @@
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 --
------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 229413)
+++ sem_util.adb (working copy)
@@ -5081,7 +5081,6 @@
(Is_Concurrent_Type (Scope (Discriminal_Link (E)))
or else
Is_Concurrent_Record_Type (Scope (Discriminal_Link (E)))));
-
end Denotes_Discriminant;
-------------------------
@@ -11677,26 +11676,46 @@
----------------------------
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 --
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 229413)
+++ sem_util.ads (working copy)
@@ -1334,10 +1334,13 @@
-- 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
-- a specific tagged type whose related subprogram is subject to pragma
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 229413)
+++ sem_res.adb (working copy)
@@ -5793,10 +5793,11 @@
-- 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);
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 229414)
+++ sem_ch6.adb (working copy)
@@ -3493,15 +3493,40 @@
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);
More information about the Gcc-patches
mailing list