[Ada] Handling of SPARK aspects/pragmas on subprogram body stubs

This patch reimplements the support for SPARK aspects/pragmas that apply to a
subprogram body stub and implements a missing rule which forbids the placement
of refinement annotations in subunits.

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

--  error.ads

package Error
  with SPARK_Mode     => On,
       Abstract_State => State
is
   procedure Spec_Stub_Body_1
     with Global => (In_Out => State);

   procedure Spec_Stub_Body_2
     with Global  => (In_Out => State),
          Depends => (State  => State);

   procedure Spec_Stub_Body_3
     with Global  => (In_Out => State),
          Depends => (State  => State);

   procedure Spec_Stub_Body_4
     with Global  => (In_Out => State),
          Depends => (State  => State);

   procedure Spec_Stub_Body_5
     with Global  => (In_Out => State),
          Depends => (State  => State);
end Error;

--  error.adb

package body Error
  with SPARK_Mode    => On,
       Refined_State => (State => (A, B))
is
   A : Integer := 1;
   B : Integer := 2;

   procedure Spec_Stub_Body_1 is separate
     with Depends => (A => B);  --  error
   --  Depends must appear on the spec (first declaration)

   procedure Spec_Stub_Body_2 is separate
     with Refined_Global => (In_Out => (A, B));
   --  Refined_Depends must appear on the stub (second declaration)

   procedure Spec_Stub_Body_3 is separate;
   --  Refined_Global and Refined_Depends must appear on the stub (second
   --  declaration).

   procedure Spec_Stub_Body_4 is separate
     with Refined_Global  => (In_Out  => (A, "error")),
          Refined_Depends => ("error" => B);
   --  Refined_Global and Refined_Depends are placed properly, but malformed

   procedure Spec_Stub_Body_5 is separate
     with Refined_Global  => (In_Out  => (A, "error")),
          Refined_Depends => ("error" => B);
   --  Refined_Global and Refined_Depends are placed properly, but malformed. A
   --  proper body is also missing.

   procedure Stub_Body is separate
     with Global  => (In_Out => (A, B)),
          Depends => (A => B);
   --  Refined_Global and Refined_Depends apply to a body whose spec (the
   --  stub) is not visible.
end Error;

--  error-spec_stub_body_1.adb

separate (Error)

procedure Spec_Stub_Body_1 is begin null; end Spec_Stub_Body_1;

--  error-spec_stub_body_2.adb

separate (Error)

procedure Spec_Stub_Body_2
  with Refined_Depends => (A => B)  --  error
is begin null; end Spec_Stub_Body_2;

--  error-spec_stub_body_3.adb

separate (Error)

procedure Spec_Stub_Body_3
  with Refined_Global  => (In_Out => (A, B)),  --  error
       Refined_Depends => (A => B)             --  error
is begin null; end Spec_Stub_Body_3;

--  error-spec_stub_body_4.adb

separate (Error)

procedure Spec_Stub_Body_4 is begin null; end Spec_Stub_Body_4;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c error.adb
error.adb:9:11: aspect specification must appear in subprogram declaration
error.adb:25:04: warning: subunit "Error.Spec_Stub_Body_5" in file
  "error-spec_stub_body_5.adb" not found
error-spec_stub_body_2.adb:4:08: aspect "Refined_Depends" cannot apply to a
  subunit
error-spec_stub_body_3.adb:4:08: aspect "Refined_Global" cannot apply to a
  subunit
error-spec_stub_body_3.adb:5:08: aspect "Refined_Depends" cannot apply to a
  subunit
error-stub_body.adb:4:08: aspect "Refined_Global" cannot apply to a subunit
error-stub_body.adb:5:08: aspect "Refined_Depends" cannot apply to a subunit

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

2014-02-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb (Add_Or_Save_Precondition): New routine.
	(Collect_Body_Postconditions_In_Decls): New routine.
	(Collect_Body_Postconditions_Of_Kind): Factor out code. Handle
	postcondition aspects or pragmas that appear on a subprogram
	body stub.
	(Collect_Spec_Preconditions): Factor out code. Handle
	precondition aspects or pragmas that appear on a subprogram
	body stub.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): The analysis of
	aspects that apply to a subprogram body stub is no longer delayed,
	the aspects are analyzed on the spot.
	(SPARK_Aspect_Error):
	Aspects that apply to a subprogram declaration cannot appear in
	a subunit.
	* sem_ch10.adb Remove with and use clause for Sem_Ch13.
	(Analyze_Proper_Body): Add local variable Comp_Unit. Unum
	is now a local variable. Code cleanup. Analysis related to
	the aspects of a subprogram body stub is now carried out by
	Analyze_Subprogram_Body_Helper. Do not propagate the aspects
	and/or pragmas of a subprogram body stub to the proper body
	as this is no longer needed. Do not analyze the aspects of a
	subprogram stub when the corresponding source unit is missing.
	(Analyze_Protected_Body_Stub): Flag the illegal use of aspects
	on a stub.
	(Analyze_Task_Body_Stub): Flag the illegal use of
	aspects on a stub.
	(Optional_Subunit): Add local variable Unum.
	* sem_ch13.adb (Insert_Delayed_Pragma): Do not analyze a generated
	pragma when it applies to a subprogram body stub.
	* sem_prag.adb (Analyze_Pragma): Pragmas Contract_Cases,
	Depends and Global can now apply to a subprogram body stub as
	long as it acts as its own spec.
	(Analyze_Refined_Pragma):
	Code reformatting. Refinement pragmas cannot apply to a subunit.

[Ada] Handling of SPARK aspects/pragmas on subprogram body stubs

Commit Message

Patch