diff mbox

[Ada] Placement of aspect/pragma SPARK_Mode

Message ID 20130910150554.GA22207@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Sept. 10, 2013, 3:05 p.m. UTC 
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].
diff mbox

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 202457)
+++ sem_prag.adb	(working copy)
@@ -16633,12 +16633,53 @@ 
                   Stmt := Prev (Stmt);
                end loop;
 
-               --  If we get here, then we ran out of preceding statements. The
-               --  pragma is immediately within a body.
+               --  Handle all cases where the pragma is actually an aspect and
+               --  applies to a library-level package spec, body or subprogram.
 
-               if Nkind_In (Context, N_Package_Body,
-                                     N_Subprogram_Body)
+               --    function F ... with SPARK_Mode => ...;
+               --    package P with SPARK_Mode => ...;
+               --    package body P with SPARK_Mode => ... is
+
+               --  The following circuitry simply prepares the proper context
+               --  for the general pragma processing mechanism below.
+
+               if Nkind (Context) = N_Compilation_Unit_Aux then
+                  Context := Unit (Parent (Context));
+
+                  if Nkind_In (Context, N_Package_Declaration,
+                                        N_Subprogram_Declaration)
+                  then
+                     Context := Specification (Context);
+                  end if;
+               end if;
+
+               --  The pragma is at the top level of a package spec or appears
+               --  as an aspect on a subprogram.
+
+               --    function F ... with SPARK_Mode => ...;
+
+               --    package P is
+               --       pragma SPARK_Mode;
+
+               if Nkind_In (Context, N_Function_Specification,
+                                     N_Package_Specification,
+                                     N_Procedure_Specification)
                then
+                  Spec_Id := Defining_Unit_Name (Context);
+                  Chain_Pragma (Spec_Id, N);
+
+               --  The pragma is immediately within a package or subprogram
+               --  body.
+
+               --    function F ... is
+               --       pragma SPARK_Mode;
+
+               --    package body P is
+               --       pragma SPARK_Mode;
+
+               elsif Nkind_In (Context, N_Package_Body,
+                                        N_Subprogram_Body)
+               then
                   Spec_Id := Corresponding_Spec (Context);
 
                   if Nkind (Context) = N_Subprogram_Body then
@@ -16650,14 +16691,12 @@ 
                   Chain_Pragma (Body_Id, N);
                   Check_Conformance (Spec_Id, Body_Id);
 
-               --  The pragma is at the top level of a package spec
+               --  The pragma applies to the statements of a package body
 
-               elsif Nkind (Context) = N_Package_Specification then
-                  Spec_Id := Defining_Unit_Name (Context);
-                  Chain_Pragma (Spec_Id, N);
+               --    package body P is
+               --    begin
+               --       pragma SPARK_Mode;
 
-               --  The pragma applies to the statements of a package body
-
                elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
                  and then Nkind (Parent (Context)) = N_Package_Body
                then