[Ada] Placement of aspect/pragma SPARK_Mode

[Arnaud Charlet <charlet at adacore dot com>]

This patch modifies the processing of aspect/pragma SPARK_Mode to properly
handle the cases where the aspect/pragma apply to a [library-level] package or
subprogram [body].

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

--  func.ads

function Func return Integer with SPARK_Mode => On;

--  pack.adb

package body Pack with SPARK_Mode => Off is
   procedure Dummy is begin null; end Dummy;
end Pack;

--  pack.ads

package Pack is
   procedure Dummy;
end Pack;

--  proc.ads

procedure Proc with SPARK_Mode => On;

--  spec.ads

package Spec with SPARK_Mode => On is
end Spec;

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

$ gcc -c -gnatc -gnat12 -gnatd.V func.ads
$ gcc -c -gnat12 -gnatd.V pack.adb
$ gcc -c -gnatc -gnat12 -gnatd.V proc.ads
$ gcc -c -gnatc -gnat12 -gnatd.V spec.ads

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

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

	* sem_prag.adb (Analyze_Pragma): Add processing
	for aspect/pragma SPARK_Mode when it applies to a [library-level]
	subprogram or package [body].

Attachment: difs
Description: Text document