procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[multiple changes]

Browse source 
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.

From-SVN: r206844
This commit is contained in:
Arnaud Charlet 2014-01-20 17:10:53 +01:00
parent e4deba8e2f
commit 43417b90cf
24 changed files with 215 additions and 111 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
gcc/ada/ChangeLog
View file

@ -1,3 +1,64 @@
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.

9
gcc/ada/atree.adb
View file

@ -733,6 +733,7 @@ package body Atree is
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));
@ -1105,19 +1106,27 @@ package body Atree is
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

2
gcc/ada/checks.adb
View file

@ -3697,7 +3697,7 @@ package body Checks is
-- 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 =>

2
gcc/ada/exp_ch4.adb
View file

@ -9654,7 +9654,7 @@ package body Exp_Ch4 is
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));

4
gcc/ada/exp_ch5.adb
View file

@ -1850,12 +1850,14 @@ package body Exp_Ch5 is
-- 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

5
gcc/ada/opt.adb
View file

@ -63,6 +63,7 @@ package body Opt is
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 @@ package body Opt is
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 @@ package body Opt is
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 @@ package body Opt is
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 @@ package body Opt is
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

18
gcc/ada/opt.ads
View file

@ -1,5 +1,5 @@
------------------------------------------------------------------------------
-- --
-- SPARK --
-- GNAT COMPILER COMPONENTS --
-- --
-- O P T --
@ -1264,6 +1264,14 @@ package Opt is
-- 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 @@ package Opt is
-- 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 @@ package Opt is
-- 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 @@ private
Persistent_BSS_Mode : Boolean;
Polling_Required : Boolean;
Short_Descriptors : Boolean;
SPARK_Mode : SPARK_Mode_Type;
Use_VADS_Size : Boolean;
end record;

1
gcc/ada/sem.adb
View file

@ -32,7 +32,6 @@ with Fname; use Fname;
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;

4
gcc/ada/sem.ads
View file

@ -203,6 +203,7 @@
with Alloc;
with Einfo; use Einfo;
with Opt; use Opt;
with Table;
with Types; use Types;
@ -474,6 +475,9 @@ package Sem is
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)

12
gcc/ada/sem_aggr.adb
View file

@ -597,7 +597,7 @@ package body Sem_Aggr is
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 @@ package body Sem_Aggr is
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 @@ package body Sem_Aggr is
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 @@ package body Sem_Aggr is
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 @@ package body Sem_Aggr is
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;

6
gcc/ada/sem_attr.adb
View file

@ -5396,7 +5396,7 @@ package body Sem_Attr is
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 @@ package body Sem_Attr is
-- 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 @@ package body Sem_Attr is
-- 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);

4
gcc/ada/sem_ch12.adb
View file

@ -13061,13 +13061,13 @@ package body Sem_Ch12 is
-- 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);

14
gcc/ada/sem_ch13.adb
View file

@ -5939,6 +5939,20 @@ package body Sem_Ch13 is
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

2
gcc/ada/sem_ch3.adb
View file

@ -3797,7 +3797,7 @@ package body Sem_Ch3 is
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);

2
gcc/ada/sem_ch4.adb
View file

@ -4651,7 +4651,7 @@ package body Sem_Ch4 is
-- 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,

13
gcc/ada/sem_ch6.adb
View file

@ -983,7 +983,7 @@ package body Sem_Ch6 is
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 @@ package body Sem_Ch6 is
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 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
& "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;

8
gcc/ada/sem_ch7.adb
View file

@ -56,6 +56,7 @@ with Sem_Ch12; use Sem_Ch12;
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 @@ package body Sem_Ch7 is
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);

2
gcc/ada/sem_ch8.adb
View file

@ -7395,6 +7395,7 @@ package body Sem_Ch8 is
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 @@ package body Sem_Ch8 is
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

8
gcc/ada/sem_elab.adb
View file

@ -1138,7 +1138,7 @@ package body Sem_Elab is
-- 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 @@ package body Sem_Elab is
-- 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 @@ package body Sem_Elab is
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 @@ package body Sem_Elab is
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);

99
gcc/ada/sem_prag.adb
View file

@ -47,7 +47,6 @@ with Lib.Xref; use Lib.Xref;
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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);
-- 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;
----------------------------------
@ -18150,9 +18145,10 @@ package body Sem_Prag is
(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 @@ package body Sem_Prag is
-- 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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 --

5
gcc/ada/sem_prag.ads
View file

@ -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 @@ package Sem_Prag is
-- 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

26
gcc/ada/sem_res.adb
View file

@ -769,7 +769,7 @@ package body Sem_Res is
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 @@ package body Sem_Res is
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 @@ package body Sem_Res is
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 @@ package body Sem_Res is
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 @@ package body Sem_Res is
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 @@ package body Sem_Res is
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 @@ package body Sem_Res is
-- 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 @@ package body Sem_Res is
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 @@ package body Sem_Res is
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 @@ package body Sem_Res is
-- 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 @@ package body Sem_Res is
-- 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 @@ package body Sem_Res is
-- 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 @@ package body Sem_Res is
-- 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);

11
gcc/ada/sem_util.adb
View file

@ -578,7 +578,7 @@ package body Sem_Util is
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 @@ package body Sem_Util is
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 @@ package body Sem_Util is
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);

8
gcc/ada/types.ads
View file

@ -882,12 +882,4 @@ package Types is
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;