This changes the handling of cases in which warnings are normally given
for constructs that are bound to raise run time exceptions if executed.
Previously we converted these to errors unconditionally in GNATProve
mode, but that caused trouble with non-SPARK code, notably s-scaval
from the run-time library.
With this patch, we now properly handle the setting of SPARK_Mode in
the front end, and these warnings are converted to errors only if we
have SPARK_Mode (On), as shown by the following test program:
1. package SPMode is
2. pragma SPARK_Mode (ON);
3. X : Positive := 0; -- ERROR
|
>>> value not in range of type "Standard.Positive"
>>> "Constraint_Error" would have been raised at run time
4. procedure P1;
5. pragma SPARK_Mode (ON);
6. procedure P2;
7. procedure P3;
8. private
9. pragma SPARK_Mode (OFF);
10. X1 : Positive := 0; -- WARNING
|
>>> warning: value not in range of type "Standard.Positive"
>>> warning: "Constraint_Error" will be raised at run time
11. end;
1. package body SPMode is
2. pragma SPARK_Mode (off);
3. Y : Positive := 0; -- WARNING
|
>>> warning: value not in range of type "Standard.Positive"
>>> warning: "Constraint_Error" will be raised at run time
4. procedure P1 is
5. P1P : Positive := 0; -- ERROR
|
>>> value not in range of type "Standard.Positive"
>>> "Constraint_Error" would have been raised at run time
6. begin
7. null;
8. end;
9. procedure P2 is
10. pragma SPARK_Mode (ON);
11. P2P : Positive := 0; -- ERROR
|
>>> value not in range of type "Standard.Positive"
>>> "Constraint_Error" would have been raised at run time
12. begin
13. null;
14. end;
15. procedure P3 is
16. P3P : Positive := 0; -- WARNING
|
>>> warning: value not in range of type "Standard.Positive"
>>> warning: "Constraint_Error" will be raised at run time
17. begin
18. null;
19. end;
20. end;
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-20 Robert Dewar <de...@adacore.com>
* checks.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* exp_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* opt.adb (SPARK_Mode_Config): Handled like other config flags
* opt.ads (SPARK_Mode_Type): Moved here from types (renamed from
SPARK_Mode_Id) (SPARK_Mode_Type): Add pragma Ordered, remove
SPARK_ from names (SPARK_Mode): New flag (SPARK_Mode_Config):
New flag (Config_Switches_Type): Add SPARK_Mode field
* sem.adb: Minor code reorganization (remove unnecessary with)
* sem.ads (Scope_Stack_Entry): Add Save_SPARK_Mode field
* sem_aggr.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* sem_attr.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* sem_ch3.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* sem_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Reset SPARK_Mode
from spec if needed
* sem_ch7.adb (Analyze_Package_Body_Helper): Reset SPARK_Mode
from spec if needed
* sem_ch8.adb (Push_Scope): Save SPARK_Mode (Pop_Scope):
Restore SPARK_Mode
* sem_elab.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* sem_prag.adb (Get_SPARK_Mode_From_Pragma): New function
(Get_SPARK_Mode_Id): Removed (Get_SPARK_Mode_Type): New name
of Get_SPARK_Mode_Id
* sem_prag.ads (Get_SPARK_Mode_From_Pragma): New function
* sem_res.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* sem_util.adb: Check SPARK_Mode instead of GNATProve_Mode for
converting warnings on inevitable exceptions to errors.
* types.ads (SPARK_Mode_Id): Moved to opt.ads and renamed
SPARK_Mode_Type
Index: sem_aggr.adb
===================================================================
--- sem_aggr.adb (revision 206841)
+++ sem_aggr.adb (working copy)
@@ -597,7 +597,7 @@
elsif Expr_Value (This_Low) /= Expr_Value (Aggr_Low (Dim)) then
Set_Raises_Constraint_Error (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("sub-aggregate low bound mismatch<<", N);
Error_Msg_N ("\Constraint_Error [<<", N);
end if;
@@ -611,7 +611,7 @@
Expr_Value (This_High) /= Expr_Value (Aggr_High (Dim))
then
Set_Raises_Constraint_Error (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("sub-aggregate high bound mismatch<<", N);
Error_Msg_N ("\Constraint_Error [<<", N);
end if;
@@ -1456,7 +1456,7 @@
if OK_BH and then OK_AH and then Val_BH < Val_AH then
Set_Raises_Constraint_Error (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("upper bound out of range<<", AH);
Error_Msg_N ("\Constraint_Error [<<", AH);
@@ -1500,14 +1500,14 @@
if OK_L and then Val_L > Val_AL then
Set_Raises_Constraint_Error (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("lower bound of aggregate out of range<<", N);
Error_Msg_N ("\Constraint_Error [<<", N);
end if;
if OK_H and then Val_H < Val_AH then
Set_Raises_Constraint_Error (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("upper bound of aggregate out of range<<", N);
Error_Msg_N ("\Constraint_Error [<<", N);
end if;
@@ -1548,7 +1548,7 @@
if Range_Len < Len then
Set_Raises_Constraint_Error (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("too many elements<<", N);
Error_Msg_N ("\Constraint_Error [<<", N);
end if;
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 206841)
+++ sem_ch3.adb (working copy)
@@ -3797,7 +3797,7 @@
and then Present (Get_Attribute_Definition_Clause
(E, Attribute_Address))
then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N
("more than one task with same entry address<<", N);
Error_Msg_N ("\Program_Error [<<", N);
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 206804)
+++ sem_ch7.adb (working copy)
@@ -56,6 +56,7 @@
with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sem_Warn; use Sem_Warn;
with Snames; use Snames;
@@ -345,6 +346,13 @@
Push_Scope (Spec_Id);
+ -- Set SPARK_Mode from spec if package spec had SPARK_Mode pragma
+
+ if Present (SPARK_Mode_Pragmas (Spec_Id)) then
+ SPARK_Mode :=
+ Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+ end if;
+
Set_Categorization_From_Pragmas (N);
Install_Visible_Declarations (Spec_Id);
Index: types.ads
===================================================================
--- types.ads (revision 206804)
+++ types.ads (working copy)
@@ -882,12 +882,4 @@
SE_Empty_Storage_Pool ..
SE_Object_Too_Large;
- ----------------------------------------
- -- Types Used for SPARK Mode Handling --
- ----------------------------------------
-
- type SPARK_Mode_Id is (None, SPARK_Off, SPARK_Auto, SPARK_On);
- -- Type used to represent all legal modes that can be set by aspect/pragma
- -- SPARK_Mode.
-
end Types;
Index: checks.adb
===================================================================
--- checks.adb (revision 206841)
+++ checks.adb (working copy)
@@ -3697,7 +3697,7 @@
-- Here we have the optimizable case, warn if not short-circuited
if K = N_Op_And or else K = N_Op_Or then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
case Check is
when Access_Check =>
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 206837)
+++ sem_prag.adb (working copy)
@@ -47,7 +47,6 @@
with Namet.Sp; use Namet.Sp;
with Nlists; use Nlists;
with Nmake; use Nmake;
-with Opt; use Opt;
with Output; use Output;
with Par_SCO; use Par_SCO;
with Restrict; use Restrict;
@@ -253,10 +252,10 @@
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
- function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id;
+ function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
-- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
- -- Get_SPARK_Mode_Id. Convert a name into a corresponding value of type
- -- SPARK_Mode_Id.
+ -- Get_SPARK_Mode_Type. Convert a name into a corresponding value of type
+ -- SPARK_Mode_Type.
function Is_Part_Of
(State : Entity_Id;
@@ -18065,8 +18064,7 @@
New_Id : Entity_Id);
-- Verify the "monotonicity" of SPARK modes between two entities.
-- The order of modes is Off < Auto < On. Governing_Id establishes
- -- the mode of the context. New_Id attempts to redefine the known
- -- mode.
+ -- the mode of the context. New_Id is the desired new mode.
procedure Check_Pragma_Conformance
(Governing_Mode : Node_Id;
@@ -18076,8 +18074,8 @@
-- mode dictated by the context. New_Mode attempts to redefine the
-- governing mode.
- function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id;
- -- Convert a value of type SPARK_Mode_Id into a corresponding name
+ function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id;
+ -- Convert a value of type SPARK_Mode_Type to corresponding name
------------------
-- Chain_Pragma --
@@ -18086,22 +18084,19 @@
procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id) is
Existing_Prag : constant Node_Id :=
SPARK_Mode_Pragmas (Context);
+
begin
- -- The context does not have a prior mode defined
+ -- Chain existing pragmas to this one, checking consistency
- if No (Existing_Prag) then
- Set_SPARK_Mode_Pragmas (Context, Prag);
-
- -- Chain the new mode on the list of SPARK_Mode pragmas. Verify
- -- the consistency between the existing mode and the new one.
-
- else
- Set_Next_Pragma (Existing_Prag, Prag);
-
+ if Present (Existing_Prag) then
Check_Pragma_Conformance
(Governing_Mode => Existing_Prag,
New_Mode => Prag);
+
+ Set_Next_Pragma (Prag, Existing_Prag);
end if;
+
+ Set_SPARK_Mode_Pragmas (Context, Prag);
end Chain_Pragma;
----------------------------------
@@ -18150,9 +18145,10 @@
(Governing_Mode : Node_Id;
New_Mode : Node_Id)
is
- Gov_M : constant SPARK_Mode_Id :=
- Get_SPARK_Mode_Id (Governing_Mode);
- New_M : constant SPARK_Mode_Id := Get_SPARK_Mode_Id (New_Mode);
+ Gov_M : constant SPARK_Mode_Type :=
+ Get_SPARK_Mode_From_Pragma (Governing_Mode);
+ New_M : constant SPARK_Mode_Type :=
+ Get_SPARK_Mode_From_Pragma (New_Mode);
begin
-- The new mode is less restrictive than the established mode
@@ -18173,13 +18169,15 @@
-- Get_SPARK_Mode_Name --
-------------------------
- function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id is
+ function Get_SPARK_Mode_Name
+ (Id : SPARK_Mode_Type) return Name_Id
+ is
begin
- if Id = SPARK_On then
+ if Id = On then
return Name_On;
- elsif Id = SPARK_Off then
+ elsif Id = Off then
return Name_Off;
- elsif Id = SPARK_Auto then
+ elsif Id = Auto then
return Name_Auto;
-- Mode "None" should never be used in error message generation
@@ -18194,51 +18192,48 @@
Body_Id : Entity_Id;
Context : Node_Id;
Mode : Name_Id;
- Mode_Id : SPARK_Mode_Id;
+ Mode_Id : SPARK_Mode_Type;
Spec_Id : Entity_Id;
Stmt : Node_Id;
- -- Start of processing for SPARK_Mode
+ -- Start of processing for SPARK_Mod
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
- -- Check the legality of the mode
+ -- Check the legality of the mode (no argument = ON)
if Arg_Count = 1 then
Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_Auto);
Mode := Chars (Get_Pragma_Arg (Arg1));
-
- -- A SPARK_Mode without an argument defaults to "On"
-
else
Mode := Name_On;
end if;
- Mode_Id := Get_SPARK_Mode_Id (Mode);
+ Mode_Id := Get_SPARK_Mode_Type (Mode);
Context := Parent (N);
+ SPARK_Mode := Mode_Id;
-- The pragma appears in a configuration file
if No (Context) then
Check_Valid_Configuration_Pragma;
- Global_SPARK_Mode := Mode_Id;
-- When the pragma is placed before the declaration of a unit, it
-- configures the whole unit.
elsif Nkind (Context) = N_Compilation_Unit then
Check_Valid_Configuration_Pragma;
- Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
+ Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
-- The pragma applies to a [library unit] subprogram or package
else
-- Mode "Auto" cannot be used in nested subprograms or packages
- if Mode_Id = SPARK_Auto then
+ if Mode_Id = Auto then
Error_Pragma_Arg
("mode `Auto` can only apply to the configuration variant "
& "of pragma %", Arg1);
@@ -18256,8 +18251,7 @@
if Pragma_Name (Stmt) = Pname then
Error_Msg_Name_1 := Pname;
Error_Msg_Sloc := Sloc (Stmt);
- Error_Msg_N
- ("pragma % duplicates pragma declared #", N);
+ Error_Msg_N ("pragma% duplicates pragma declared#", N);
end if;
-- Skip internally generated code
@@ -18322,8 +18316,7 @@
Spec_Id := Defining_Unit_Name (Context);
Chain_Pragma (Spec_Id, N);
- -- The pragma is immediately within a package or subprogram
- -- body.
+ -- Pragma is immediately within a package or subprogram body
-- function F ... is
-- pragma SPARK_Mode;
@@ -22845,30 +22838,30 @@
end Get_Base_Subprogram;
-----------------------
- -- Get_SPARK_Mode_Id --
+ -- Get_SPARK_Mode_Type --
-----------------------
- function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id is
+ function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type is
begin
if N = Name_On then
- return SPARK_On;
+ return On;
elsif N = Name_Off then
- return SPARK_Off;
+ return Off;
elsif N = Name_Auto then
- return SPARK_Auto;
+ return Auto;
-- Any other argument is erroneous
else
raise Program_Error;
end if;
- end Get_SPARK_Mode_Id;
+ end Get_SPARK_Mode_Type;
- -----------------------
- -- Get_SPARK_Mode_Id --
- -----------------------
+ --------------------------------
+ -- Get_SPARK_Mode_From_Pragma --
+ --------------------------------
- function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id is
+ function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type is
Args : List_Id;
Mode : Node_Id;
@@ -22880,14 +22873,14 @@
if Present (Args) then
Mode := First (Pragma_Argument_Associations (N));
- return Get_SPARK_Mode_Id (Chars (Get_Pragma_Arg (Mode)));
+ return Get_SPARK_Mode_Type (Chars (Get_Pragma_Arg (Mode)));
- -- When SPARK_Mode appears without an argument, the default is ON
+ -- If SPARK_Mode pragma has no argument, default is ON
else
- return SPARK_On;
+ return On;
end if;
- end Get_SPARK_Mode_Id;
+ end Get_SPARK_Mode_From_Pragma;
----------------
-- Initialize --
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 206804)
+++ sem_prag.ads (working copy)
@@ -27,6 +27,7 @@
-- (logically this processing belongs in chapter 4)
with Namet; use Namet;
+with Opt; use Opt;
with Snames; use Snames;
with Types; use Types;
@@ -130,8 +131,8 @@
-- True have their analysis delayed until after the main program is parsed
-- and analyzed.
- function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id;
- -- Given a pragma SPARK_Mode node, return the corresponding mode id
+ function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
+ -- Given a pragma SPARK_Mode node, return corresponding mode id
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called
Index: sem.adb
===================================================================
--- sem.adb (revision 206827)
+++ sem.adb (working copy)
@@ -32,7 +32,6 @@
with Lib; use Lib;
with Lib.Load; use Lib.Load;
with Nlists; use Nlists;
-with Opt; use Opt;
with Output; use Output;
with Restrict; use Restrict;
with Sem_Attr; use Sem_Attr;
Index: sem.ads
===================================================================
--- sem.ads (revision 206804)
+++ sem.ads (working copy)
@@ -203,6 +203,7 @@
with Alloc;
with Einfo; use Einfo;
+with Opt; use Opt;
with Table;
with Types; use Types;
@@ -474,6 +475,9 @@
Save_Default_Storage_Pool : Node_Id;
-- Save contents of Default_Storage_Pool on entry to restore on exit
+ Save_SPARK_Mode : SPARK_Mode_Type;
+ -- Setting of SPARK_Mode on entry to restore on exit
+
Is_Transient : Boolean;
-- Marks transient scopes (see Exp_Ch7 body for details)
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 206841)
+++ sem_util.adb (working copy)
@@ -578,7 +578,7 @@
begin
if Has_Predicates (Typ) then
if Is_Generic_Actual_Type (Typ) then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_FE (Msg & "<<", N, Typ);
Error_Msg_F ("\Program_Error [<<", N);
Insert_Action (N,
@@ -3268,11 +3268,10 @@
Eloc : Source_Ptr;
begin
- -- If this is a warning, convert it into an error if we are operating
- -- in GNATprove mode, because in SPARK, we are allowed to consider
- -- such warnings as illegalities, and we choose to do so!
+ -- If this is a warning, convert it into an error if we are in code
+ -- subject to SPARK_Mode being set ON.
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
-- A static constraint error in an instance body is not a fatal error.
-- we choose to inhibit the message altogether, because there is no
@@ -3414,7 +3413,7 @@
end loop;
if Msgs then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
if Present (Ent) then
Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc);
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 206841)
+++ sem_res.adb (working copy)
@@ -769,7 +769,7 @@
and then Nkind (Parent (P)) = N_Subprogram_Body
and then Is_Empty_List (Declarations (Parent (P)))
then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("!infinite recursion<<", N);
Error_Msg_N ("\!Storage_Error [<<", N);
Insert_Action (N,
@@ -868,7 +868,7 @@
end if;
end loop;
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("!possible infinite recursion<<", N);
Error_Msg_N ("\!??Storage_Error ]<<", N);
@@ -4555,7 +4555,7 @@
Deepest_Type_Access_Level (Typ)
then
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N
("type in allocator has deeper level than "
& "designated class-wide type<<", E);
@@ -4666,7 +4666,7 @@
and then Ekind (Current_Scope) = E_Package
and then not In_Package_Body (Current_Scope)
then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("cannot activate task before body seen<<", N);
Error_Msg_N ("\Program_Error [<<", N);
end if;
@@ -4680,7 +4680,7 @@
and then Present (Subpool_Handle_Name (N))
and then Has_Task (Desig_T)
then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("cannot allocate task on subpool<<", N);
Error_Msg_N ("\Program_Error [<<", N);
@@ -5396,7 +5396,7 @@
and then Is_Entry_Barrier_Function (P))
then
Rtype := Etype (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_NE
("& should not be used in entry body (RM C.7(17))<<",
N, Nam);
@@ -5697,7 +5697,7 @@
-- Here warning is to be issued
Set_Has_Recursive_Call (Nam);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("possible infinite recursion<<!", N);
Error_Msg_N ("\Storage_Error ]<<!", N);
end if;
@@ -6011,7 +6011,7 @@
end loop;
if not Call_OK then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("!cannot determine tag of result<<", N);
Error_Msg_N ("\Program_Error [<<!", N);
Insert_Action (N,
@@ -10877,7 +10877,7 @@
Deepest_Type_Access_Level (Opnd_Type)
then
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Conversion_Error_N
("source array type has deeper accessibility "
& "level than target<<", Operand);
@@ -11186,7 +11186,7 @@
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Conversion_Error_N
("cannot convert local pointer to non-local access type<<",
Operand);
@@ -11219,7 +11219,7 @@
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Conversion_Error_N
("cannot convert access discriminant to non-local "
& "access type<<", Operand);
@@ -11366,7 +11366,7 @@
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Conversion_Error_N
("cannot convert local pointer to non-local access type<<",
Operand);
@@ -11406,7 +11406,7 @@
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Conversion_Error_N
("cannot convert access discriminant to non-local "
& "access type<<", Operand);
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 206841)
+++ sem_attr.adb (working copy)
@@ -5396,7 +5396,7 @@
Name_Simple_Storage_Pool_Type))
then
Error_Msg_Name_1 := Aname;
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("cannot use % attribute for type with simple "
& "storage pool<<", N);
Error_Msg_N ("\Program_Error [<<", N);
@@ -9311,7 +9311,7 @@
-- know will fail, so generate an appropriate warning.
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_F
("non-local pointer cannot point to local object<<", P);
Error_Msg_F ("\Program_Error [<<", P);
@@ -9792,7 +9792,7 @@
-- know will fail, so generate an appropriate warning.
if In_Instance_Body then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_F
("non-local pointer cannot point to local object<<", P);
Error_Msg_F ("\Program_Error [<<", P);
Index: sem_elab.adb
===================================================================
--- sem_elab.adb (revision 206841)
+++ sem_elab.adb (working copy)
@@ -1138,7 +1138,7 @@
-- Here we definitely have a bad instantiation
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_NE ("cannot instantiate& before body seen<<", N, Ent);
if Present (Instance_Spec (N)) then
@@ -2179,7 +2179,7 @@
-- level, and the ABE is bound to occur.
if Elab_Call.Last = 0 then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
if Inst_Case then
Error_Msg_NE
@@ -2263,7 +2263,7 @@
and then (Nkind (Original_Node (N)) /= N_Function_Call
or else not In_Assertion_Expression (Original_Node (N)))
then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
if Inst_Case then
Error_Msg_NE
@@ -2370,7 +2370,7 @@
or else
Scope (Proc) = Scope (Defining_Identifier (Decl)))
then
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N
("task will be activated before elaboration of its body<<",
Decl);
Index: exp_ch4.adb
===================================================================
--- exp_ch4.adb (revision 206841)
+++ exp_ch4.adb (working copy)
@@ -9654,7 +9654,7 @@
procedure Raise_Accessibility_Error is
begin
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Rewrite (N,
Make_Raise_Program_Error (Sloc (N),
Reason => PE_Accessibility_Check_Failed));
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb (revision 206843)
+++ sem_ch4.adb (working copy)
@@ -4651,7 +4651,7 @@
-- In SPARK mode, this is made into an error to simplify
-- the processing of the formal verification backend.
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Apply_Compile_Time_Constraint_Error
(N, "component not present in }<<",
CE_Discriminant_Check_Failed,
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 206841)
+++ sem_ch6.adb (working copy)
@@ -983,7 +983,7 @@
Reason => PE_Accessibility_Check_Failed));
Analyze (N);
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N ("cannot return a local value by reference<<", N);
Error_Msg_NE ("\& [<<", N, Standard_Program_Error);
end if;
@@ -2987,6 +2987,13 @@
Push_Scope (Spec_Id);
+ -- Set SPARK_Mode from spec if spec had a SPARK_Mode pragma
+
+ if Present (SPARK_Mode_Pragmas (Spec_Id)) then
+ SPARK_Mode :=
+ Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+ 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.
@@ -7223,7 +7230,7 @@
-- In GNATprove mode, it is an error to have a missing return
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_N
("RETURN statement missing following this statement<<!",
Last_Stm);
@@ -7252,7 +7259,7 @@
& "will raise Program_Error??", Last_Stm);
end if;
- Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_Warn := SPARK_Mode /= On;
Error_Msg_NE
("\procedure & is marked as No_Return<<!", Last_Stm, Proc);
end if;
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb (revision 206813)
+++ sem_ch8.adb (working copy)
@@ -7395,6 +7395,7 @@
Local_Suppress_Stack_Top := SST.Save_Local_Suppress_Stack_Top;
Check_Policy_List := SST.Save_Check_Policy_List;
Default_Pool := SST.Save_Default_Storage_Pool;
+ SPARK_Mode := SST.Save_SPARK_Mode;
if Debug_Flag_W then
Write_Str ("<-- exiting scope: ");
@@ -7468,6 +7469,7 @@
SST.Save_Local_Suppress_Stack_Top := Local_Suppress_Stack_Top;
SST.Save_Check_Policy_List := Check_Policy_List;
SST.Save_Default_Storage_Pool := Default_Pool;
+ SST.Save_SPARK_Mode := SPARK_Mode;
if Scope_Stack.Last > Scope_Stack.First then
SST.Component_Alignment_Default := Scope_Stack.Table
Index: opt.adb
===================================================================
--- opt.adb (revision 206806)
+++ opt.adb (working copy)
@@ -63,6 +63,7 @@
Persistent_BSS_Mode_Config := Persistent_BSS_Mode;
Polling_Required_Config := Polling_Required;
Short_Descriptors_Config := Short_Descriptors;
+ SPARK_Mode_Config := SPARK_Mode;
Use_VADS_Size_Config := Use_VADS_Size;
-- Reset the indication that Optimize_Alignment was set locally, since
@@ -98,6 +99,7 @@
Persistent_BSS_Mode := Save.Persistent_BSS_Mode;
Polling_Required := Save.Polling_Required;
Short_Descriptors := Save.Short_Descriptors;
+ SPARK_Mode := Save.SPARK_Mode;
Use_VADS_Size := Save.Use_VADS_Size;
-- Update consistently the value of Init_Or_Norm_Scalars. The value of
@@ -134,6 +136,7 @@
Save.Persistent_BSS_Mode := Persistent_BSS_Mode;
Save.Polling_Required := Polling_Required;
Save.Short_Descriptors := Short_Descriptors;
+ Save.SPARK_Mode := SPARK_Mode;
Save.Use_VADS_Size := Use_VADS_Size;
end Save_Opt_Config_Switches;
@@ -164,6 +167,7 @@
Persistent_BSS_Mode := False;
Use_VADS_Size := False;
Optimize_Alignment_Local := True;
+ SPARK_Mode := Auto;
-- For an internal unit, assertions/debug pragmas are off unless this
-- is the main unit and they were explicitly enabled. We also make
@@ -198,6 +202,7 @@
Optimize_Alignment := Optimize_Alignment_Config;
Optimize_Alignment_Local := False;
Persistent_BSS_Mode := Persistent_BSS_Mode_Config;
+ SPARK_Mode := SPARK_Mode_Config;
Use_VADS_Size := Use_VADS_Size_Config;
-- Update consistently the value of Init_Or_Norm_Scalars. The value
Index: opt.ads
===================================================================
--- opt.ads (revision 206837)
+++ opt.ads (working copy)
@@ -1,5 +1,5 @@
------------------------------------------------------------------------------
--- --
+-- SPARK
--
-- GNAT COMPILER COMPONENTS --
-- --
-- O P T --
@@ -1264,6 +1264,14 @@
-- GNAT
-- Set True if a pragma Short_Descriptors applies to the current unit.
+ type SPARK_Mode_Type is (None, Off, Auto, On);
+ pragma Ordered (SPARK_Mode_Type);
+ -- Possible legal modes that can be set by aspect/pragma SPARK_Mode
+
+ SPARK_Mode : SPARK_Mode_Type := None;
+ -- GNAT
+ -- Current SPARK mode setting
+
Special_Exception_Package_Used : Boolean := False;
-- GNAT
-- Set to True if either of the unit GNAT.Most_Recent_Exception or
@@ -1895,6 +1903,9 @@
-- This flag is used to set the initial value for Short_Descriptors at the
-- start of analyzing each unit.
+ SPARK_Mode_Config : SPARK_Mode_Type := None;
+ -- The setting of SPARK_Mode from configuration pragmas
+
Use_VADS_Size_Config : Boolean;
-- GNAT
-- This is the value of the configuration switch that controls the use of
@@ -2001,10 +2012,6 @@
-- Modes for Formal Verification --
-----------------------------------
- Global_SPARK_Mode : SPARK_Mode_Id := None;
- -- The mode applicable to the whole compilation. The global mode can be set
- -- in a configuration file such as gnat.adc.
-
GNATprove_Mode : Boolean := False;
-- Specific compiling mode targeting formal verification for those parts
-- of the input code that belong to the SPARK 2014 subset of Ada. Set True
@@ -2043,6 +2050,7 @@
Persistent_BSS_Mode : Boolean;
Polling_Required : Boolean;
Short_Descriptors : Boolean;
+ SPARK_Mode : SPARK_Mode_Type;
Use_VADS_Size : Boolean;
end record;
