+2014-01-20 Robert Dewar <dewar@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
+
+2014-01-20 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch13.adb: Add semantic information to rewritten type
+ reference.
+
+2014-01-20 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_ch5.adb (Expand_N_Assignment_Statement): If both sides
+ are of a type with unknown discriminants, convert both to the
+ underlying view of the type, so that the proper constraint check
+ can be applied to the right-hand side.
+
+2014-01-20 Robert Dewar <dewar@adacore.com>
+
+ * atree.adb (Copy_Node): Fix failure to copy last component
+ (Exchange_Entities): Fix failure to exchange last entity
+
+2014-01-20 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch12.adb: Code clean up.
+
2014-01-20 Robert Dewar <dewar@adacore.com>
* gnat_rm.texi, sem_ch4.adb: Minor reformatting.
Nodes.Table (Destination + 2) := Nodes.Table (Source + 2);
Nodes.Table (Destination + 3) := Nodes.Table (Source + 3);
Nodes.Table (Destination + 4) := Nodes.Table (Source + 4);
+ Nodes.Table (Destination + 5) := Nodes.Table (Source + 5);
else
pragma Assert (not Has_Extension (Source));
Temp_Ent := Nodes.Table (E1);
Nodes.Table (E1) := Nodes.Table (E2);
Nodes.Table (E2) := Temp_Ent;
+
Temp_Ent := Nodes.Table (E1 + 1);
Nodes.Table (E1 + 1) := Nodes.Table (E2 + 1);
Nodes.Table (E2 + 1) := Temp_Ent;
+
Temp_Ent := Nodes.Table (E1 + 2);
Nodes.Table (E1 + 2) := Nodes.Table (E2 + 2);
Nodes.Table (E2 + 2) := Temp_Ent;
+
Temp_Ent := Nodes.Table (E1 + 3);
Nodes.Table (E1 + 3) := Nodes.Table (E2 + 3);
Nodes.Table (E2 + 3) := Temp_Ent;
+
Temp_Ent := Nodes.Table (E1 + 4);
Nodes.Table (E1 + 4) := Nodes.Table (E2 + 4);
Nodes.Table (E2 + 4) := Temp_Ent;
+ Temp_Ent := Nodes.Table (E1 + 5);
+ Nodes.Table (E1 + 5) := Nodes.Table (E2 + 5);
+ Nodes.Table (E2 + 5) := Temp_Ent;
+
-- That exchange exchanged the parent pointers as well, which is what
-- we want, but we need to patch up the defining identifier pointers
-- in the parent nodes (the child pointers) to match this switch
-- 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 =>
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));
-- If the Lhs has a private type with unknown discriminants, it
-- may have a full view with discriminants, but those are nameable
-- only in the underlying type, so convert the Rhs to it before
- -- potential checking.
+ -- potential checking. Convert Lhs as well, otherwise the actual
+ -- subtype might not be constructible.
elsif Has_Unknown_Discriminants (Base_Type (Etype (Lhs)))
and then Has_Discriminants (Typ)
then
Rewrite (Rhs, OK_Convert_To (Base_Type (Typ), Rhs));
+ Rewrite (Lhs, OK_Convert_To (Base_Type (Typ), Lhs));
Apply_Discriminant_Check (Rhs, Typ, Lhs);
-- In the access type case, we need the same discriminant check, and
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
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
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;
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
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
------------------------------------------------------------------------------
--- --
+-- SPARK --
-- GNAT COMPILER COMPONENTS --
-- --
-- O P T --
-- 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
-- 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
-- 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
Persistent_BSS_Mode : Boolean;
Polling_Required : Boolean;
Short_Descriptors : Boolean;
+ SPARK_Mode : SPARK_Mode_Type;
Use_VADS_Size : Boolean;
end record;
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;
with Alloc;
with Einfo; use Einfo;
+with Opt; use Opt;
with Table;
with Types; use Types;
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)
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;
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;
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);
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;
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;
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);
-- 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);
-- 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);
-- ASIS tree traversal, so we recover the original entity to
-- expose the renaming. Take into account that the context may
-- be a nested generic and that the original node may itself
- -- have an associated node.
+ -- have an associated node that had better be an entity.
if Ekind (E) = E_Package
and then Nkind (Parent (N)) = N_Expanded_Name
and then Present (Original_Node (N2))
+ and then Is_Entity_Name (Original_Node (N2))
and then Present (Entity (Original_Node (N2)))
- and then Is_Entity_Name (Entity (Original_Node (N2)))
then
if Is_Global (Entity (Original_Node (N2))) then
N2 := Original_Node (N2);
procedure Replace_Type_Reference (N : Node_Id) is
begin
+
+ -- Add semantic information to node to be rewritten, for ASIS
+ -- navigation needs.
+
+ if Nkind (N) = N_Identifier then
+ Set_Entity (N, T);
+ Set_Etype (N, T);
+
+ elsif Nkind (N) = N_Selected_Component then
+ Analyze (Prefix (N));
+ Set_Entity (Selector_Name (N), T);
+ Set_Etype (Selector_Name (N), T);
+ end if;
+
-- Invariant'Class, replace with T'Class (obj)
if Class_Present (Ritem) then
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);
-- 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,
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;
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.
-- 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);
& "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;
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;
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);
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: ");
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
-- 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
-- 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
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
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);
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;
-- 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;
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;
-- 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 --
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
-
- 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);
+ begin
+ -- Chain existing pragmas to this one, checking consistency
+ 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;
----------------------------------
(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
-- 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
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);
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
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;
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;
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 --
-- (logically this processing belongs in chapter 4)
with Namet; use Namet;
+with Opt; use Opt;
with Snames; use Snames;
with Types; use Types;
-- 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
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,
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);
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);
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;
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);
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);
-- 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;
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,
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);
-- 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);
-- 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);
-- 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);
-- 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);
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,
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
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);
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;
projects / thirdparty / gcc.git / commitdiff
