The rules for pragma SPARK_Mode have changed. In particular, the mode
is not inherited anymore from a the spec to the body, and the body
should not have a mode if the spec did not have one. These new rules
are checked now. A minor change is that SPARK_Mode is set even on
subprograms for which Comes_From_Source returns False (including
internal subprograms), as we need this information on subprograms
from instances of generics.
The following test now generates an error:
1. package SPARKcode is
2. pragma SPARK_Mode (On);
3. procedure P1;
4. procedure P2 with SPARK_Mode => On;
5. procedure P3 with SPARK_Mode => Off;
6. end SPARKcode;
1. package body SPARKcode is
2. pragma SPARK_Mode (On);
3. procedure P1 is begin null; end;
4. procedure P2 is begin null; end;
5. procedure P3 is begin null; end;
|
>>> incorrect application of SPARK_Mode at line 2
>>> value Off was set for SPARK_Mode on "P3" at sparkcode.ads:5
6. end SPARKcode;
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-29 Yannick Moy <m...@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode
not inherited from spec anymore. Check consistency
rules after processing of declarations.
* sem_ch7.adb (Analyze_Package_Body_Helper): SPARK_Mode not inherited
from spec anymore. Check consistency rules after processing of
declarations.
(Analyze_Package_Declaration): Set SPARK_Mode only for non-generic
packages.
* sem_prag.adb (Analyze_Pragma/Pragma_SPARK_Mode): Implement new
consistency rules.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 207241)
+++ sem_ch7.adb (working copy)
@@ -346,29 +346,20 @@
Push_Scope (Spec_Id);
- -- Set SPARK_Mode from private part of spec if it has a SPARK pragma.
- -- Note that in the default case, SPARK_Aux_Pragma will be a copy of
- -- SPARK_Pragma in the spec, so this properly handles the case where
- -- there is no explicit SPARK_Pragma mode in the private part.
+ -- Set SPARK_Mode only for non-generic package
- if Present (SPARK_Pragma (Spec_Id)) then
- SPARK_Mode_Pragma := SPARK_Aux_Pragma (Spec_Id);
- SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
+ if Ekind (Spec_Id) = E_Package then
+ -- Set SPARK_Mode from context
+
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
- -- Otherwise set from context
+ -- Set elaboration code SPARK mode the same for now
- else
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id, True);
+ Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
end if;
- -- Set elaboration code SPARK mode the same for now
-
- Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
- Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
-
Set_Categorization_From_Pragmas (N);
Install_Visible_Declarations (Spec_Id);
@@ -400,6 +391,32 @@
Inspect_Deferred_Constant_Completion (Declarations (N));
end if;
+ -- After declarations have been analyzed, the body has been set
+ -- its final value of SPARK_Mode. Check that SPARK_Mode for body
+ -- is consistent with SPARK_Mode for spec.
+
+ if Present (SPARK_Pragma (Body_Id)) then
+ if Present (SPARK_Aux_Pragma (Spec_Id)) then
+ if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
+ and then
+ Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+ then
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (SPARK_Aux_Pragma (Spec_Id));
+ Error_Msg_NE ("\value Off was set for SPARK_Mode on & #",
+ N, Spec_Id);
+ end if;
+
+ else
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (Spec_Id);
+ Error_Msg_NE ("\no value was set for SPARK_Mode on & #",
+ N, Spec_Id);
+ end if;
+ end if;
+
-- Analyze_Declarations has caused freezing of all types. Now generate
-- bodies for RACW primitives and stream attributes, if any.
@@ -814,12 +831,14 @@
Set_Etype (Id, Standard_Void_Type);
Set_Contract (Id, Make_Contract (Sloc (Id)));
- -- Inherit spark mode from context for now
+ -- Set SPARK_Mode from context only for non-generic package
- Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
- Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Id, True);
- Set_SPARK_Aux_Pragma_Inherited (Id, True);
+ if Ekind (Id) = E_Package then
+ Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Id, True);
+ Set_SPARK_Aux_Pragma_Inherited (Id, True);
+ end if;
-- Analyze aspect specifications immediately, since we need to recognize
-- things like Pure early enough to diagnose violations during analysis.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 207241)
+++ sem_prag.adb (working copy)
@@ -18597,14 +18597,26 @@
Spec_Id : Entity_Id;
Stmt : Node_Id;
- procedure Check_Pragma_Conformance (Old_Pragma : Node_Id);
- -- Verify the monotonicity of SPARK modes between the new pragma
- -- N, and the old pragma, Old_Pragma, that was inherited. If
- -- Old_Pragma is Empty, the call has no effect, otherwise we
- -- verify that the new mode is less restrictive than the old mode.
- -- For example, if the old mode is ON, then the new mode can be
- -- anything. But if the old mode is OFF, then the only allowed
- -- new mode is also OFF.
+ procedure Check_Pragma_Conformance
+ (Context_Pragma : Node_Id;
+ Entity_Pragma : Node_Id;
+ Entity : Entity_Id);
+ -- If Context_Pragma is not Empty, verify that the new pragma N
+ -- is compatible with the pragma Context_Pragma that was inherited
+ -- from the context:
+ -- . if Context_Pragma is ON, then the new mode can be anything
+ -- . if Context_Pragma is OFF, then the only allowed new mode is
+ -- also OFF.
+ --
+ -- If Entity is not Empty, verify that the new pragma N is
+ -- compatible with Entity_Pragma, the SPARK_Mode previously set
+ -- for Entity (which may be Empty):
+ -- . if Entity_Pragma is ON, then the new mode can be anything
+ -- . if Entity_Pragma is OFF, then the only allowed new mode is
+ -- also OFF.
+ -- . if Entity_Pragma is Empty, we always issue an error, as this
+ -- corresponds to a case where a previous section of Entity
+ -- had no SPARK_Mode set.
procedure Check_Library_Level_Entity (E : Entity_Id);
-- Verify that pragma is applied to library-level entity E
@@ -18613,23 +18625,47 @@
-- Check_Pragma_Conformance --
------------------------------
- procedure Check_Pragma_Conformance (Old_Pragma : Node_Id) is
+ procedure Check_Pragma_Conformance
+ (Context_Pragma : Node_Id;
+ Entity_Pragma : Node_Id;
+ Entity : Entity_Id) is
begin
- if Present (Old_Pragma) then
- pragma Assert (Nkind (Old_Pragma) = N_Pragma);
+ if Present (Context_Pragma) then
+ pragma Assert (Nkind (Context_Pragma) = N_Pragma);
-- New mode less restrictive than the established mode
- if Get_SPARK_Mode_From_Pragma (Old_Pragma) = Off
+ if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
and then Mode_Id = On
then
Error_Msg_N
- ("cannot change 'S'P'A'R'K_Mode from Off to On", Arg1);
+ ("cannot change SPARK_Mode from Off to On", Arg1);
Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
- Error_Msg_N ("\'S'P'A'R'K_Mode was set to Off#", Arg1);
+ Error_Msg_N ("\SPARK_Mode was set to Off#", Arg1);
raise Pragma_Exit;
end if;
end if;
+
+ if Present (Entity) then
+ if Present (Entity_Pragma) then
+ if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
+ and then Mode_Id = On
+ then
+ Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
+ Error_Msg_Sloc := Sloc (Entity_Pragma);
+ Error_Msg_NE
+ ("\value Off was set for SPARK_Mode on & #",
+ Arg1, Entity);
+ raise Pragma_Exit;
+ end if;
+ else
+ Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
+ Error_Msg_Sloc := Sloc (Entity);
+ Error_Msg_NE ("\no value was set for SPARK_Mode on & #",
+ Arg1, Entity);
+ raise Pragma_Exit;
+ end if;
+ end if;
end Check_Pragma_Conformance;
--------------------------------
@@ -18733,7 +18769,10 @@
then
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
Set_SPARK_Pragma (Spec_Id, N);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
@@ -18748,7 +18787,10 @@
then
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
Set_SPARK_Pragma (Spec_Id, N);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
@@ -18804,7 +18846,10 @@
if List_Containing (N) = Private_Declarations (Context) then
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity_Pragma => SPARK_Pragma (Spec_Id),
+ Entity => Spec_Id);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@@ -18815,7 +18860,10 @@
else
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@@ -18834,8 +18882,10 @@
then
Spec_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
-
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
Set_SPARK_Pragma (Spec_Id, N);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
@@ -18848,7 +18898,10 @@
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity_Pragma => SPARK_Aux_Pragma (Spec_Id),
+ Entity => Spec_Id);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@@ -18867,7 +18920,19 @@
Context := Specification (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
+
+ if Present (Spec_Id) then
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity_Pragma => SPARK_Pragma (Spec_Id),
+ Entity => Spec_Id);
+ else
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
+ end if;
+
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@@ -18887,7 +18952,10 @@
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity_Pragma => SPARK_Pragma (Body_Id),
+ Entity => Body_Id);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 207241)
+++ sem_ch6.adb (working copy)
@@ -2999,35 +2999,11 @@
Push_Scope (Spec_Id);
- -- Set SPARK_Mode
+ -- Set SPARK_Mode from context
- -- For internally generated subprogram, always off. But generic
- -- instances are not generated implicitly, so are never considered
- -- as internal, even though Comes_From_Source is false.
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
- if not Comes_From_Source (Spec_Id)
- and then not Is_Generic_Instance (Spec_Id)
- then
- SPARK_Mode := Off;
- SPARK_Mode_Pragma := Empty;
-
- -- Inherited from spec
-
- elsif Present (SPARK_Pragma (Spec_Id))
- and then not SPARK_Pragma_Inherited (Spec_Id)
- then
- SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
- SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
- Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
- Set_SPARK_Pragma_Inherited (Body_Id, True);
-
- -- Otherwise set from context
-
- else
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id, True);
- end if;
-
-- Make sure that the subprogram is immediately visible. For
-- child units that have no separate spec this is indispensable.
-- Otherwise it is safe albeit redundant.
@@ -3076,17 +3052,10 @@
Push_Scope (Body_Id);
- -- Set SPARK_Mode from context or OFF for internal routine
+ -- Set SPARK_Mode from context
- if Comes_From_Source (Body_Id) then
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id, True);
- else
- Set_SPARK_Pragma (Body_Id, Empty);
- Set_SPARK_Pragma_Inherited (Body_Id, False);
- SPARK_Mode := Off;
- SPARK_Mode_Pragma := Empty;
- end if;
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
end if;
-- For stubs and bodies with no previous spec, generate references to
@@ -3277,6 +3246,35 @@
Analyze_Declarations (Declarations (N));
+ -- After declarations have been analyzed, the body has been set
+ -- its final value of SPARK_Mode. Check that SPARK_Mode for body
+ -- is consistent with SPARK_Mode for spec.
+
+ if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
+ if Present (SPARK_Pragma (Spec_Id)) then
+ if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
+ and then
+ Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+ then
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id));
+ Error_Msg_NE
+ ("\value Off was set for SPARK_Mode on & #", N, Spec_Id);
+ end if;
+
+ elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then
+ null;
+
+ else
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (Spec_Id);
+ Error_Msg_NE
+ ("\no value was set for SPARK_Mode on & #", N, Spec_Id);
+ end if;
+ end if;
+
-- Check completion, and analyze the statements
Check_Completion;
@@ -3632,16 +3630,11 @@
Generate_Definition (Designator);
- -- Set SPARK mode, always off for internal routines, otherwise set
- -- from current context (may be overwritten later with explicit pragma)
+ -- Set SPARK mode from current context (may be overwritten later with
+ -- explicit pragma).
- if Comes_From_Source (Designator) then
- Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Designator, True);
- else
- Set_SPARK_Pragma (Designator, Empty);
- Set_SPARK_Pragma_Inherited (Designator, False);
- end if;
+ Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Designator, True);
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
