Skip to content

R
riscv-gcc-1
Commit 7ffbef99 by Arnaud Charlet Committed by Arnaud Charlet
Options

spark_xrefs.ads (Scope_Num): type refined to positive integers. 

2016-06-22  Arnaud Charlet  <charlet@adacore.com>

	* spark_xrefs.ads (Scope_Num): type refined to positive integers.
	* lib-xref-spark_specific.adb (Detect_And_Add_SPARK_Scope):
	moved into scope of Collect_SPARK_Xrefs.
	(Add_SPARK_Scope): moved into scope of Collect_SPARK_Xrefs;
	now uses Dspec and Scope_Id from Collect_SPARK_Xrefs.
	(Collect_SPARK_Xrefs): refactored to avoid retraversing the list
	of scopes.
	(Traverse_Compilation_Unit): refactored as a generic procedure.
	* types.ads (Unit_Number_Type): range refined.

From-SVN: r237690
parent 71b23599
Showing with 377 additions and 415 deletions
gcc/ada/ChangeLog
2016-06-22 Arnaud Charlet <charlet@adacore.com>
* spark_xrefs.ads (Scope_Num): type refined to positive integers.
* lib-xref-spark_specific.adb (Detect_And_Add_SPARK_Scope):
moved into scope of Collect_SPARK_Xrefs.
(Add_SPARK_Scope): moved into scope of Collect_SPARK_Xrefs;
now uses Dspec and Scope_Id from Collect_SPARK_Xrefs.
(Collect_SPARK_Xrefs): refactored to avoid retraversing the list
of scopes.
(Traverse_Compilation_Unit): refactored as a generic procedure.
* types.ads (Unit_Number_Type): range refined.
2016-06-22 Hristian Kirtchev <kirtchev@adacore.com>
* lib-xref-spark_specific.adb, a-cuprqu.ads, sem_ch6.adb: Minor
......
gcc/ada/lib-xref-spark_specific.adb
......@@ -85,160 +85,68 @@ package body SPARK_Specific is
-- Local Subprograms --
-----------------------
procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat);
procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat);
-- Add file and corresponding scopes for unit to the tables
-- SPARK_File_Table and SPARK_Scope_Table. When two units are present for
-- the same compilation unit, as it happens for library-level
-- instantiations of generics, then Ubody /= Uspec, and all scopes are
-- added to the same SPARK file. Otherwise Ubody = Uspec.
procedure Add_SPARK_Scope (N : Node_Id);
-- Add scope N to the table SPARK_Scope_Table
-- SPARK_File_Table and SPARK_Scope_Table. When two units are present
-- for the same compilation unit, as it happens for library-level
-- instantiations of generics, then Ubody is the number of the body
-- unit; otherwise it is No_Unit.
procedure Add_SPARK_Xrefs;
-- Filter table Xrefs to add all references used in SPARK to the table
-- SPARK_Xref_Table.
procedure Detect_And_Add_SPARK_Scope (N : Node_Id);
-- Call Add_SPARK_Scope on scopes
function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
-- Hash function for hash table
procedure Traverse_Declaration_Or_Statement
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean);
procedure Traverse_Declarations_Or_Statements
(L : List_Id;
Process : Node_Processing;
Inside_Stubs : Boolean);
procedure Traverse_Handled_Statement_Sequence
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean);
procedure Traverse_Protected_Body
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean);
procedure Traverse_Package_Body
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean);
procedure Traverse_Subprogram_Body
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean);
-- Traverse corresponding construct, calling Process on all declarations
generic
with procedure Process (N : Node_Id) is <>;
procedure Traverse_Compilation_Unit (CU : Node_Id; Inside_Stubs : Boolean);
-- Call Process on all declarations in compilation unit CU. If
-- Inside_Stubs is True, then the body of stubs is also traversed.
-- Generic declarations are ignored.
--------------------
-- Add_SPARK_File --
--------------------
procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat) is
procedure Add_SPARK_File (Uspec, Ubody : Unit_Number_Type; Dspec : Nat) is
File : constant Source_File_Index := Source_Index (Uspec);
From : Scope_Index;
From : constant Scope_Index := SPARK_Scope_Table.Last + 1;
File_Name : String_Ptr;
Unit_File_Name : String_Ptr;
begin
-- Source file could be inexistant as a result of an error, if option
-- gnatQ is used.
Scope_Id : Pos := 1;
if File = No_Source_File then
return;
end if;
procedure Add_SPARK_Scope (N : Node_Id);
-- Add scope N to the table SPARK_Scope_Table
-- Subunits are traversed as part of the top-level unit to which they
-- belong.
if Nkind (Unit (Cunit (Ubody))) = N_Subunit then
return;
end if;
procedure Detect_And_Add_SPARK_Scope (N : Node_Id);
-- Call Add_SPARK_Scope on scopes
From := SPARK_Scope_Table.Last + 1;
Traverse_Compilation_Unit
(CU => Cunit (Ubody),
Process => Detect_And_Add_SPARK_Scope'Access,
Inside_Stubs => True);
---------------------
-- Add_SPARK_Scope --
---------------------
-- When two units are present for the same compilation unit, as it
-- happens for library-level instantiations of generics, then add all
-- scopes to the same SPARK file.
procedure Add_SPARK_Scope (N : Node_Id) is
E : constant Entity_Id := Defining_Entity (N);
Loc : constant Source_Ptr := Sloc (E);
if Ubody /= Uspec then
Traverse_Compilation_Unit
(CU => Cunit (Uspec),
Process => Detect_And_Add_SPARK_Scope'Access,
Inside_Stubs => True);
end if;
-- The character describing the kind of scope is chosen to be the
-- same as the one describing the corresponding entity in cross
-- references, see Xref_Entity_Letters in lib-xrefs.ads
-- Update scope numbers
Typ : Character;
declare
Scope_Id : Pos;
begin
Scope_Id := 1;
for Index in From .. SPARK_Scope_Table.Last loop
declare
S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index);
begin
S.Scope_Num := Scope_Id;
S.File_Num := Dspec;
Scope_Id := Scope_Id + 1;
end;
end loop;
end;
-- Make entry for new file in file table
Get_Name_String (Reference_Name (File));
File_Name := new String'(Name_Buffer (1 .. Name_Len));
-- For subunits, also retrieve the file name of the unit. Only do so if
-- unit has an associated compilation unit.
-- Ignore scopes without a proper location
if Present (Cunit (Unit (File)))
and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
then
Get_Name_String (Reference_Name (Main_Source_File));
Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len));
else
Unit_File_Name := null;
end if;
SPARK_File_Table.Append (
(File_Name => File_Name,
Unit_File_Name => Unit_File_Name,
File_Num => Dspec,
From_Scope => From,
To_Scope => SPARK_Scope_Table.Last));
end Add_SPARK_File;
---------------------
-- Add_SPARK_Scope --
---------------------
procedure Add_SPARK_Scope (N : Node_Id) is
E : constant Entity_Id := Defining_Entity (N);
Loc : constant Source_Ptr := Sloc (E);
-- The character describing the kind of scope is chosen to be the same
-- as the one describing the corresponding entity in cross references,
-- see Xref_Entity_Letters in lib-xrefs.ads
Typ : Character;
begin
-- Ignore scopes without a proper location
if Sloc (N) = No_Location then
return;
end if;
if Sloc (N) = No_Location then
return;
end if;
case Ekind (E) is
case Ekind (E) is
when E_Entry
| E_Entry_Family
| E_Generic_Function
......@@ -247,16 +155,16 @@ package body SPARK_Specific is
| E_Package
| E_Protected_Type
| E_Task_Type
=>
=>
Typ := Xref_Entity_Letters (Ekind (E));
when E_Function
| E_Procedure
=>
=>
-- In SPARK we need to distinguish protected functions and
-- procedures from ordinary subprograms, but there are no special
-- Xref letters for them. Since this distiction is only needed
-- to detect protected calls, we pretend that such calls are entry
-- Xref letters for them. Since this distiction is only needed to
-- detect protected calls, we pretend that such calls are entry
-- calls.
if Ekind (Scope (E)) = E_Protected_Type then
......@@ -269,7 +177,7 @@ package body SPARK_Specific is
| E_Protected_Body
| E_Subprogram_Body
| E_Task_Body
=>
=>
Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
when E_Void =>
......@@ -282,24 +190,111 @@ package body SPARK_Specific is
when others =>
raise Program_Error;
end case;
-- File_Num and Scope_Num are filled later. From_Xref and To_Xref are
-- filled even later, but are initialized to represent an empty range.
SPARK_Scope_Table.Append (
(Scope_Name => new String'(Unique_Name (E)),
File_Num => 0,
Scope_Num => 0,
Spec_File_Num => 0,
Spec_Scope_Num => 0,
Line => Nat (Get_Logical_Line_Number (Loc)),
Stype => Typ,
Col => Nat (Get_Column_Number (Loc)),
From_Xref => 1,
To_Xref => 0,
Scope_Entity => E));
end Add_SPARK_Scope;
end case;
-- File_Num and Scope_Num are filled later. From_Xref and To_Xref
-- are filled even later, but are initialized to represent an empty
-- range.
SPARK_Scope_Table.Append
((Scope_Name => new String'(Unique_Name (E)),
File_Num => Dspec,
Scope_Num => Scope_Id,
Spec_File_Num => 0,
Spec_Scope_Num => 0,
Line => Nat (Get_Logical_Line_Number (Loc)),
Stype => Typ,
Col => Nat (Get_Column_Number (Loc)),
From_Xref => 1,
To_Xref => 0,
Scope_Entity => E));
Scope_Id := Scope_Id + 1;
end Add_SPARK_Scope;
--------------------------------
-- Detect_And_Add_SPARK_Scope --
--------------------------------
procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
begin
if Nkind_In (N, N_Entry_Body, -- entries
N_Entry_Declaration)
or else
Nkind_In (N, N_Package_Body, -- packages
N_Package_Body_Stub,
N_Package_Declaration)
or else
Nkind_In (N, N_Protected_Body, -- protected objects
N_Protected_Body_Stub,
N_Protected_Type_Declaration)
or else
Nkind_In (N, N_Subprogram_Body, -- subprograms
N_Subprogram_Body_Stub,
N_Subprogram_Declaration)
or else
Nkind_In (N, N_Task_Body, -- tasks
N_Task_Body_Stub,
N_Task_Type_Declaration)
then
Add_SPARK_Scope (N);
end if;
end Detect_And_Add_SPARK_Scope;
procedure Traverse_Scopes is new
Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
-- Start of processing for Add_SPARK_File
begin
-- Source file could be inexistant as a result of an error, if option
-- gnatQ is used.
if File = No_Source_File then
return;
end if;
-- Subunits are traversed as part of the top-level unit to which they
-- belong.
if Nkind (Unit (Cunit (Uspec))) = N_Subunit then
return;
end if;
Traverse_Scopes (CU => Cunit (Uspec), Inside_Stubs => True);
-- When two units are present for the same compilation unit, as it
-- happens for library-level instantiations of generics, then add all
-- scopes to the same SPARK file.
if Ubody /= No_Unit then
Traverse_Scopes (CU => Cunit (Ubody), Inside_Stubs => True);
end if;
-- Make entry for new file in file table
Get_Name_String (Reference_Name (File));
File_Name := new String'(Name_Buffer (1 .. Name_Len));
-- For subunits, also retrieve the file name of the unit. Only do so if
-- unit has an associated compilation unit.
if Present (Cunit (Unit (File)))
and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
then
Get_Name_String (Reference_Name (Main_Source_File));
Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len));
else
Unit_File_Name := null;
end if;
SPARK_File_Table.Append (
(File_Name => File_Name,
Unit_File_Name => Unit_File_Name,
File_Num => Dspec,
From_Scope => From,
To_Scope => SPARK_Scope_Table.Last));
end Add_SPARK_File;
---------------------
-- Add_SPARK_Xrefs --
......@@ -905,8 +900,17 @@ package body SPARK_Specific is
(Sdep_Table : Unit_Ref_Table;
Num_Sdep : Nat)
is
D1 : Pos;
D2 : Pos;
Sdep, Sdep_Next : Pos;
-- Index of the current and next source dependency
Sdep_File : Pos;
-- Index of the file to which the scopes need to be assigned; for
-- library-level instances of generic units this points to the unit
-- of the body, because this is where references are assigned to.
Uspec, Ubody : Unit_Number_Type;
-- Unit numbers for the dependency spec and possibly its body (only in
-- the case of library-level instance of a generic package).
begin
-- Cross-references should have been computed first
......@@ -917,70 +921,82 @@ package body SPARK_Specific is
-- Generate file and scope SPARK cross-reference information
D1 := 1;
while D1 <= Num_Sdep loop
Sdep := 1;
while Sdep <= Num_Sdep loop
-- In rare cases, when treating the library-level instantiation of a
-- generic, two consecutive units refer to the same compilation unit
-- node and entity. In that case, treat them as a single unit for the
-- sake of SPARK cross references by passing to Add_SPARK_File.
-- For library-level instantiation of a generic, two consecutive
-- units refer to the same compilation unit node and entity (one to
-- body, one to spec). In that case, treat them as a single unit for
-- the sake of SPARK cross references by passing to Add_SPARK_File.
if D1 < Num_Sdep
and then Cunit_Entity (Sdep_Table (D1)) =
Cunit_Entity (Sdep_Table (D1 + 1))
if Sdep < Num_Sdep
and then Cunit_Entity (Sdep_Table (Sdep)) =
Cunit_Entity (Sdep_Table (Sdep + 1))
then
declare
Cunit1 : Node_Id renames Cunit (Sdep_Table (D1));
Cunit2 : Node_Id renames Cunit (Sdep_Table (D1 + 1));
Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
begin
-- Both Cunit point to compilation unit nodes
pragma Assert
(Nkind (Cunit1) = N_Compilation_Unit
and then Nkind (Cunit2) = N_Compilation_Unit);
pragma Assert (Nkind (Cunit1) = N_Compilation_Unit
and then
Nkind (Cunit2) = N_Compilation_Unit);
-- Do not depend on the sorting order, which is based on
-- Unit_Name and for library-level instances of nested
-- generic-packages they are equal.
-- If declaration comes before the body then just set D2
-- If declaration comes before the body
if Nkind (Unit (Cunit1)) = N_Package_Declaration
and then Nkind (Unit (Cunit2)) = N_Package_Body
and then
Nkind (Unit (Cunit2)) = N_Package_Body
then
D2 := D1 + 1;
Uspec := Sdep_Table (Sdep);
Ubody := Sdep_Table (Sdep + 1);
Sdep_File := Sdep + 1;
-- If body comes before declaration then set D2 and adjust D1
-- If body comes before declaration
elsif Nkind (Unit (Cunit1)) = N_Package_Body
and then Nkind (Unit (Cunit2)) = N_Package_Declaration
and then
Nkind (Unit (Cunit2)) = N_Package_Declaration
then
D2 := D1;
D1 := D1 + 1;
Uspec := Sdep_Table (Sdep + 1);
Ubody := Sdep_Table (Sdep);
Sdep_File := Sdep;
-- Otherwise it is an error
else
raise Program_Error;
end if;
Sdep_Next := Sdep + 2;
end;
else
D2 := D1;
Uspec := Sdep_Table (Sdep);
Ubody := No_Unit;
Sdep_File := Sdep;
Sdep_Next := Sdep + 1;
end if;
-- Skip dependencies with no entity node, e.g. configuration files
-- with pragmas (.adc) or target description (.atp), since they
-- present no interest for SPARK cross references.
if Present (Cunit_Entity (Sdep_Table (D1))) then
if Present (Cunit_Entity (Uspec)) then
Add_SPARK_File
(Ubody => Sdep_Table (D1),
Uspec => Sdep_Table (D2),
Dspec => D2);
(Uspec => Uspec,
Ubody => Ubody,
Dspec => Sdep_File);
end if;
-- ??? this needs a comment
D1 := Pos'Max (D1, D2) + 1;
Sdep := Sdep_Next;
end loop;
-- Fill in the spec information when relevant
......@@ -1037,35 +1053,6 @@ package body SPARK_Specific is
Add_SPARK_Xrefs;
end Collect_SPARK_Xrefs;
--------------------------------
-- Detect_And_Add_SPARK_Scope --
--------------------------------
procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
begin
if Nkind_In (N, N_Entry_Body, -- entries
N_Entry_Declaration)
or else
Nkind_In (N, N_Package_Body, -- packages
N_Package_Body_Stub,
N_Package_Declaration)
or else
Nkind_In (N, N_Protected_Body, -- protected objects
N_Protected_Body_Stub,
N_Protected_Type_Declaration)
or else
Nkind_In (N, N_Subprogram_Body, -- subprograms
N_Subprogram_Body_Stub,
N_Subprogram_Declaration)
or else
Nkind_In (N, N_Task_Body, -- tasks
N_Task_Body_Stub,
N_Task_Type_Declaration)
then
Add_SPARK_Scope (N);
end if;
end Detect_And_Add_SPARK_Scope;
-------------------------------------
-- Enclosing_Subprogram_Or_Package --
-------------------------------------
......@@ -1245,65 +1232,44 @@ package body SPARK_Specific is
procedure Traverse_Compilation_Unit
(CU : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean)
is
Lu : Node_Id;
begin
-- Get Unit (checking case of subunit)
Lu := Unit (CU);
if Nkind (Lu) = N_Subunit then
Lu := Proper_Body (Lu);
end if;
-- Do not add scopes for generic units
procedure Traverse_Block (N : Node_Id);
procedure Traverse_Declarations_And_HSS (N : Node_Id);
procedure Traverse_Declaration_Or_Statement (N : Node_Id);
procedure Traverse_Declarations_Or_Statements (L : List_Id);
procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
procedure Traverse_Package_Body (N : Node_Id);
procedure Traverse_Visible_And_Private_Parts (N : Node_Id);
procedure Traverse_Protected_Body (N : Node_Id);
procedure Traverse_Subprogram_Body (N : Node_Id);
procedure Traverse_Task_Body (N : Node_Id);
if Nkind (Lu) = N_Package_Body
and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
then
return;
end if;
-- Call Process on all declarations
if Nkind (Lu) in N_Declaration
or else Nkind (Lu) in N_Later_Decl_Item
then
Process (Lu);
end if;
-- Traverse corresponding construct, calling Process on all declarations
-- Traverse the unit
--------------------
-- Traverse_Block --
--------------------
Traverse_Declaration_Or_Statement (Lu, Process, Inside_Stubs);
end Traverse_Compilation_Unit;
procedure Traverse_Block (N : Node_Id) renames
Traverse_Declarations_And_HSS;
---------------------------------------
-- Traverse_Declaration_Or_Statement --
---------------------------------------
---------------------------------------
-- Traverse_Declaration_Or_Statement --
---------------------------------------
procedure Traverse_Declaration_Or_Statement
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean)
is
begin
case Nkind (N) is
procedure Traverse_Declaration_Or_Statement (N : Node_Id)
is
begin
case Nkind (N) is
when N_Package_Declaration =>
declare
Spec : constant Node_Id := Specification (N);
begin
Traverse_Declarations_Or_Statements
(Visible_Declarations (Spec), Process, Inside_Stubs);
Traverse_Declarations_Or_Statements
(Private_Declarations (Spec), Process, Inside_Stubs);
end;
Traverse_Visible_And_Private_Parts (Specification (N));
when N_Package_Body =>
if Ekind (Defining_Entity (N)) /= E_Generic_Package then
Traverse_Package_Body (N, Process, Inside_Stubs);
Traverse_Package_Body (N);
end if;
when N_Package_Body_Stub =>
......@@ -1315,19 +1281,19 @@ package body SPARK_Specific is
and then
Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
then
Traverse_Package_Body (Body_N, Process, Inside_Stubs);
Traverse_Package_Body (Body_N);
end if;
end;
end if;
when N_Subprogram_Declaration =>
null;
when N_Entry_Body | N_Subprogram_Body =>
when N_Subprogram_Body =>
if not Is_Generic_Subprogram (Defining_Entity (N)) then
Traverse_Subprogram_Body (N, Process, Inside_Stubs);
Traverse_Subprogram_Body (N);
end if;
when N_Entry_Body =>
Traverse_Subprogram_Body (N);
when N_Subprogram_Body_Stub =>
if Present (Library_Unit (N)) then
declare
......@@ -1337,75 +1303,45 @@ package body SPARK_Specific is
and then
not Is_Generic_Subprogram (Defining_Entity (Body_N))
then
Traverse_Subprogram_Body (Body_N, Process, Inside_Stubs);
Traverse_Subprogram_Body (Body_N);
end if;
end;
end if;
when N_Protected_Body =>
Traverse_Protected_Body (N, Process, Inside_Stubs);
Traverse_Protected_Body (N);
when N_Protected_Body_Stub =>
if Present (Library_Unit (N)) then
declare
Body_N : constant Node_Id := Get_Body_From_Stub (N);
begin
if Inside_Stubs then
Traverse_Declarations_Or_Statements
(Declarations (Body_N), Process, Inside_Stubs);
end if;
end;
if Inside_Stubs then
Traverse_Protected_Body (Get_Body_From_Stub (N));
end if;
end if;
when N_Protected_Type_Declaration | N_Single_Protected_Declaration =>
declare
Def : constant Node_Id := Protected_Definition (N);
begin
Traverse_Declarations_Or_Statements
(Visible_Declarations (Def), Process, Inside_Stubs);
Traverse_Declarations_Or_Statements
(Private_Declarations (Def), Process, Inside_Stubs);
end;
Traverse_Visible_And_Private_Parts (Protected_Definition (N));
when N_Task_Definition =>
Traverse_Declarations_Or_Statements
(Visible_Declarations (N), Process, Inside_Stubs);
Traverse_Declarations_Or_Statements
(Private_Declarations (N), Process, Inside_Stubs);
Traverse_Visible_And_Private_Parts (N);
when N_Task_Body =>
Traverse_Declarations_Or_Statements
(Declarations (N), Process, Inside_Stubs);
Traverse_Handled_Statement_Sequence
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
Traverse_Task_Body (N);
when N_Task_Body_Stub =>
if Present (Library_Unit (N)) then
declare
Body_N : constant Node_Id := Get_Body_From_Stub (N);
begin
if Inside_Stubs then
Traverse_Declarations_Or_Statements
(Declarations (Body_N), Process, Inside_Stubs);
Traverse_Handled_Statement_Sequence
(Handled_Statement_Sequence (Body_N), Process,
Inside_Stubs);
end if;
end;
if Inside_Stubs then
Traverse_Task_Body (Get_Body_From_Stub (N));
end if;
end if;
when N_Block_Statement =>
Traverse_Declarations_Or_Statements
(Declarations (N), Process, Inside_Stubs);
Traverse_Handled_Statement_Sequence
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
Traverse_Block (N);
when N_If_Statement =>
-- Traverse the statements in the THEN part
Traverse_Declarations_Or_Statements
(Then_Statements (N), Process, Inside_Stubs);
Traverse_Declarations_Or_Statements (Then_Statements (N));
-- Loop through ELSIF parts if present
......@@ -1416,7 +1352,7 @@ package body SPARK_Specific is
begin
while Present (Elif) loop
Traverse_Declarations_Or_Statements
(Then_Statements (Elif), Process, Inside_Stubs);
(Then_Statements (Elif));
Next (Elif);
end loop;
end;
......@@ -1424,8 +1360,7 @@ package body SPARK_Specific is
-- Finally traverse the ELSE statements if present
Traverse_Declarations_Or_Statements
(Else_Statements (N), Process, Inside_Stubs);
Traverse_Declarations_Or_Statements (Else_Statements (N));
when N_Case_Statement =>
......@@ -1436,129 +1371,154 @@ package body SPARK_Specific is
begin
Alt := First (Alternatives (N));
while Present (Alt) loop
Traverse_Declarations_Or_Statements
(Statements (Alt), Process, Inside_Stubs);
Traverse_Declarations_Or_Statements (Statements (Alt));
Next (Alt);
end loop;
end;
when N_Extended_Return_Statement =>
Traverse_Handled_Statement_Sequence
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
(Handled_Statement_Sequence (N));
when N_Loop_Statement =>
Traverse_Declarations_Or_Statements
(Statements (N), Process, Inside_Stubs);
Traverse_Declarations_Or_Statements (Statements (N));
-- Generic declarations are ignored
-- Generic declarations are ignored
when others =>
null;
end case;
end Traverse_Declaration_Or_Statement;
end case;
end Traverse_Declaration_Or_Statement;
-----------------------------------------
-- Traverse_Declarations_Or_Statements --
-----------------------------------------
-----------------------------------
-- Traverse_Declarations_And_HSS --
-----------------------------------
procedure Traverse_Declarations_Or_Statements
(L : List_Id;
Process : Node_Processing;
Inside_Stubs : Boolean)
is
N : Node_Id;
procedure Traverse_Declarations_And_HSS (N : Node_Id)
is
begin
Traverse_Declarations_Or_Statements (Declarations (N));
Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
end Traverse_Declarations_And_HSS;
begin
-- Loop through statements or declarations
-----------------------------------------
-- Traverse_Declarations_Or_Statements --
-----------------------------------------
N := First (L);
while Present (N) loop
-- Call Process on all declarations
procedure Traverse_Declarations_Or_Statements (L : List_Id)
is
N : Node_Id;
if Nkind (N) in N_Declaration
begin
-- Loop through statements or declarations
N := First (L);
while Present (N) loop
-- Call Process on all declarations
if Nkind (N) in N_Declaration
or else
Nkind (N) in N_Later_Decl_Item
Nkind (N) in N_Later_Decl_Item
or else
Nkind (N) = N_Entry_Body
then
Process (N);
Nkind (N) = N_Entry_Body
then
Process (N);
end if;
Traverse_Declaration_Or_Statement (N);
Next (N);
end loop;
end Traverse_Declarations_Or_Statements;
-----------------------------------------
-- Traverse_Handled_Statement_Sequence --
-----------------------------------------
procedure Traverse_Handled_Statement_Sequence (N : Node_Id)
is
Handler : Node_Id;
begin
if Present (N) then
Traverse_Declarations_Or_Statements (Statements (N));
if Present (Exception_Handlers (N)) then
Handler := First (Exception_Handlers (N));
while Present (Handler) loop
Traverse_Declarations_Or_Statements (Statements (Handler));
Next (Handler);
end loop;
end if;
end if;
end Traverse_Handled_Statement_Sequence;
Traverse_Declaration_Or_Statement (N, Process, Inside_Stubs);
---------------------------
-- Traverse_Package_Body --
---------------------------
Next (N);
end loop;
end Traverse_Declarations_Or_Statements;
procedure Traverse_Package_Body (N : Node_Id) renames
Traverse_Declarations_And_HSS;
-----------------------------------------
-- Traverse_Handled_Statement_Sequence --
-----------------------------------------
-----------------------------
-- Traverse_Protected_Body --
-----------------------------
procedure Traverse_Handled_Statement_Sequence
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean)
is
Handler : Node_Id;
procedure Traverse_Protected_Body (N : Node_Id) is
begin
Traverse_Declarations_Or_Statements (Declarations (N));
end Traverse_Protected_Body;
------------------------------
-- Traverse_Subprogram_Body --
------------------------------
procedure Traverse_Subprogram_Body (N : Node_Id) renames
Traverse_Declarations_And_HSS;
------------------------
-- Traverse_Task_Body --
------------------------
procedure Traverse_Task_Body (N : Node_Id) renames
Traverse_Declarations_And_HSS;
procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
begin
Traverse_Declarations_Or_Statements (Visible_Declarations (N));
Traverse_Declarations_Or_Statements (Private_Declarations (N));
end Traverse_Visible_And_Private_Parts;
-- Start of processing for Traverse_Compilation_Unit
begin
if Present (N) then
Traverse_Declarations_Or_Statements
(Statements (N), Process, Inside_Stubs);
if Present (Exception_Handlers (N)) then
Handler := First (Exception_Handlers (N));
while Present (Handler) loop
Traverse_Declarations_Or_Statements
(Statements (Handler), Process, Inside_Stubs);
Next (Handler);
end loop;
end if;
-- Get Unit (checking case of subunit)
Lu := Unit (CU);
if Nkind (Lu) = N_Subunit then
Lu := Proper_Body (Lu);
end if;
end Traverse_Handled_Statement_Sequence;
---------------------------
-- Traverse_Package_Body --
---------------------------
-- Do not add scopes for generic units
procedure Traverse_Package_Body
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean) is
begin
Traverse_Declarations_Or_Statements
(Declarations (N), Process, Inside_Stubs);
Traverse_Handled_Statement_Sequence
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
end Traverse_Package_Body;
-----------------------------
-- Traverse_Protected_Body --
-----------------------------
procedure Traverse_Protected_Body
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean) is
begin
Traverse_Declarations_Or_Statements
(Declarations (N), Process, Inside_Stubs);
end Traverse_Protected_Body;
if Nkind (Lu) = N_Package_Body
and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
then
return;
end if;
------------------------------
-- Traverse_Subprogram_Body --
------------------------------
-- Call Process on all declarations
procedure Traverse_Subprogram_Body
(N : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean)
is
begin
Traverse_Declarations_Or_Statements
(Declarations (N), Process, Inside_Stubs);
Traverse_Handled_Statement_Sequence
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
end Traverse_Subprogram_Body;
if Nkind (Lu) in N_Declaration
or else Nkind (Lu) in N_Later_Decl_Item
then
Process (Lu);
end if;
-- Traverse the unit
Traverse_Declaration_Or_Statement (Lu);
end Traverse_Compilation_Unit;
end SPARK_Specific;
gcc/ada/lib-xref.ads
......@@ -639,16 +639,6 @@ package Lib.Xref is
-- This procedure is called to record a dereference. N is the location
-- of the dereference.
type Node_Processing is access procedure (N : Node_Id);
procedure Traverse_Compilation_Unit
(CU : Node_Id;
Process : Node_Processing;
Inside_Stubs : Boolean);
-- Call Process on all declarations in compilation unit CU. If
-- Inside_Stubs is True, then the body of stubs is also traversed.
-- Generic declarations are ignored.
procedure Collect_SPARK_Xrefs
(Sdep_Table : Unit_Ref_Table;
Num_Sdep : Nat);
......
gcc/ada/spark_xrefs.ads
......@@ -285,7 +285,7 @@ package SPARK_Xrefs is
File_Num : Nat;
-- Set to the file dependency number for the scope
Scope_Num : Nat;
Scope_Num : Pos;
-- Set to the scope number for the scope
Spec_File_Num : Nat;
......
gcc/ada/types.ads
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -554,7 +554,7 @@ package Types is
-- Types used for Library Management --
---------------------------------------
type Unit_Number_Type is new Int;
type Unit_Number_Type is new Int range -1 .. Int'Last;
-- Unit number. The main source is unit 0, and subsidiary sources have
-- non-zero numbers starting with 1. Unit numbers are used to index the
-- Units table in package Lib.
......
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