[Ada] Non-SPARK package bodies and state refinement

[Arnaud Charlet <charlet at adacore dot com>]

This patch modifies the analysis of package bodies to suppress an error message
prompting for state refinement when the body's SPARK mode is Off.

------------
-- Source --
------------

--  pack.ads

package Pack
   with Abstract_State => State,
        Initializes    => State
is
   procedure Proc
      with Global  => (In_Out => State),
           Depends => (State  => State);
end Pack;

--  pack.adb

package body Pack is
   pragma SPARK_Mode (Off);

   X : Integer := 0;

   procedure Proc is
   begin
      X := X + 1;
   end Proc;
end Pack;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnatd.V pack.adb

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch3.adb (Analyze_Declarations): Emit an
	error message concerning state refinement when the spec defines at
	least one non-null abstract state and the body's SPARK mode is On.
	(Requires_State_Refinement): New routine.

Attachment: difs
Description: Text document