[Ada] Remove special handling for package declaring abstract state

[Arnaud Charlet]

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  <dewar@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.

-------------- next part --------------
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