Commit ddd2bec5 by Arnaud Charlet

[multiple changes]

2014-02-19  Yannick Moy  <moy@adacore.com>

	* sem_ch10.adb (Analyze_Proper_Body): Issue error on missing
	subunit in GNATprove_Mode.
	* sinfo.ads (GNATprove_Mode): Document error issued in GNATprove_Mode.

2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* lib-xref.ads Alphabetize the contents of table
	Xref_Entity_Letters. Add an entry in table Xref_Entity_Letters
	for E_Abstract_State. List all letters and symbols in use.
	* sem_prag.adb (Analyze_Abstract_State): Update all calls
	to Create_Abstract_State to reflect the new signature.
	(Create_Abstract_State): Change subprogram profile and update
	the comment on usage. Use the proper location of the state
	declaration when creating a new abstract state entity. Do not
	generate an external name, but simply reuse the name coming from
	the state declaration.

From-SVN: r207884
parent 3a845e07
2014-02-19 Yannick Moy <moy@adacore.com>
* sem_ch10.adb (Analyze_Proper_Body): Issue error on missing
subunit in GNATprove_Mode.
* sinfo.ads (GNATprove_Mode): Document error issued in GNATprove_Mode.
2014-02-19 Hristian Kirtchev <kirtchev@adacore.com>
* lib-xref.ads Alphabetize the contents of table
Xref_Entity_Letters. Add an entry in table Xref_Entity_Letters
for E_Abstract_State. List all letters and symbols in use.
* sem_prag.adb (Analyze_Abstract_State): Update all calls
to Create_Abstract_State to reflect the new signature.
(Create_Abstract_State): Change subprogram profile and update
the comment on usage. Use the proper location of the state
declaration when creating a new abstract state entity. Do not
generate an external name, but simply reuse the name coming from
the state declaration.
2014-02-19 Robert Dewar <dewar@adacore.com>
* exp_ch4.adb (Expand_N_Expression_With_Actions): Make sure
......
......@@ -433,95 +433,87 @@ package Lib.Xref is
-- indicating procedures and functions. If the operation is abstract,
-- these letters are replaced in the xref by 'x' and 'y' respectively.
Xref_Entity_Letters : array (Entity_Kind) of Character :=
(E_Void => ' ',
E_Variable => '*',
E_Component => '*',
E_Constant => '*',
E_Discriminant => '*',
E_Loop_Parameter => '*',
E_In_Parameter => '*',
E_Out_Parameter => '*',
E_In_Out_Parameter => '*',
E_Generic_In_Out_Parameter => '*',
E_Generic_In_Parameter => '*',
E_Named_Integer => 'N',
E_Named_Real => 'N',
E_Enumeration_Type => 'E', -- B for boolean
E_Enumeration_Subtype => 'E', -- B for boolean
-- The following letters and symbols are currently in use:
-- A B C D E F I K L M N O P R S T U V W X Y
-- a b c d e f i k l m n o p q r s t u v w x y
-- @ * + space
E_Signed_Integer_Type => 'I',
E_Signed_Integer_Subtype => 'I',
E_Modular_Integer_Type => 'M',
E_Modular_Integer_Subtype => 'M',
E_Ordinary_Fixed_Point_Type => 'O',
E_Ordinary_Fixed_Point_Subtype => 'O',
E_Decimal_Fixed_Point_Type => 'D',
E_Decimal_Fixed_Point_Subtype => 'D',
E_Floating_Point_Type => 'F',
E_Floating_Point_Subtype => 'F',
E_Access_Type => 'P',
E_Access_Subtype => 'P',
Xref_Entity_Letters : array (Entity_Kind) of Character :=
(E_Abstract_State => '@',
E_Access_Attribute_Type => 'P',
E_Allocator_Type => ' ',
E_General_Access_Type => 'P',
E_Access_Subprogram_Type => 'P',
E_Access_Protected_Subprogram_Type => 'P',
E_Anonymous_Access_Subprogram_Type => ' ',
E_Access_Subprogram_Type => 'P',
E_Access_Subtype => 'P',
E_Access_Type => 'P',
E_Allocator_Type => ' ',
E_Anonymous_Access_Protected_Subprogram_Type => ' ',
E_Anonymous_Access_Subprogram_Type => ' ',
E_Anonymous_Access_Type => ' ',
E_Array_Type => 'A',
E_Array_Subtype => 'A',
E_String_Type => 'S',
E_String_Subtype => 'S',
E_String_Literal_Subtype => ' ',
E_Class_Wide_Type => 'C',
E_Array_Type => 'A',
E_Block => 'q',
E_Class_Wide_Subtype => 'C',
E_Record_Type => 'R',
E_Record_Subtype => 'R',
E_Record_Type_With_Private => 'R',
E_Record_Subtype_With_Private => 'R',
E_Private_Type => '+',
E_Private_Subtype => '+',
E_Limited_Private_Type => '+',
E_Limited_Private_Subtype => '+',
E_Incomplete_Type => '+',
E_Incomplete_Subtype => '+',
E_Task_Type => 'T',
E_Task_Subtype => 'T',
E_Protected_Type => 'W',
E_Protected_Subtype => 'W',
E_Exception_Type => ' ',
E_Subprogram_Type => ' ',
E_Enumeration_Literal => 'n',
E_Function => 'V',
E_Operator => 'V',
E_Procedure => 'U',
E_Class_Wide_Type => 'C',
E_Component => '*',
E_Constant => '*',
E_Decimal_Fixed_Point_Subtype => 'D',
E_Decimal_Fixed_Point_Type => 'D',
E_Discriminant => '*',
E_Entry => 'Y',
E_Entry_Family => 'Y',
E_Block => 'q',
E_Entry_Index_Parameter => '*',
E_Enumeration_Literal => 'n',
E_Enumeration_Subtype => 'E', -- B for boolean
E_Enumeration_Type => 'E', -- B for boolean
E_Exception => 'X',
E_Exception_Type => ' ',
E_Floating_Point_Subtype => 'F',
E_Floating_Point_Type => 'F',
E_Function => 'V',
E_General_Access_Type => 'P',
E_Generic_Function => 'v',
E_Generic_In_Out_Parameter => '*',
E_Generic_In_Parameter => '*',
E_Generic_Package => 'k',
E_Generic_Procedure => 'u',
E_Label => 'L',
E_Limited_Private_Subtype => '+',
E_Limited_Private_Type => '+',
E_Loop => 'l',
E_Return_Statement => ' ',
E_Loop_Parameter => '*',
E_In_Out_Parameter => '*',
E_In_Parameter => '*',
E_Incomplete_Subtype => '+',
E_Incomplete_Type => '+',
E_Modular_Integer_Subtype => 'M',
E_Modular_Integer_Type => 'M',
E_Named_Integer => 'N',
E_Named_Real => 'N',
E_Operator => 'V',
E_Ordinary_Fixed_Point_Subtype => 'O',
E_Ordinary_Fixed_Point_Type => 'O',
E_Out_Parameter => '*',
E_Package => 'K',
E_Private_Subtype => '+',
E_Private_Type => '+',
E_Procedure => 'U',
E_Protected_Subtype => 'W',
E_Protected_Type => 'W',
E_Record_Subtype => 'R',
E_Record_Subtype_With_Private => 'R',
E_Record_Type => 'R',
E_Record_Type_With_Private => 'R',
E_Return_Statement => ' ',
E_Signed_Integer_Subtype => 'I',
E_Signed_Integer_Type => 'I',
E_String_Literal_Subtype => ' ',
E_String_Subtype => 'S',
E_String_Type => 'S',
E_Subprogram_Type => ' ',
E_Task_Subtype => 'T',
E_Task_Type => 'T',
E_Variable => '*',
E_Void => ' ',
-- The following entities are not ones to which we gather the cross-
-- references, since it does not make sense to do so (e.g. references to
......@@ -529,15 +521,10 @@ package Lib.Xref is
-- body entity is considered to be a reference to the spec entity.
E_Package_Body => ' ',
E_Protected_Object => ' ',
E_Protected_Body => ' ',
E_Task_Body => ' ',
E_Protected_Object => ' ',
E_Subprogram_Body => ' ',
-- ??? The following letter is added for completion, proper design and
-- implementation of abstract state cross-referencing to follow.
E_Abstract_State => ' ');
E_Task_Body => ' ');
-- The following table is for information purposes. It shows the use of
-- each character appearing as an entity type.
......
......@@ -1563,8 +1563,9 @@ package body Sem_Ch10 is
procedure Optional_Subunit;
-- This procedure is called when the main unit is a stub, or when we
-- are not generating code. In such a case, we analyze the subunit if
-- present, which is user-friendly and in fact required for ASIS, but
-- we don't complain if the subunit is missing.
-- present, which is user-friendly and in fact required for ASIS, but we
-- don't complain if the subunit is missing. In GNATprove_Mode, we issue
-- an error to avoid formal verification of a partial unit.
----------------------
-- Optional_Subunit --
......@@ -1579,18 +1580,18 @@ package body Sem_Ch10 is
-- ignore all errors. Note that Fatal_Error will still be set, so we
-- will be able to check for this case below.
if not ASIS_Mode then
if not (ASIS_Mode or GNATprove_Mode) then
Ignore_Errors_Enable := Ignore_Errors_Enable + 1;
end if;
Unum :=
Load_Unit
(Load_Name => Subunit_Name,
Required => False,
Required => GNATprove_Mode,
Subunit => True,
Error_Node => N);
if not ASIS_Mode then
if not (ASIS_Mode or GNATprove_Mode) then
Ignore_Errors_Enable := Ignore_Errors_Enable - 1;
end if;
......
......@@ -9986,14 +9986,16 @@ package body Sem_Prag is
-- Opt is not a duplicate property and sets the flag Status.
procedure Create_Abstract_State
(State_Nam : Name_Id;
State_Decl : Node_Id;
Is_Null : Boolean := False);
-- Generate an abstract state entity with name State_Nam and
-- enter it into visibility. State_Decl is the "declaration"
-- of the state as it appears in pragma Abstract_State. Flag
-- Is_Null should be set when the associated Abstract_State
-- pragma defines a null state.
(Nam : Name_Id;
Decl : Node_Id;
Loc : Source_Ptr;
Is_Null : Boolean);
-- Generate an abstract state entity with name Nam and enter it
-- into visibility. Decl is the "declaration" of the state as
-- it appears in pragma Abstract_State. Loc is the location of
-- the related state "declaration". Flag Is_Null should be set
-- when the associated Abstract_State pragma defines a null
-- state.
-----------------------------
-- Analyze_External_Option --
......@@ -10243,17 +10245,16 @@ package body Sem_Prag is
---------------------------
procedure Create_Abstract_State
(State_Nam : Name_Id;
State_Decl : Node_Id;
Is_Null : Boolean := False)
(Nam : Name_Id;
Decl : Node_Id;
Loc : Source_Ptr;
Is_Null : Boolean)
is
begin
-- The generated state abstraction reuses the same chars
-- from the original state declaration. Decorate the entity.
State_Id :=
Make_Defining_Identifier (Sloc (State),
Chars => New_External_Name (State_Nam));
State_Id := Make_Defining_Identifier (Loc, Nam);
-- Null states never come from source
......@@ -10270,15 +10271,16 @@ package body Sem_Prag is
-- N_Null and does not carry any linkages.
if not Is_Null then
if Present (State_Decl) then
Set_Entity (State_Decl, State_Id);
Set_Etype (State_Decl, Standard_Void_Type);
if Present (Decl) then
Set_Entity (Decl, State_Id);
Set_Etype (Decl, Standard_Void_Type);
end if;
-- Every non-null state must be nameable and resolvable
-- the same way a constant is.
-- Every non-null state must be defined, nameable and
-- resolvable.
Push_Scope (Pack_Id);
Generate_Definition (State_Id);
Enter_Name (State_Id);
Pop_Scope;
end if;
......@@ -10303,9 +10305,10 @@ package body Sem_Prag is
elsif Nkind (State) = N_Null then
Create_Abstract_State
(State_Nam => New_Internal_Name ('S'),
State_Decl => Empty,
Is_Null => True);
(Nam => New_Internal_Name ('S'),
Decl => Empty,
Loc => Sloc (State),
Is_Null => True);
Null_Seen := True;
-- Catch a case where a null state appears in a list of
......@@ -10321,8 +10324,10 @@ package body Sem_Prag is
elsif Nkind (State) = N_Identifier then
Create_Abstract_State
(State_Nam => Chars (State),
State_Decl => State);
(Nam => Chars (State),
Decl => State,
Loc => Sloc (State),
Is_Null => False);
Non_Null_Seen := True;
-- State declaration with various options. This construct
......@@ -10331,8 +10336,10 @@ package body Sem_Prag is
elsif Nkind (State) = N_Extension_Aggregate then
if Nkind (Ancestor_Part (State)) = N_Identifier then
Create_Abstract_State
(State_Nam => Chars (Ancestor_Part (State)),
State_Decl => Ancestor_Part (State));
(Nam => Chars (Ancestor_Part (State)),
Decl => Ancestor_Part (State),
Loc => Sloc (Ancestor_Part (State)),
Is_Null => False);
Non_Null_Seen := True;
else
Error_Msg_N
......
......@@ -552,6 +552,10 @@ package Sinfo is
-- In addition pragma Debug statements are removed from the tree (rewritten
-- to NULL stmt), since they should be taken into account in flow analysis.
-- An error is also issued for missing subunits, similar to the warning
-- issued when generating code, to avoid formal verification of a partial
-- unit.
-----------------------
-- Check Flag Fields --
-----------------------
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment