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 <[email protected]>
* sem_prag.adb (Analyze_Pragma): Add processing
for aspect/pragma SPARK_Mode when it applies to a [library-level]
subprogram or package [body].
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
