If a library level package declaration or generic package declaration
contains a non-null abstract state, and does not otherwise require a
body, then in accorance with SPARK (LRM 7.1.5(4)), the package must
contain a pragma Elaborate_Body. This implements this requirement,
as shown in the following compiled with -gnatj60 -gnatd.V.
1. package Needs_Pragma_Elaborate_Body
2. with Abstract_State => State
|
>>> package "Needs_Pragma_Elaborate_Body" specifies
a non-null abstract state, but package does not
otherwise require a body, pragma Elaborate_Body
is required in this case
3. is
4. -- package declarations with non-null
5. -- Abstract State shall have bodies.
6.
7. -- There should be a pragma Elaborate_Body
8. end Needs_Pragma_Elaborate_Body;
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-15 Robert Dewar <de...@adacore.com>
* sem_ch7.adb (Unit_Requires_Body): Add flag
Ignore_Abstract_State (Analyze_Package_Specification): Enforce
rule requiring Elaborate_Body if a non-null abstract state is
specified for a library-level package.
* sem_ch7.ads (Unit_Requires_Body): Add flag Ignore_Abstract_State.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 203568)
+++ sem_ch7.adb (working copy)
@@ -1483,7 +1483,38 @@
Clear_Constants (Id, First_Private_Entity (Id));
end if;
+ -- Issue an error in SPARK mode if a package specification contains
+ -- more than one tagged type or type extension.
+
Check_One_Tagged_Type_Or_Extension_At_Most;
+
+ -- Issue an error if a package that is a library unit does not require a
+ -- body, and we have a non-null abstract state (SPARK LRM 7.1.5(4)).
+
+ if not Unit_Requires_Body (Id, Ignore_Abstract_State => True)
+ and then Present (Abstract_States (Id))
+
+ -- We use Scope_Depth of 1 to identify library units, which seems a
+ -- bit ugly, but there doesn't seem to be an easier way.
+
+ and then Scope_Depth (Id) = 1
+
+ -- A null abstract state always appears as the sole element of the
+ -- state list.
+
+ and then not Is_Null_State (Node (First_Elmt (Abstract_States (Id))))
+ then
+ declare
+ P : constant Node_Id := Get_Pragma (Id, Pragma_Abstract_State);
+ begin
+ Error_Msg_NE
+ ("package & specifies a non-null abstract state", P, Id);
+ Error_Msg_N
+ ("\but package does not otherwise require a body", P);
+ Error_Msg_N
+ ("\pragma Elaborate_Body is required in this case", P);
+ end;
+ end if;
end Analyze_Package_Specification;
--------------------------------------
@@ -2588,7 +2619,10 @@
-- Unit_Requires_Body --
------------------------
- function Unit_Requires_Body (P : Entity_Id) return Boolean is
+ function Unit_Requires_Body
+ (P : Entity_Id;
+ Ignore_Abstract_State : Boolean := False) return Boolean
+ is
E : Entity_Id;
begin
@@ -2627,12 +2661,17 @@
end;
-- A [generic] package that introduces at least one non-null abstract
- -- state requires completion. A null abstract state always appears as
- -- the sole element of the state list.
+ -- state requires completion. However, there is a separate rule that
+ -- requires that such a package have a reason other than this for a
+ -- body being required (if necessary a pragma Elaborate_Body must be
+ -- provided). If Ignore_Abstract_State is True, we don't do this check
+ -- (so we can use Unit_Requires_Body to check for some other reason).
elsif Ekind_In (P, E_Generic_Package, E_Package)
+ and then not Ignore_Abstract_State
and then Present (Abstract_States (P))
- and then not Is_Null_State (Node (First_Elmt (Abstract_States (P))))
+ and then
+ not Is_Null_State (Node (First_Elmt (Abstract_States (P))))
then
return True;
end if;
Index: sem_ch7.ads
===================================================================
--- sem_ch7.ads (revision 203568)
+++ sem_ch7.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2008, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2013, 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- --
@@ -52,9 +52,15 @@
-- but is deferred until the compilation of the private part of the
-- child for public child packages.
- function Unit_Requires_Body (P : Entity_Id) return Boolean;
- -- Check if a unit requires a body. A specification requires a body
- -- if it contains declarations that require completion in a body.
+ function Unit_Requires_Body
+ (P : Entity_Id;
+ Ignore_Abstract_State : Boolean := False) return Boolean;
+ -- Check if a unit requires a body. A specification requires a body if it
+ -- contains declarations that require completion in a body. If the flag
+ -- Ignore_Abstract_State is set True, then the test for a non-null abstract
+ -- state (which normally requires a body) is not carried out. This allows
+ -- the use of this routine to tell if there is some other reason that a
+ -- body is required (as is required for analyzing Abstract_State).
procedure May_Need_Implicit_Body (E : Entity_Id);
-- If a package declaration contains tasks or RACWs and does not require
