On the basis of further discussion, we decided not to implement the
rule saying that a package body must be required for some other
reason if an abstract state is declared. Now we just say a package
body is required if a non-null abstract state and that's it! This
change undoes the error message. So if we compile the following
with -gnatd.V -gnatld7 (but without -gnatc), we get
cannot generate code for file nnas.ads (package spec)
Compiling: nnas.ads
1. package NNAS
2. with Abstract_State => State
3. is
4. -- package declarations with non-null
5. -- Abstract State shall have bodies.
6. end NNAS;
6 lines: No errors
The "cannot generate" line reflects the fact that this package
spec requires a body, so the spec cannot be compiled alone.
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-17 Robert Dewar <de...@adacore.com>
* sem_ch7.adb (Analyze_Package_Specification): Remove circuit
for ensuring that a package spec requires a body for some other
reason than that it contains the declaration of an abstract state.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 203755)
+++ sem_ch7.adb (working copy)
@@ -1493,34 +1493,6 @@
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;
-
-- If switch set, output information on why body required
if List_Body_Required_Info
