2011-08-31 Jose Ruiz <ruiz@adacore.com>
* s-taprop-linux.adb (Set_Task_Affinity): Avoid the use of anonymous
access types.
* affinity.c (__gnat_set_affinity_mask): Declare index variable.
2011-08-31 Yannick Moy <moy@adacore.com>
* sem_ch8.adb (Analyze_Subprogram_Renaming): Refine expander test in
full-expander test.
Minor reformatting, renaming ALFA in Alfa (we dropped acronym)
* einfo.adb (Primitive_Operations): Correctly return list of primitive
operations in a case where it returned previously No_Elist.
From-SVN: r178358
39 files changed:
+2011-08-31 Jose Ruiz <ruiz@adacore.com>
+
+ * s-taprop-linux.adb (Set_Task_Affinity): Avoid the use of anonymous
+ access types.
+ * affinity.c (__gnat_set_affinity_mask): Declare index variable.
+
+2011-08-31 Yannick Moy <moy@adacore.com>
+
+ * sem_ch8.adb (Analyze_Subprogram_Renaming): Refine expander test in
+ full-expander test.
+ Minor reformatting, renaming ALFA in Alfa (we dropped acronym)
+ * einfo.adb (Primitive_Operations): Correctly return list of primitive
+ operations in a case where it returned previously No_Elist.
+
2011-08-31 Robert Dewar <dewar@adacore.com>
* s-taprop-vxworks.adb, sem_ch5.adb, s-taprop-tru64.adb, exp_alfa.adb,
2011-08-31 Robert Dewar <dewar@adacore.com>
* s-taprop-vxworks.adb, sem_ch5.adb, s-taprop-tru64.adb, exp_alfa.adb,
int
__gnat_set_affinity_mask (int tid, unsigned mask)
{
int
__gnat_set_affinity_mask (int tid, unsigned mask)
{
cpuset_t cpuset;
CPUSET_ZERO(cpuset);
cpuset_t cpuset;
CPUSET_ZERO(cpuset);
------------------------------------------------------------------------------
with Output; use Output;
------------------------------------------------------------------------------
with Output; use Output;
- -- Dump ALFA file table
+ -- Dump Alfa file table
- Write_Line ("ALFA File Table");
+ Write_Line ("Alfa File Table");
Write_Line ("---------------");
Write_Line ("---------------");
- for Index in 1 .. ALFA_File_Table.Last loop
+ for Index in 1 .. Alfa_File_Table.Last loop
- AFR : ALFA_File_Record renames ALFA_File_Table.Table (Index);
+ AFR : Alfa_File_Record renames Alfa_File_Table.Table (Index);
- -- Dump ALFA scope table
+ -- Dump Alfa scope table
- Write_Line ("ALFA Scope Table");
+ Write_Line ("Alfa Scope Table");
Write_Line ("----------------");
Write_Line ("----------------");
- for Index in 1 .. ALFA_Scope_Table.Last loop
+ for Index in 1 .. Alfa_Scope_Table.Last loop
- ASR : ALFA_Scope_Record renames ALFA_Scope_Table.Table (Index);
+ ASR : Alfa_Scope_Record renames Alfa_Scope_Table.Table (Index);
- -- Dump ALFA cross-reference table
+ -- Dump Alfa cross-reference table
- Write_Line ("ALFA Xref Table");
+ Write_Line ("Alfa Xref Table");
Write_Line ("---------------");
Write_Line ("---------------");
- for Index in 1 .. ALFA_Xref_Table.Last loop
+ for Index in 1 .. Alfa_Xref_Table.Last loop
- AXR : ALFA_Xref_Record renames ALFA_Xref_Table.Table (Index);
+ AXR : Alfa_Xref_Record renames Alfa_Xref_Table.Table (Index);
-- Initialize --
----------------
-- Initialize --
----------------
- procedure Initialize_ALFA_Tables is
+ procedure Initialize_Alfa_Tables is
- ALFA_File_Table.Init;
- ALFA_Scope_Table.Init;
- ALFA_Xref_Table.Init;
- end Initialize_ALFA_Tables;
+ Alfa_File_Table.Init;
+ Alfa_Scope_Table.Init;
+ Alfa_Xref_Table.Init;
+ end Initialize_Alfa_Tables;
Write_Int (N);
end Write_Info_Nat;
Write_Int (N);
end Write_Info_Nat;
- procedure Debug_Put_ALFA is new Put_ALFA;
+ procedure Debug_Put_Alfa is new Put_Alfa;
-- Start of processing for palfa
begin
-- Start of processing for palfa
begin
-- --
------------------------------------------------------------------------------
-- --
------------------------------------------------------------------------------
--- This package defines tables used to store information needed for the ALFA
--- mode. It is used by procedures in Lib.Xref.ALFA to build the ALFA
--- information before writing it out to the ALI file, and by Get_ALFA/Put_ALFA
+-- This package defines tables used to store information needed for the Alfa
+-- mode. It is used by procedures in Lib.Xref.Alfa to build the Alfa
+-- information before writing it out to the ALI file, and by Get_Alfa/Put_Alfa
-- to read and write the text form that is used in the ALI file.
with Types; use Types;
with GNAT.Table;
-- to read and write the text form that is used in the ALI file.
with Types; use Types;
with GNAT.Table;
- -- ALFA information can exist in one of two forms. In the ALI file, it is
+ -- Alfa information can exist in one of two forms. In the ALI file, it is
-- represented using a text format that is described in this specification.
-- represented using a text format that is described in this specification.
- -- Internally it is stored using three tables ALFA_Xref_Table,
- -- ALFA_Scope_Table and ALFA_File_Table, which are also defined in this
+ -- Internally it is stored using three tables Alfa_Xref_Table,
+ -- Alfa_Scope_Table and Alfa_File_Table, which are also defined in this
- -- Lib.Xref.ALFA is part of the compiler. It extracts ALFA information from
+ -- Lib.Xref.Alfa is part of the compiler. It extracts Alfa information from
-- the complete set of cross-references generated during compilation.
-- the complete set of cross-references generated during compilation.
- -- Get_ALFA reads the text lines in ALI format and populates the internal
+ -- Get_Alfa reads the text lines in ALI format and populates the internal
-- tables with corresponding information.
-- tables with corresponding information.
- -- Put_ALFA reads the internal tables and generates text lines in the ALI
+ -- Put_Alfa reads the internal tables and generates text lines in the ALI
-- format.
---------------------
-- format.
---------------------
- -- ALFA information is generated on a unit-by-unit basis in the ALI file,
+ -- Alfa information is generated on a unit-by-unit basis in the ALI file,
-- using lines that start with the identifying character F ("Formal").
-- These lines are generated if one of the -gnatd.E (SPARK generation mode)
-- or gnatd.F (Why generation mode) switches is set.
-- using lines that start with the identifying character F ("Formal").
-- These lines are generated if one of the -gnatd.E (SPARK generation mode)
-- or gnatd.F (Why generation mode) switches is set.
- -- The ALFA information follows the cross-reference information, so it
+ -- The Alfa information follows the cross-reference information, so it
-- needs not be read by tools like gnatbind, gnatmake etc.
-- -------------------
-- needs not be read by tools like gnatbind, gnatmake etc.
-- -------------------
-- Note: the filename is redundant in that it could be deduced from the
-- corresponding D line, but it is convenient at least for human
-- Note: the filename is redundant in that it could be deduced from the
-- corresponding D line, but it is convenient at least for human
- -- reading of the ALFA information, and means that the ALFA information
+ -- reading of the Alfa information, and means that the Alfa information
-- can stand on its own without needing other parts of the ALI file.
-- FS . scope line type col entity (-> spec-file . spec-scope)?
-- can stand on its own without needing other parts of the ALI file.
-- FS . scope line type col entity (-> spec-file . spec-scope)?
-- Xref Table --
----------------
-- Xref Table --
----------------
- -- The following table records ALFA cross-references
+ -- The following table records Alfa cross-references
type Xref_Index is new Int;
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
type Xref_Index is new Int;
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
- type ALFA_Xref_Record is record
+ type Alfa_Xref_Record is record
Entity_Name : String_Ptr;
-- Pointer to entity name in ALI file
Entity_Name : String_Ptr;
-- Pointer to entity name in ALI file
-- Column number for the reference
end record;
-- Column number for the reference
end record;
- package ALFA_Xref_Table is new GNAT.Table (
- Table_Component_Type => ALFA_Xref_Record,
+ package Alfa_Xref_Table is new GNAT.Table (
+ Table_Component_Type => Alfa_Xref_Record,
Table_Index_Type => Xref_Index,
Table_Low_Bound => 1,
Table_Initial => 2000,
Table_Index_Type => Xref_Index,
Table_Low_Bound => 1,
Table_Initial => 2000,
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
- type ALFA_Scope_Record is record
+ type Alfa_Scope_Record is record
Scope_Name : String_Ptr;
-- Pointer to scope name in ALI file
Scope_Name : String_Ptr;
-- Pointer to scope name in ALI file
-- Entity (subprogram or package) for the scope
end record;
-- Entity (subprogram or package) for the scope
end record;
- package ALFA_Scope_Table is new GNAT.Table (
- Table_Component_Type => ALFA_Scope_Record,
+ package Alfa_Scope_Table is new GNAT.Table (
+ Table_Component_Type => Alfa_Scope_Record,
Table_Index_Type => Scope_Index,
Table_Low_Bound => 1,
Table_Initial => 200,
Table_Index_Type => Scope_Index,
Table_Low_Bound => 1,
Table_Initial => 200,
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
-- Used to index values in this table. Values start at 1 and are assigned
-- sequentially as entries are constructed.
- type ALFA_File_Record is record
+ type Alfa_File_Record is record
File_Name : String_Ptr;
-- Pointer to file name in ALI file
File_Name : String_Ptr;
-- Pointer to file name in ALI file
-- Ending index in Scope table for this unit
end record;
-- Ending index in Scope table for this unit
end record;
- package ALFA_File_Table is new GNAT.Table (
- Table_Component_Type => ALFA_File_Record,
+ package Alfa_File_Table is new GNAT.Table (
+ Table_Component_Type => Alfa_File_Record,
Table_Index_Type => File_Index,
Table_Low_Bound => 1,
Table_Initial => 20,
Table_Index_Type => File_Index,
Table_Low_Bound => 1,
Table_Initial => 20,
-- Subprograms --
-----------------
-- Subprograms --
-----------------
- procedure Initialize_ALFA_Tables;
+ procedure Initialize_Alfa_Tables;
-- Reset tables for a new compilation
procedure dalfa;
-- Reset tables for a new compilation
procedure dalfa;
- -- Debug routine to dump internal ALFA tables. This is a raw format dump
+ -- Debug routine to dump internal Alfa tables. This is a raw format dump
-- showing exactly what the tables contain.
procedure palfa;
-- showing exactly what the tables contain.
procedure palfa;
- -- Debugging procedure to output contents of ALFA binary tables in the
+ -- Debugging procedure to output contents of Alfa binary tables in the
-- format in which they appear in an ALI file.
-- format in which they appear in an ALI file.
-- --
------------------------------------------------------------------------------
-- --
------------------------------------------------------------------------------
--- This utility program is used to test proper operation of the Get_ALFA and
--- Put_ALFA units. To run it, compile any source file with switch -gnatd.E or
--- -gnatd.F to get an ALI file file.ALI containing ALFA information. Then run
+-- This utility program is used to test proper operation of the Get_Alfa and
+-- Put_Alfa units. To run it, compile any source file with switch -gnatd.E or
+-- -gnatd.F to get an ALI file file.ALI containing Alfa information. Then run
--- This test will read the ALFA information from the ALI file, and use
--- Get_ALFA to store this in binary form in the internal tables in ALFA. Then
--- Put_ALFA is used to write the information from these tables back into text
--- form. This output is compared with the original ALFA information in the ALI
+-- This test will read the Alfa information from the ALI file, and use
+-- Get_Alfa to store this in binary form in the internal tables in Alfa. Then
+-- Put_Alfa is used to write the information from these tables back into text
+-- form. This output is compared with the original Alfa information in the ALI
-- file and the two should be identical. If not an error message is output.
-- file and the two should be identical. If not an error message is output.
-with Get_ALFA;
-with Put_ALFA;
+with Get_Alfa;
+with Put_Alfa;
with Types; use Types;
with Ada.Command_Line; use Ada.Command_Line;
with Types; use Types;
with Ada.Command_Line; use Ada.Command_Line;
with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO;
with Ada.Text_IO;
with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO;
with Ada.Text_IO;
Infile : File_Type;
Outfile_1 : File_Type;
Outfile_2 : File_Type;
Infile : File_Type;
Outfile_1 : File_Type;
Outfile_2 : File_Type;
- -- Subprograms used by Get_ALFA (these also copy the output to Outfile_1
- -- for later comparison with the output generated by Put_ALFA).
+ -- Subprograms used by Get_Alfa (these also copy the output to Outfile_1
+ -- for later comparison with the output generated by Put_Alfa).
function Getc return Character;
function Nextc return Character;
function Getc return Character;
function Nextc return Character;
- -- Subprograms used by Put_ALFA, which write information to Outfile_2
+ -- Subprograms used by Put_Alfa, which write information to Outfile_2
function Write_Info_Col return Positive;
procedure Write_Info_Char (C : Character);
function Write_Info_Col return Positive;
procedure Write_Info_Char (C : Character);
Write_Info_Char (LF);
end Write_Info_Terminate;
Write_Info_Char (LF);
end Write_Info_Terminate;
- -- Local instantiations of Put_ALFA and Get_ALFA
+ -- Local instantiations of Put_Alfa and Get_Alfa
- procedure Get_ALFA_Info is new Get_ALFA;
- procedure Put_ALFA_Info is new Put_ALFA;
+ procedure Get_Alfa_Info is new Get_Alfa;
+ procedure Put_Alfa_Info is new Put_Alfa;
-- Start of processing for Process
-- Start of processing for Process
Set_Index (Infile, Index (Infile) - 1);
Set_Index (Infile, Index (Infile) - 1);
- -- Read ALFA information to internal ALFA tables, also copying ALFA info
+ -- Read Alfa information to internal Alfa tables, also copying Alfa info
- Initialize_ALFA_Tables;
- Get_ALFA_Info;
+ Initialize_Alfa_Tables;
+ Get_Alfa_Info;
- -- Write ALFA information from internal ALFA tables to Outfile_2
+ -- Write Alfa information from internal Alfa tables to Outfile_2
-- Junk blank line (see comment at end of Lib.Writ)
-- Junk blank line (see comment at end of Lib.Writ)
exception
when Stop =>
null;
exception
when Stop =>
null;
'S' => True, -- specific dispatching
'Y' => True, -- limited_with
'C' => True, -- SCO information
'S' => True, -- specific dispatching
'Y' => True, -- limited_with
'C' => True, -- SCO information
- 'F' => True, -- ALFA information
+ 'F' => True, -- Alfa information
others => False);
--------------------
others => False);
--------------------
-- Here after dealing with xref sections
-- Ignore remaining lines, which belong to an additional section of the
-- Here after dealing with xref sections
-- Ignore remaining lines, which belong to an additional section of the
- -- ALI file not considered here (like SCO or ALFA).
+ -- ALI file not considered here (like SCO or Alfa).
-- d.C Generate concatenation call, do not generate inline code
-- d.D
-- d.E
-- d.C Generate concatenation call, do not generate inline code
-- d.D
-- d.E
-- d.G Precondition only mode for gnat2why
-- d.H Standard package only mode for gnat2why
-- d.I SCIL generation mode
-- d.G Precondition only mode for gnat2why
-- d.H Standard package only mode for gnat2why
-- d.I SCIL generation mode
-- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases
-- where we would normally generate inline concatenation code.
-- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases
-- where we would normally generate inline concatenation code.
- -- d.F ALFA mode. Generate AST in a form suitable for formal verification,
+ -- d.F Alfa mode. Generate AST in a form suitable for formal verification,
-- as well as additional cross reference information in ALI files to
-- compute effects of subprograms.
-- as well as additional cross reference information in ALI files to
-- compute effects of subprograms.
if Is_Concurrent_Type (Id) then
if Present (Corresponding_Record_Type (Id)) then
return Direct_Primitive_Operations
if Is_Concurrent_Type (Id) then
if Present (Corresponding_Record_Type (Id)) then
return Direct_Primitive_Operations
- (Corresponding_Record_Type (Id));
+ (Corresponding_Record_Type (Id));
+
+ -- If expansion is disabled the corresponding record type is absent,
+ -- but if the type has ancestors it may have primitive operations.
+
+ elsif Is_Tagged_Type (Id) then
+ return Direct_Primitive_Operations (Id);
+
else
return No_Elist;
end if;
else
return No_Elist;
end if;
elsif Msg = "size for& too small, minimum allowed is ^" then
elsif Msg = "size for& too small, minimum allowed is ^" then
- -- Suppress "size too small" errors in CodePeer mode and ALFA mode,
+ -- Suppress "size too small" errors in CodePeer mode and Alfa mode,
-- since pragma Pack is also ignored in these configurations.
-- since pragma Pack is also ignored in these configurations.
- if CodePeer_Mode or ALFA_Mode then
+ if CodePeer_Mode or Alfa_Mode then
return True;
-- When a size is wrong for a frozen type there is no explicit size
return True;
-- When a size is wrong for a frozen type there is no explicit size
-- Note: a special exception is that RM is never treated as a keyword
-- but instead is copied literally into the message, this avoids the
-- need for writing 'R'M for all reference manual quotes. A similar
-- Note: a special exception is that RM is never treated as a keyword
-- but instead is copied literally into the message, this avoids the
-- need for writing 'R'M for all reference manual quotes. A similar
- -- exception is applied to the occurrence of the string ALFA used in
- -- error messages about the ALFA subset of Ada.
+ -- exception is applied to the occurrence of the string Alfa used in
+ -- error messages about the Alfa subset of Ada.
-- In the case of names, the default mode for the error text processor
-- is to surround the name by quotation marks automatically. The case
-- In the case of names, the default mode for the error text processor
-- is to surround the name by quotation marks automatically. The case
if Name_Len = 2 and then Name_Buffer (1 .. 2) = "RM" then
Set_Msg_Name_Buffer;
if Name_Len = 2 and then Name_Buffer (1 .. 2) = "RM" then
Set_Msg_Name_Buffer;
- -- We make a similar exception for ALFA
+ -- We make a similar exception for Alfa
- elsif Name_Len = 4 and then Name_Buffer (1 .. 4) = "ALFA" then
+ elsif Name_Len = 4 and then Name_Buffer (1 .. 4) = "Alfa" then
- -- Neither RM nor ALFA: case appropriately and add surrounding quotes
+ -- Neither RM nor Alfa: case appropriately and add surrounding quotes
else
Set_Casing (Keyword_Casing (Flag_Source), All_Lower_Case);
else
Set_Casing (Keyword_Casing (Flag_Source), All_Lower_Case);
-- CodePeer and GNATprove want to see the unexpanded N_Op_Expon node
-- CodePeer and GNATprove want to see the unexpanded N_Op_Expon node
- if CodePeer_Mode or ALFA_Mode then
+ if CodePeer_Mode or Alfa_Mode then
-- this node and enclosed expression are not expanded, so do not apply
-- any transformations here.
-- this node and enclosed expression are not expanded, so do not apply
-- any transformations here.
and then Nkind (Wrap_Node) = N_Pragma
and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
then
and then Nkind (Wrap_Node) = N_Pragma
and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
then
Debug_A_Entry ("expanding ", N);
begin
Debug_A_Entry ("expanding ", N);
begin
- -- In ALFA mode we only need a very limited subset of the usual
+ -- In Alfa mode we only need a very limited subset of the usual
-- expansions. This limited subset is implemented in Expand_Alfa.
-- expansions. This limited subset is implemented in Expand_Alfa.
- -- Here for normal non-ALFA mode
+ -- Here for normal non-Alfa mode
else
-- Processing depends on node kind. For full details on the
else
-- Processing depends on node kind. For full details on the
and then RM_Size (Rec) >= Scalar_Component_Total_RM_Size
and then RM_Size (Rec) >= Scalar_Component_Total_RM_Size
- -- Never do implicit packing in CodePeer or ALFA modes since
+ -- Never do implicit packing in CodePeer or Alfa modes since
-- we don't do any packing in these modes, since this generates
-- over-complex code that confuses static analysis, and in
-- general, neither CodePeer not GNATprove care about the
-- internal representation of objects.
-- we don't do any packing in these modes, since this generates
-- over-complex code that confuses static analysis, and in
-- general, neither CodePeer not GNATprove care about the
-- internal representation of objects.
- and then not (CodePeer_Mode or ALFA_Mode)
+ and then not (CodePeer_Mode or Alfa_Mode)
then
-- If implicit packing enabled, do it
then
-- If implicit packing enabled, do it
and then not Is_Limited_Composite (E)
and then not Is_Packed (Root_Type (E))
and then not Has_Component_Size_Clause (Root_Type (E))
and then not Is_Limited_Composite (E)
and then not Is_Packed (Root_Type (E))
and then not Has_Component_Size_Clause (Root_Type (E))
- and then not (CodePeer_Mode or ALFA_Mode)
+ and then not (CodePeer_Mode or Alfa_Mode)
then
Get_Index_Bounds (First_Index (E), Lo, Hi);
then
Get_Index_Bounds (First_Index (E), Lo, Hi);
-- --
------------------------------------------------------------------------------
-- --
------------------------------------------------------------------------------
with Types; use Types;
with Ada.IO_Exceptions; use Ada.IO_Exceptions;
with Types; use Types;
with Ada.IO_Exceptions; use Ada.IO_Exceptions;
C : Character;
use ASCII;
C : Character;
use ASCII;
-- Scope number for the current scope entity
Cur_File_Idx : File_Index;
-- Scope number for the current scope entity
Cur_File_Idx : File_Index;
- -- Index in ALFA_File_Table of the current file
+ -- Index in Alfa_File_Table of the current file
Cur_Scope_Idx : Scope_Index;
Cur_Scope_Idx : Scope_Index;
- -- Index in ALFA_Scope_Table of the current scope
+ -- Index in Alfa_Scope_Table of the current scope
Name_Str : String (1 .. 32768);
Name_Len : Natural := 0;
Name_Str : String (1 .. 32768);
Name_Len : Natural := 0;
end loop;
end Skip_Spaces;
end loop;
end Skip_Spaces;
--- Start of processing for Get_ALFA
+-- Start of processing for Get_Alfa
- Initialize_ALFA_Tables;
+ Initialize_Alfa_Tables;
Cur_File := 0;
Cur_Scope := 0;
Cur_File_Idx := 1;
Cur_Scope_Idx := 0;
Cur_File := 0;
Cur_Scope := 0;
Cur_File_Idx := 1;
Cur_Scope_Idx := 0;
- -- Loop through lines of ALFA information
+ -- Loop through lines of Alfa information
while Nextc = 'F' loop
Skipc;
while Nextc = 'F' loop
Skipc;
-- Make sure first line is a File line
-- Make sure first line is a File line
- if ALFA_File_Table.Last = 0 and then C /= 'D' then
+ if Alfa_File_Table.Last = 0 and then C /= 'D' then
raise Data_Error;
end if;
raise Data_Error;
end if;
-- Complete previous entry if any
-- Complete previous entry if any
- if ALFA_File_Table.Last /= 0 then
- ALFA_File_Table.Table (ALFA_File_Table.Last).To_Scope :=
- ALFA_Scope_Table.Last;
+ if Alfa_File_Table.Last /= 0 then
+ Alfa_File_Table.Table (Alfa_File_Table.Last).To_Scope :=
+ Alfa_Scope_Table.Last;
end if;
-- Scan out dependency number and file name
end if;
-- Scan out dependency number and file name
-- Make new File table entry (will fill in To_Scope later)
-- Make new File table entry (will fill in To_Scope later)
- ALFA_File_Table.Append (
+ Alfa_File_Table.Append (
(File_Name => new String'(Name_Str (1 .. Name_Len)),
File_Num => Cur_File,
(File_Name => new String'(Name_Str (1 .. Name_Len)),
File_Num => Cur_File,
- From_Scope => ALFA_Scope_Table.Last + 1,
+ From_Scope => Alfa_Scope_Table.Last + 1,
To_Scope => 0));
-- Initialize counter for scopes
To_Scope => 0));
-- Initialize counter for scopes
-- To_Xref later). Initial range (From_Xref .. To_Xref) is
-- empty for scopes without entities.
-- To_Xref later). Initial range (From_Xref .. To_Xref) is
-- empty for scopes without entities.
- ALFA_Scope_Table.Append (
+ Alfa_Scope_Table.Append (
(Scope_Entity => Empty,
Scope_Name => new String'(Name_Str (1 .. Name_Len)),
File_Num => Cur_File,
(Scope_Entity => Empty,
Scope_Name => new String'(Name_Str (1 .. Name_Len)),
File_Num => Cur_File,
-- Update component From_Xref of current file if first reference
-- in this file.
-- Update component From_Xref of current file if first reference
-- in this file.
- while ALFA_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
+ while Alfa_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
loop
Cur_File_Idx := Cur_File_Idx + 1;
end loop;
loop
Cur_File_Idx := Cur_File_Idx + 1;
end loop;
-- Update component To_Xref of previous scope
if Cur_Scope_Idx /= 0 then
-- Update component To_Xref of previous scope
if Cur_Scope_Idx /= 0 then
- ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
- ALFA_Xref_Table.Last;
+ Alfa_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
+ Alfa_Xref_Table.Last;
end if;
-- Update component From_Xref of current scope
end if;
-- Update component From_Xref of current scope
- Cur_Scope_Idx := ALFA_File_Table.Table (Cur_File_Idx).From_Scope;
+ Cur_Scope_Idx := Alfa_File_Table.Table (Cur_File_Idx).From_Scope;
- while ALFA_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /= Cur_Scope
+ while Alfa_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /= Cur_Scope
loop
Cur_Scope_Idx := Cur_Scope_Idx + 1;
end loop;
loop
Cur_Scope_Idx := Cur_Scope_Idx + 1;
end loop;
- ALFA_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
- ALFA_Xref_Table.Last + 1;
+ Alfa_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
+ Alfa_Xref_Table.Last + 1;
Rtype = 'm' or else
Rtype = 's');
Rtype = 'm' or else
Rtype = 's');
- ALFA_Xref_Table.Append (
+ Alfa_Xref_Table.Append (
(Entity_Name => XR_Entity,
Entity_Line => XR_Entity_Line,
Etype => XR_Entity_Typ,
(Entity_Name => XR_Entity,
Entity_Line => XR_Entity_Line,
Etype => XR_Entity_Typ,
- -- No other ALFA lines are possible
+ -- No other Alfa lines are possible
when others =>
raise Data_Error;
when others =>
raise Data_Error;
-- Here with all Xrefs stored, complete last entries in File/Scope tables
-- Here with all Xrefs stored, complete last entries in File/Scope tables
- if ALFA_File_Table.Last /= 0 then
- ALFA_File_Table.Table (ALFA_File_Table.Last).To_Scope :=
- ALFA_Scope_Table.Last;
+ if Alfa_File_Table.Last /= 0 then
+ Alfa_File_Table.Table (Alfa_File_Table.Last).To_Scope :=
+ Alfa_Scope_Table.Last;
end if;
if Cur_Scope_Idx /= 0 then
end if;
if Cur_Scope_Idx /= 0 then
- ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref := ALFA_Xref_Table.Last;
+ Alfa_Scope_Table.Table (Cur_Scope_Idx).To_Xref := Alfa_Xref_Table.Last;
-- --
------------------------------------------------------------------------------
-- --
------------------------------------------------------------------------------
--- This package contains the function used to read ALFA information from an
--- ALI file and populate the tables defined in package ALFA with the result.
+-- This package contains the function used to read Alfa information from an
+-- ALI file and populate the tables defined in package Alfa with the result.
generic
-- These subprograms provide access to the ALI file. Locating, opening and
generic
-- These subprograms provide access to the ALI file. Locating, opening and
-- and position to the next character, which will be returned by the next
-- call to Getc or Nextc.
-- and position to the next character, which will be returned by the next
-- call to Getc or Nextc.
-procedure Get_ALFA;
--- Load ALFA information from ALI file text format into internal ALFA tables
--- (ALFA.ALFA_Xref_Table, ALFA.ALFA_Scope_Table and ALFA.ALFA_File_Table). On
--- entry the input file is positioned to the initial 'F' of the first ALFA
+procedure Get_Alfa;
+-- Load Alfa information from ALI file text format into internal Alfa tables
+-- (Alfa.Alfa_Xref_Table, Alfa.Alfa_Scope_Table and Alfa.Alfa_File_Table). On
+-- entry the input file is positioned to the initial 'F' of the first Alfa
-- line in the ALI file. On return, the file is positioned either to the end
-- line in the ALI file. On return, the file is positioned either to the end
--- of file, or to the first character of the line following the ALFA
+-- of file, or to the first character of the line following the Alfa
-- information (which will never start with an 'F').
--
-- If a format error is detected in the input, then an exception is raised
-- information (which will never start with an 'F').
--
-- If a format error is detected in the input, then an exception is raised
if Debug_Flag_Dot_FF then
if Debug_Flag_Dot_FF then
-- Turn off inlining, which would confuse formal verification output
-- and gain nothing.
-- Turn off inlining, which would confuse formal verification output
-- and gain nothing.
-- Enable some restrictions systematically to simplify the generated
-- code (and ease analysis). Note that restriction checks are also
-- Enable some restrictions systematically to simplify the generated
-- code (and ease analysis). Note that restriction checks are also
- -- disabled in ALFA mode, see Restrict.Check_Restriction, and user
+ -- disabled in Alfa mode, see Restrict.Check_Restriction, and user
-- specified Restrictions pragmas are ignored, see
-- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
-- specified Restrictions pragmas are ignored, see
-- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
Polling_Required := False;
-- Set operating mode to Generate_Code, but full front-end expansion
Polling_Required := False;
-- Set operating mode to Generate_Code, but full front-end expansion
- -- is not desirable in ALFA mode, so a light expansion is performed
+ -- is not desirable in Alfa mode, so a light expansion is performed
-- instead.
Operating_Mode := Generate_Code;
-- instead.
Operating_Mode := Generate_Code;
Debug_Pragmas_Enabled := True;
-- Turn off style check options since we are not interested in any
Debug_Pragmas_Enabled := True;
-- Turn off style check options since we are not interested in any
- -- front-end warnings when we are getting ALFA output.
+ -- front-end warnings when we are getting Alfa output.
Reset_Style_Check_Options;
Reset_Style_Check_Options;
with Fname.UF; use Fname.UF;
with Lib.Util; use Lib.Util;
with Lib.Xref; use Lib.Xref;
with Fname.UF; use Fname.UF;
with Lib.Util; use Lib.Util;
with Lib.Xref; use Lib.Xref;
with Nlists; use Nlists;
with Gnatvsn; use Gnatvsn;
with Opt; use Opt;
with Nlists; use Nlists;
with Gnatvsn; use Gnatvsn;
with Opt; use Opt;
- -- Output ALFA information if needed
+ -- Output Alfa information if needed
- if Opt.Xref_Active and then ALFA_Mode then
- Collect_ALFA (Sdep_Table => Sdep_Table, Num_Sdep => Num_Sdep);
- Output_ALFA;
+ if Opt.Xref_Active and then Alfa_Mode then
+ Collect_Alfa (Sdep_Table => Sdep_Table, Num_Sdep => Num_Sdep);
+ Output_Alfa;
end if;
-- Output final blank line and we are done. This final blank line is
end if;
-- Output final blank line and we are done. This final blank line is
-- reference data. See the spec of Par_SCO for full details of the format.
----------------------
-- reference data. See the spec of Par_SCO for full details of the format.
----------------------
- -- The ALFA information follows the SCO information. See the spec of Alfa
+ -- The Alfa information follows the SCO information. See the spec of Alfa
-- for full details of the format.
----------------------
-- for full details of the format.
----------------------
-- --
------------------------------------------------------------------------------
-- --
------------------------------------------------------------------------------
with Einfo; use Einfo;
with Nmake; use Nmake;
with Einfo; use Einfo;
with Nmake; use Nmake;
with GNAT.HTable;
separate (Lib.Xref)
with GNAT.HTable;
separate (Lib.Xref)
---------------------
-- Local Constants --
---------------------
---------------------
-- Local Constants --
---------------------
- -- Table of ALFA_Entities, True for each entity kind used in ALFA
+ -- Table of Alfa_Entities, True for each entity kind used in Alfa
- ALFA_Entities : constant array (Entity_Kind) of Boolean :=
+ Alfa_Entities : constant array (Entity_Kind) of Boolean :=
(E_Void => False,
E_Variable => True,
E_Component => False,
(E_Void => False,
E_Variable => True,
E_Component => False,
E_Task_Body => False,
E_Subprogram_Body => False);
E_Task_Body => False,
E_Subprogram_Body => False);
- -- True for each reference type used in ALFA
- ALFA_References : constant array (Character) of Boolean :=
+ -- True for each reference type used in Alfa
+ Alfa_References : constant array (Character) of Boolean :=
('m' => True,
'r' => True,
's' => True,
('m' => True,
'r' => True,
's' => True,
-- Table of cross-references for reads and writes through explicit
-- dereferences, that are output as reads/writes to the special variable
-- "Heap". These references are added to the regular references when
-- Table of cross-references for reads and writes through explicit
-- dereferences, that are output as reads/writes to the special variable
-- "Heap". These references are added to the regular references when
- -- computing ALFA cross-references.
+ -- computing Alfa cross-references.
-----------------------
-- Local Subprograms --
-----------------------
-----------------------
-- Local Subprograms --
-----------------------
- procedure Add_ALFA_File (U : Unit_Number_Type; D : Nat);
- -- Add file U and all scopes in U to the tables ALFA_File_Table and
- -- ALFA_Scope_Table.
+ procedure Add_Alfa_File (U : Unit_Number_Type; D : Nat);
+ -- Add file U and all scopes in U to the tables Alfa_File_Table and
+ -- Alfa_Scope_Table.
- procedure Add_ALFA_Scope (N : Node_Id);
- -- Add scope N to the table ALFA_Scope_Table
+ procedure Add_Alfa_Scope (N : Node_Id);
+ -- Add scope N to the table Alfa_Scope_Table
- procedure Add_ALFA_Xrefs;
- -- Filter table Xrefs to add all references used in ALFA to the table
- -- ALFA_Xref_Table.
+ procedure Add_Alfa_Xrefs;
+ -- Filter table Xrefs to add all references used in Alfa to the table
+ -- Alfa_Xref_Table.
- procedure Detect_And_Add_ALFA_Scope (N : Node_Id);
- -- Call Add_ALFA_Scope on scopes
+ procedure Detect_And_Add_Alfa_Scope (N : Node_Id);
+ -- Call Add_Alfa_Scope on scopes
function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
-- Hash function for hash table
function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
-- Hash function for hash table
-- declarations.
-------------------
-- declarations.
-------------------
- procedure Add_ALFA_File (U : Unit_Number_Type; D : Nat) is
+ procedure Add_Alfa_File (U : Unit_Number_Type; D : Nat) is
From : Scope_Index;
S : constant Source_File_Index := Source_Index (U);
From : Scope_Index;
S : constant Source_File_Index := Source_Index (U);
- From := ALFA_Scope_Table.Last + 1;
+ From := Alfa_Scope_Table.Last + 1;
- Traverse_Compilation_Unit (Cunit (U), Detect_And_Add_ALFA_Scope'Access,
+ Traverse_Compilation_Unit (Cunit (U), Detect_And_Add_Alfa_Scope'Access,
Inside_Stubs => False);
-- Update scope numbers
Inside_Stubs => False);
-- Update scope numbers
- for S in From .. ALFA_Scope_Table.Last loop
+ for S in From .. Alfa_Scope_Table.Last loop
- E : Entity_Id renames ALFA_Scope_Table.Table (S).Scope_Entity;
+ E : Entity_Id renames Alfa_Scope_Table.Table (S).Scope_Entity;
begin
if Lib.Get_Source_Unit (E) = U then
begin
if Lib.Get_Source_Unit (E) = U then
- ALFA_Scope_Table.Table (S).Scope_Num := Count;
- ALFA_Scope_Table.Table (S).File_Num := D;
+ Alfa_Scope_Table.Table (S).Scope_Num := Count;
+ Alfa_Scope_Table.Table (S).File_Num := D;
-- U, for example for scope inside generics that get
-- instantiated.
-- U, for example for scope inside generics that get
-- instantiated.
- ALFA_Scope_Table.Table (S).Scope_Num := 0;
+ Alfa_Scope_Table.Table (S).Scope_Num := 0;
- for S in From .. ALFA_Scope_Table.Last loop
+ for S in From .. Alfa_Scope_Table.Last loop
-- Remove those scopes previously marked for removal
-- Remove those scopes previously marked for removal
- if ALFA_Scope_Table.Table (S).Scope_Num /= 0 then
- ALFA_Scope_Table.Table (Snew) := ALFA_Scope_Table.Table (S);
+ if Alfa_Scope_Table.Table (S).Scope_Num /= 0 then
+ Alfa_Scope_Table.Table (Snew) := Alfa_Scope_Table.Table (S);
Snew := Snew + 1;
end if;
end loop;
Snew := Snew + 1;
end if;
end loop;
- ALFA_Scope_Table.Set_Last (Snew - 1);
+ Alfa_Scope_Table.Set_Last (Snew - 1);
end;
-- Make entry for new file in file table
Get_Name_String (Reference_Name (S));
end;
-- Make entry for new file in file table
Get_Name_String (Reference_Name (S));
- ALFA_File_Table.Append (
+ Alfa_File_Table.Append (
(File_Name => new String'(Name_Buffer (1 .. Name_Len)),
File_Num => D,
From_Scope => From,
(File_Name => new String'(Name_Buffer (1 .. Name_Len)),
File_Num => D,
From_Scope => From,
- To_Scope => ALFA_Scope_Table.Last));
- end Add_ALFA_File;
+ To_Scope => Alfa_Scope_Table.Last));
+ end Add_Alfa_File;
- procedure Add_ALFA_Scope (N : Node_Id) is
+ procedure Add_Alfa_Scope (N : Node_Id) is
E : constant Entity_Id := Defining_Entity (N);
Loc : constant Source_Ptr := Sloc (E);
Typ : Character;
E : constant Entity_Id := Defining_Entity (N);
Loc : constant Source_Ptr := Sloc (E);
Typ : Character;
-- 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.
-- 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.
- ALFA_Scope_Table.Append (
+ Alfa_Scope_Table.Append (
(Scope_Name => new String'(Unique_Name (E)),
File_Num => 0,
Scope_Num => 0,
(Scope_Name => new String'(Unique_Name (E)),
File_Num => 0,
Scope_Num => 0,
From_Xref => 1,
To_Xref => 0,
Scope_Entity => E));
From_Xref => 1,
To_Xref => 0,
Scope_Entity => E));
- procedure Add_ALFA_Xrefs is
+ procedure Add_Alfa_Xrefs is
Cur_Scope_Idx : Scope_Index;
From_Xref_Idx : Xref_Index;
Cur_Entity : Entity_Id;
Cur_Scope_Idx : Scope_Index;
From_Xref_Idx : Xref_Index;
Cur_Entity : Entity_Id;
- -- Start of processing for Add_ALFA_Xrefs
+ -- Start of processing for Add_Alfa_Xrefs
- for J in ALFA_Scope_Table.First .. ALFA_Scope_Table.Last loop
- Set_Scope_Num (N => ALFA_Scope_Table.Table (J).Scope_Entity,
- Num => ALFA_Scope_Table.Table (J).Scope_Num);
+ for J in Alfa_Scope_Table.First .. Alfa_Scope_Table.Last loop
+ Set_Scope_Num (N => Alfa_Scope_Table.Table (J).Scope_Entity,
+ Num => Alfa_Scope_Table.Table (J).Scope_Num);
end loop;
-- Set up the pointer vector for the sort
end loop;
-- Set up the pointer vector for the sort
Rnums (Nrefs) := Xrefs.Last;
end loop;
Rnums (Nrefs) := Xrefs.Last;
end loop;
- -- Eliminate entries not appropriate for ALFA. Done prior to sorting
+ -- Eliminate entries not appropriate for Alfa. Done prior to sorting
-- cross-references, as it discards useless references which do not have
-- a proper format for the comparison function (like no location).
Eliminate_Before_Sort : declare
NR : Nat;
-- cross-references, as it discards useless references which do not have
-- a proper format for the comparison function (like no location).
Eliminate_Before_Sort : declare
NR : Nat;
- function Is_ALFA_Scope (E : Entity_Id) return Boolean;
+ function Is_Alfa_Scope (E : Entity_Id) return Boolean;
-- Return whether the entity or reference scope is adequate
function Is_Global_Constant (E : Entity_Id) return Boolean;
-- Return True if E is a global constant for which we should ignore
-- Return whether the entity or reference scope is adequate
function Is_Global_Constant (E : Entity_Id) return Boolean;
-- Return True if E is a global constant for which we should ignore
- function Is_ALFA_Scope (E : Entity_Id) return Boolean is
+ function Is_Alfa_Scope (E : Entity_Id) return Boolean is
begin
return Present (E)
and then not Is_Generic_Unit (E)
and then Renamed_Entity (E) = Empty
and then Get_Scope_Num (E) /= No_Scope;
begin
return Present (E)
and then not Is_Generic_Unit (E)
and then Renamed_Entity (E) = Empty
and then Get_Scope_Num (E) /= No_Scope;
------------------------
-- Is_Global_Constant --
------------------------
-- Is_Global_Constant --
Nrefs := 0;
for J in 1 .. NR loop
Nrefs := 0;
for J in 1 .. NR loop
- if ALFA_Entities (Ekind (Xrefs.Table (Rnums (J)).Ent))
- and then ALFA_References (Xrefs.Table (Rnums (J)).Typ)
- and then Is_ALFA_Scope (Xrefs.Table (Rnums (J)).Ent_Scope)
- and then Is_ALFA_Scope (Xrefs.Table (Rnums (J)).Ref_Scope)
+ if Alfa_Entities (Ekind (Xrefs.Table (Rnums (J)).Ent))
+ and then Alfa_References (Xrefs.Table (Rnums (J)).Typ)
+ and then Is_Alfa_Scope (Xrefs.Table (Rnums (J)).Ent_Scope)
+ and then Is_Alfa_Scope (Xrefs.Table (Rnums (J)).Ref_Scope)
and then not Is_Global_Constant (Xrefs.Table (Rnums (J)).Ent)
then
Nrefs := Nrefs + 1;
and then not Is_Global_Constant (Xrefs.Table (Rnums (J)).Ent)
then
Nrefs := Nrefs + 1;
From_Xref_Idx := 1;
Cur_Entity := Empty;
From_Xref_Idx := 1;
Cur_Entity := Empty;
- if ALFA_Scope_Table.Last = 0 then
+ if Alfa_Scope_Table.Last = 0 then
function Cur_Scope return Node_Id;
-- Return scope entity which corresponds to index Cur_Scope_Idx in
function Cur_Scope return Node_Id;
-- Return scope entity which corresponds to index Cur_Scope_Idx in
- -- table ALFA_Scope_Table.
+ -- table Alfa_Scope_Table.
function Get_Entity_Type (E : Entity_Id) return Character;
-- Return a character representing the type of entity
function Is_Future_Scope_Entity (E : Entity_Id) return Boolean;
function Get_Entity_Type (E : Entity_Id) return Character;
-- Return a character representing the type of entity
function Is_Future_Scope_Entity (E : Entity_Id) return Boolean;
- -- Check whether entity E is in ALFA_Scope_Table at index
+ -- Check whether entity E is in Alfa_Scope_Table at index
-- Cur_Scope_Idx or higher.
function Is_Past_Scope_Entity (E : Entity_Id) return Boolean;
-- Cur_Scope_Idx or higher.
function Is_Past_Scope_Entity (E : Entity_Id) return Boolean;
- -- Check whether entity E is in ALFA_Scope_Table at index strictly
+ -- Check whether entity E is in Alfa_Scope_Table at index strictly
-- lower than Cur_Scope_Idx.
---------------
-- lower than Cur_Scope_Idx.
---------------
function Cur_Scope return Node_Id is
begin
function Cur_Scope return Node_Id is
begin
- return ALFA_Scope_Table.Table (Cur_Scope_Idx).Scope_Entity;
+ return Alfa_Scope_Table.Table (Cur_Scope_Idx).Scope_Entity;
end Cur_Scope;
---------------------
end Cur_Scope;
---------------------
function Is_Future_Scope_Entity (E : Entity_Id) return Boolean is
begin
function Is_Future_Scope_Entity (E : Entity_Id) return Boolean is
begin
- for J in Cur_Scope_Idx .. ALFA_Scope_Table.Last loop
- if E = ALFA_Scope_Table.Table (J).Scope_Entity then
+ for J in Cur_Scope_Idx .. Alfa_Scope_Table.Last loop
+ if E = Alfa_Scope_Table.Table (J).Scope_Entity then
return True;
end if;
end loop;
return True;
end if;
end loop;
function Is_Past_Scope_Entity (E : Entity_Id) return Boolean is
begin
function Is_Past_Scope_Entity (E : Entity_Id) return Boolean is
begin
- for J in ALFA_Scope_Table.First .. Cur_Scope_Idx - 1 loop
- if E = ALFA_Scope_Table.Table (J).Scope_Entity then
+ for J in Alfa_Scope_Table.First .. Cur_Scope_Idx - 1 loop
+ if E = Alfa_Scope_Table.Table (J).Scope_Entity then
return True;
end if;
end loop;
return True;
end if;
end loop;
begin
-- If this assertion fails, the scope which we are looking for is
begin
-- If this assertion fails, the scope which we are looking for is
- -- not in ALFA scope table, which reveals either a problem in the
+ -- not in Alfa scope table, which reveals either a problem in the
-- construction of the scope table, or an erroneous scope for the
-- current cross-reference.
-- construction of the scope table, or an erroneous scope for the
-- current cross-reference.
-- considered.
if XE.Ent_Scope /= Cur_Scope then
-- considered.
if XE.Ent_Scope /= Cur_Scope then
- ALFA_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
+ Alfa_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
- ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
- ALFA_Xref_Table.Last;
- From_Xref_Idx := ALFA_Xref_Table.Last + 1;
+ Alfa_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
+ Alfa_Xref_Table.Last;
+ From_Xref_Idx := Alfa_Xref_Table.Last + 1;
end if;
while XE.Ent_Scope /= Cur_Scope loop
Cur_Scope_Idx := Cur_Scope_Idx + 1;
end if;
while XE.Ent_Scope /= Cur_Scope loop
Cur_Scope_Idx := Cur_Scope_Idx + 1;
- pragma Assert (Cur_Scope_Idx <= ALFA_Scope_Table.Last);
+ pragma Assert (Cur_Scope_Idx <= Alfa_Scope_Table.Last);
end loop;
if XE.Ent /= Cur_Entity then
end loop;
if XE.Ent /= Cur_Entity then
end if;
if XE.Ent = Heap then
end if;
if XE.Ent = Heap then
- ALFA_Xref_Table.Append (
+ Alfa_Xref_Table.Append (
(Entity_Name => Cur_Entity_Name,
Entity_Line => 0,
Etype => Get_Entity_Type (XE.Ent),
(Entity_Name => Cur_Entity_Name,
Entity_Line => 0,
Etype => Get_Entity_Type (XE.Ent),
Col => Int (Get_Column_Number (XE.Loc))));
else
Col => Int (Get_Column_Number (XE.Loc))));
else
- ALFA_Xref_Table.Append (
+ Alfa_Xref_Table.Append (
(Entity_Name => Cur_Entity_Name,
Entity_Line => Int (Get_Logical_Line_Number (XE.Def)),
Etype => Get_Entity_Type (XE.Ent),
(Entity_Name => Cur_Entity_Name,
Entity_Line => Int (Get_Logical_Line_Number (XE.Def)),
Etype => Get_Entity_Type (XE.Ent),
-- Update the range of cross references to which the scope refers to
-- Update the range of cross references to which the scope refers to
- ALFA_Scope_Table.Table (Cur_Scope_Idx).From_Xref := From_Xref_Idx;
- ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref := ALFA_Xref_Table.Last;
- end Add_ALFA_Xrefs;
+ Alfa_Scope_Table.Table (Cur_Scope_Idx).From_Xref := From_Xref_Idx;
+ Alfa_Scope_Table.Table (Cur_Scope_Idx).To_Xref := Alfa_Xref_Table.Last;
+ end Add_Alfa_Xrefs;
- procedure Collect_ALFA (Sdep_Table : Unit_Ref_Table; Num_Sdep : Nat) is
+ procedure Collect_Alfa (Sdep_Table : Unit_Ref_Table; Num_Sdep : Nat) is
begin
-- Cross-references should have been computed first
pragma Assert (Xrefs.Last /= 0);
begin
-- Cross-references should have been computed first
pragma Assert (Xrefs.Last /= 0);
- Initialize_ALFA_Tables;
+ Initialize_Alfa_Tables;
- -- Generate file and scope ALFA information
+ -- Generate file and scope Alfa information
for D in 1 .. Num_Sdep loop
for D in 1 .. Num_Sdep loop
if Units.Table (Sdep_Table (D)).Source_Index /=
System_Source_File_Index
then
if Units.Table (Sdep_Table (D)).Source_Index /=
System_Source_File_Index
then
- Add_ALFA_File (U => Sdep_Table (D), D => D);
+ Add_Alfa_File (U => Sdep_Table (D), D => D);
begin
-- Fill in the hash-table
begin
-- Fill in the hash-table
- for S in ALFA_Scope_Table.First .. ALFA_Scope_Table.Last loop
+ for S in Alfa_Scope_Table.First .. Alfa_Scope_Table.Last loop
- Srec : ALFA_Scope_Record renames ALFA_Scope_Table.Table (S);
+ Srec : Alfa_Scope_Record renames Alfa_Scope_Table.Table (S);
begin
Entity_Hash_Table.Set (Srec.Scope_Entity, S);
end;
begin
Entity_Hash_Table.Set (Srec.Scope_Entity, S);
end;
-- Use the hash-table to locate spec entities
-- Use the hash-table to locate spec entities
- for S in ALFA_Scope_Table.First .. ALFA_Scope_Table.Last loop
+ for S in Alfa_Scope_Table.First .. Alfa_Scope_Table.Last loop
- Srec : ALFA_Scope_Record renames ALFA_Scope_Table.Table (S);
+ Srec : Alfa_Scope_Record renames Alfa_Scope_Table.Table (S);
Spec_Entity : constant Entity_Id :=
Unique_Entity (Srec.Scope_Entity);
Spec_Entity : constant Entity_Id :=
Unique_Entity (Srec.Scope_Entity);
and then Spec_Scope /= 0
then
Srec.Spec_File_Num :=
and then Spec_Scope /= 0
then
Srec.Spec_File_Num :=
- ALFA_Scope_Table.Table (Spec_Scope).File_Num;
+ Alfa_Scope_Table.Table (Spec_Scope).File_Num;
- ALFA_Scope_Table.Table (Spec_Scope).Scope_Num;
+ Alfa_Scope_Table.Table (Spec_Scope).Scope_Num;
end if;
end;
end loop;
end;
end if;
end;
end loop;
end;
- -- Generate cross reference ALFA information
+ -- Generate cross reference Alfa information
- Add_ALFA_Xrefs;
- end Collect_ALFA;
+ Add_Alfa_Xrefs;
+ end Collect_Alfa;
-------------------------------
-------------------------------
- -- Detect_And_Add_ALFA_Scope --
+ -- Detect_And_Add_Alfa_Scope --
-------------------------------
-------------------------------
- procedure Detect_And_Add_ALFA_Scope (N : Node_Id) is
+ procedure Detect_And_Add_Alfa_Scope (N : Node_Id) is
begin
if Nkind_In (N, N_Subprogram_Declaration,
N_Subprogram_Body,
begin
if Nkind_In (N, N_Subprogram_Declaration,
N_Subprogram_Body,
N_Package_Declaration,
N_Package_Body)
then
N_Package_Declaration,
N_Package_Body)
then
- end Detect_And_Add_ALFA_Scope;
+ end Detect_And_Add_Alfa_Scope;
-------------------------------------
-- Enclosing_Subprogram_Or_Package --
-------------------------------------
-- Enclosing_Subprogram_Or_Package --
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
end Traverse_Subprogram_Body;
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
end Traverse_Subprogram_Body;
-- Unit number corresponding to Loc. Value is undefined and not
-- referenced if Loc is set to No_Location.
-- Unit number corresponding to Loc. Value is undefined and not
-- referenced if Loc is set to No_Location.
- -- The following components are only used for ALFA cross-references
+ -- The following components are only used for Alfa cross-references
Ref_Scope : Entity_Id;
-- Entity of the closest subprogram or package enclosing the reference
Ref_Scope : Entity_Id;
-- Entity of the closest subprogram or package enclosing the reference
Table_Name => "Xrefs");
----------------------
Table_Name => "Xrefs");
----------------------
- package body ALFA is separate;
+ package body Alfa is separate;
------------------------
-- Local Subprograms --
------------------------
-- Local Subprograms --
Ref := Original_Location (Sloc (Nod));
Def := Original_Location (Sloc (Ent));
Ref := Original_Location (Sloc (Nod));
Def := Original_Location (Sloc (Ent));
- Ref_Scope := ALFA.Enclosing_Subprogram_Or_Package (N);
- Ent_Scope := ALFA.Enclosing_Subprogram_Or_Package (Ent);
+ Ref_Scope := Alfa.Enclosing_Subprogram_Or_Package (N);
+ Ent_Scope := Alfa.Enclosing_Subprogram_Or_Package (Ent);
Xrefs.Increment_Last;
Indx := Xrefs.Last;
Xrefs.Increment_Last;
Indx := Xrefs.Last;
with Einfo; use Einfo;
with Lib.Util; use Lib.Util;
with Einfo; use Einfo;
with Lib.Util; use Lib.Util;
-- in the pragma is "there".
----------------------
-- in the pragma is "there".
----------------------
- -- This package defines procedures for collecting ALFA information and
+ -- This package defines procedures for collecting Alfa information and
-- printing in ALI files.
-- printing in ALI files.
function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id;
-- Return the closest enclosing subprogram of package
function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id;
-- Return the closest enclosing subprogram of package
procedure Traverse_All_Compilation_Units (Process : Node_Processing);
-- Call Process on all declarations through all compilation units
procedure Traverse_All_Compilation_Units (Process : Node_Processing);
-- Call Process on all declarations through all compilation units
- procedure Collect_ALFA (Sdep_Table : Unit_Ref_Table; Num_Sdep : Nat);
- -- Collect ALFA information from library units (for files and scopes)
+ procedure Collect_Alfa (Sdep_Table : Unit_Ref_Table; Num_Sdep : Nat);
+ -- Collect Alfa information from library units (for files and scopes)
-- and from cross-references. Fill in the tables in library package
-- and from cross-references. Fill in the tables in library package
- procedure Output_ALFA is new Put_ALFA;
- -- Output ALFA information to the ALI files, based on the information
- -- collected in the tables in library package called ALFA, and using
+ procedure Output_Alfa is new Put_Alfa;
+ -- Output Alfa information to the ALI files, based on the information
+ -- collected in the tables in library package called Alfa, and using
-----------------
-- Subprograms --
-----------------
-- Subprograms --
function Full_Expander_Active return Boolean is
begin
function Full_Expander_Active return Boolean is
begin
- return Expander_Active and not ALFA_Mode;
+ return Expander_Active and not Alfa_Mode;
end Full_Expander_Active;
----------------------------------
end Full_Expander_Active;
----------------------------------
-- Modes for Formal Verification --
-----------------------------------
-- Modes for Formal Verification --
-----------------------------------
- ALFA_Mode : Boolean := False;
+ Alfa_Mode : Boolean := False;
-- Specific compiling mode targeting formal verification through the
-- generation of Why code for those parts of the input code that belong to
-- Specific compiling mode targeting formal verification through the
-- generation of Why code for those parts of the input code that belong to
- -- the ALFA subset of Ada. Set by debug flag -gnatd.F.
+ -- the Alfa subset of Ada. Set by debug flag -gnatd.F.
function Full_Expander_Active return Boolean;
pragma Inline (Full_Expander_Active);
function Full_Expander_Active return Boolean;
pragma Inline (Full_Expander_Active);
- -- Returns the value of (Expander_Active and not ALFA_Mode). This "flag"
+ -- Returns the value of (Expander_Active and not Alfa_Mode). This "flag"
-- indicates that expansion is fully active, that is, not in the reduced
-- mode for Alfa (True) or that expansion is either deactivated, or active
-- in the reduced mode for Alfa (False). For more information on full
-- indicates that expansion is fully active, that is, not in the reduced
-- mode for Alfa (True) or that expansion is either deactivated, or active
-- in the reduced mode for Alfa (False). For more information on full
-- --
------------------------------------------------------------------------------
-- --
------------------------------------------------------------------------------
- -- Loop through entries in ALFA_File_Table
+ -- Loop through entries in Alfa_File_Table
- for J in 1 .. ALFA_File_Table.Last loop
+ for J in 1 .. Alfa_File_Table.Last loop
- F : ALFA_File_Record renames ALFA_File_Table.Table (J);
+ F : Alfa_File_Record renames Alfa_File_Table.Table (J);
Start : Scope_Index;
Stop : Scope_Index;
Start : Scope_Index;
Stop : Scope_Index;
pragma Assert (Start <= Stop);
declare
pragma Assert (Start <= Stop);
declare
- S : ALFA_Scope_Record renames ALFA_Scope_Table.Table (Start);
+ S : Alfa_Scope_Record renames Alfa_Scope_Table.Table (Start);
begin
Write_Info_Initiate ('F');
begin
Write_Info_Initiate ('F');
- -- Loop through entries in ALFA_File_Table
+ -- Loop through entries in Alfa_File_Table
- for J in 1 .. ALFA_File_Table.Last loop
+ for J in 1 .. Alfa_File_Table.Last loop
- F : ALFA_File_Record renames ALFA_File_Table.Table (J);
+ F : Alfa_File_Record renames Alfa_File_Table.Table (J);
Start : Scope_Index;
Stop : Scope_Index;
File : Nat;
Start : Scope_Index;
Stop : Scope_Index;
File : Nat;
pragma Assert (Start <= Stop);
Output_One_Scope : declare
pragma Assert (Start <= Stop);
Output_One_Scope : declare
- S : ALFA_Scope_Record renames ALFA_Scope_Table.Table (Start);
+ S : Alfa_Scope_Record renames Alfa_Scope_Table.Table (Start);
XStart : Xref_Index;
XStop : Xref_Index;
XStart : Xref_Index;
XStop : Xref_Index;
pragma Assert (XStart <= XStop);
Output_One_Xref : declare
pragma Assert (XStart <= XStop);
Output_One_Xref : declare
- R : ALFA_Xref_Record renames
- ALFA_Xref_Table.Table (XStart);
+ R : Alfa_Xref_Record renames
+ Alfa_Xref_Table.Table (XStart);
begin
if R.Entity_Line /= Entity_Line
begin
if R.Entity_Line /= Entity_Line
-- --
------------------------------------------------------------------------------
-- --
------------------------------------------------------------------------------
--- This package contains the function used to read ALFA information from the
--- internal tables defined in package ALFA, and output text information for
+-- This package contains the function used to read Alfa information from the
+-- internal tables defined in package Alfa, and output text information for
-- the ALI file. The interface allows control over the destination of the
-- output, so that this routine can also be used for debugging purposes.
-- the ALI file. The interface allows control over the destination of the
-- output, so that this routine can also be used for debugging purposes.
with procedure Write_Info_Terminate is <>;
-- Terminate current info line and output lines built in Info_Buffer
with procedure Write_Info_Terminate is <>;
-- Terminate current info line and output lines built in Info_Buffer
-procedure Put_ALFA;
--- Read information from ALFA tables (ALFA.ALFA_Xref_Table,
--- ALFA.ALFA_Scope_Table and ALFA.ALFA_File_Table) and output corresponding
+procedure Put_Alfa;
+-- Read information from Alfa tables (Alfa.Alfa_Xref_Table,
+-- Alfa.Alfa_Scope_Table and Alfa.Alfa_File_Table) and output corresponding
-- information in ALI format using the Write_Info procedures.
-- information in ALI format using the Write_Info procedures.
begin
Msg_Issued := False;
begin
Msg_Issued := False;
- -- In CodePeer and ALFA mode, we do not want to check for any
+ -- In CodePeer and Alfa mode, we do not want to check for any
-- restriction, or set additional restrictions other than those already
-- set in gnat1drv.adb so that we have consistency between each
-- compilation.
-- restriction, or set additional restrictions other than those already
-- set in gnat1drv.adb so that we have consistency between each
-- compilation.
- if CodePeer_Mode or ALFA_Mode then
+ if CodePeer_Mode or Alfa_Mode then
begin
if pthread_setaffinity_np'Address /= System.Null_Address then
declare
begin
if pthread_setaffinity_np'Address /= System.Null_Address then
declare
- CPU_Set : access cpu_set_t := null;
+ type cpu_set_t_ptr is access all cpu_set_t;
+
+ CPU_Set : cpu_set_t_ptr := null;
Result : Interfaces.C.int;
begin
Result : Interfaces.C.int;
begin
or else Might_Inline_Subp)
and then not Is_Actual_Pack
and then not Inline_Now
or else Might_Inline_Subp)
and then not Is_Actual_Pack
and then not Inline_Now
and then (Operating_Mode = Generate_Code
or else (Operating_Mode = Check_Semantics
and then ASIS_Mode));
and then (Operating_Mode = Generate_Code
or else (Operating_Mode = Check_Semantics
and then ASIS_Mode));
end if;
-- Process Ignore_Rep_Clauses option (we also ignore rep clauses in
end if;
-- Process Ignore_Rep_Clauses option (we also ignore rep clauses in
- -- CodePeer mode or ALFA mode, since they are not relevant in these
+ -- CodePeer mode or Alfa mode, since they are not relevant in these
- if Ignore_Rep_Clauses or CodePeer_Mode or ALFA_Mode then
+ if Ignore_Rep_Clauses or CodePeer_Mode or Alfa_Mode then
case Id is
-- The following should be ignored. They do not affect legality
case Id is
-- The following should be ignored. They do not affect legality
Rewrite (N, Make_Null_Statement (Sloc (N)));
return;
Rewrite (N, Make_Null_Statement (Sloc (N)));
return;
- -- We do not want too ignore 'Small in CodePeer_Mode or ALFA_Mode,
+ -- We do not want too ignore 'Small in CodePeer_Mode or Alfa_Mode,
-- since it has an impact on the exact computations performed.
-- Perhaps 'Small should also not be ignored by
-- since it has an impact on the exact computations performed.
-- Perhaps 'Small should also not be ignored by
-- and First_Rep_Item info, which should not be relied upon in formal
-- verification.
-- and First_Rep_Item info, which should not be relied upon in formal
-- verification.
-- If the range of the type is already symmetric with a possible
-- extra negative value, leave it this way.
-- If the range of the type is already symmetric with a possible
-- extra negative value, leave it this way.
-- In formal verification mode, keep track of all reads and writes
-- through explicit dereferences.
-- In formal verification mode, keep track of all reads and writes
-- through explicit dereferences.
- if ALFA_Mode then
- ALFA.Generate_Dereference (N);
+ if Alfa_Mode then
+ Alfa.Generate_Dereference (N);
if Nkind (D_Copy) = N_Function_Call
or else
if Nkind (D_Copy) = N_Function_Call
or else
and then (Nkind (D_Copy) = N_Attribute_Reference
and then
(Attribute_Name (D_Copy) = Name_Result
and then (Nkind (D_Copy) = N_Attribute_Reference
and then
(Attribute_Name (D_Copy) = Name_Result
-- than inserted in the code, in order to facilitate a distinct
-- treatment for them.
-- than inserted in the code, in order to facilitate a distinct
-- treatment for them.
Process_PPCs (N, Gen_Id, Body_Id);
end if;
Process_PPCs (N, Gen_Id, Body_Id);
end if;
-- than inserted in the code, in order to facilitate a distinct
-- treatment for them.
-- than inserted in the code, in order to facilitate a distinct
-- treatment for them.
Process_PPCs (N, Spec_Id, Body_Id);
end if;
Process_PPCs (N, Spec_Id, Body_Id);
end if;
-- expanded in subsequent instantiations.
if Is_Actual and then Is_Abstract_Subprogram (Formal_Spec)
-- expanded in subsequent instantiations.
if Is_Actual and then Is_Abstract_Subprogram (Formal_Spec)
- and then Expander_Active
+ and then Full_Expander_Active
then
declare
Stream_Prim : Entity_Id;
then
declare
Stream_Prim : Entity_Id;
-- In formal verification mode, analyze pragma expression for
-- correctness, as it is not expanded later.
-- In formal verification mode, analyze pragma expression for
-- correctness, as it is not expanded later.
Analyze_PPC_In_Decl_Part
(N, Defining_Entity (Unit (Parent (Parent (N)))));
end if;
Analyze_PPC_In_Decl_Part
(N, Defining_Entity (Unit (Parent (Parent (N)))));
end if;
-- Start of processing for Process_Restrictions_Or_Restriction_Warnings
begin
-- Start of processing for Process_Restrictions_Or_Restriction_Warnings
begin
- -- Ignore all Restrictions pragma in CodePeer and ALFA modes
+ -- Ignore all Restrictions pragma in CodePeer and Alfa modes
- if CodePeer_Mode or ALFA_Mode then
+ if CodePeer_Mode or Alfa_Mode then
-- Start of processing for Process_Suppress_Unsuppress
begin
-- Start of processing for Process_Suppress_Unsuppress
begin
- -- Ignore pragma Suppress/Unsuppress in CodePeer and ALFA modes on
+ -- Ignore pragma Suppress/Unsuppress in CodePeer and Alfa modes on
-- user code: we want to generate checks for analysis purposes, as
-- set respectively by -gnatC and -gnatd.F
-- user code: we want to generate checks for analysis purposes, as
-- set respectively by -gnatC and -gnatd.F
- if (CodePeer_Mode or ALFA_Mode)
+ if (CodePeer_Mode or Alfa_Mode)
and then Comes_From_Source (N)
then
return;
and then Comes_From_Source (N)
then
return;
Check_Restriction (No_Initialize_Scalars, N);
-- Initialize_Scalars creates false positives in CodePeer, and
Check_Restriction (No_Initialize_Scalars, N);
-- Initialize_Scalars creates false positives in CodePeer, and
- -- incorrect negative results in ALFA mode, so ignore this pragma
+ -- incorrect negative results in Alfa mode, so ignore this pragma
-- in these modes.
if not Restriction_Active (No_Initialize_Scalars)
-- in these modes.
if not Restriction_Active (No_Initialize_Scalars)
- and then not (CodePeer_Mode or ALFA_Mode)
+ and then not (CodePeer_Mode or Alfa_Mode)
then
Init_Or_Norm_Scalars := True;
Initialize_Scalars := True;
then
Init_Or_Norm_Scalars := True;
Initialize_Scalars := True;
when Pragma_Inline_Always =>
GNAT_Pragma;
when Pragma_Inline_Always =>
GNAT_Pragma;
- -- Pragma always active unless in CodePeer or ALFA mode, since
+ -- Pragma always active unless in CodePeer or Alfa mode, since
-- this causes walk order issues.
-- this causes walk order issues.
- if not (CodePeer_Mode or ALFA_Mode) then
+ if not (CodePeer_Mode or Alfa_Mode) then
Process_Inline (True);
end if;
Process_Inline (True);
end if;
Check_Valid_Configuration_Pragma;
-- Normalize_Scalars creates false positives in CodePeer, and
Check_Valid_Configuration_Pragma;
-- Normalize_Scalars creates false positives in CodePeer, and
- -- incorrect negative results in ALFA mode, so ignore this pragma
+ -- incorrect negative results in Alfa mode, so ignore this pragma
- if not (CodePeer_Mode or ALFA_Mode) then
+ if not (CodePeer_Mode or Alfa_Mode) then
Normalize_Scalars := True;
Init_Or_Norm_Scalars := True;
end if;
Normalize_Scalars := True;
Init_Or_Norm_Scalars := True;
end if;
-- complex front-end expansions related to pragma Pack,
-- so disable handling of pragma Pack in these cases.
-- complex front-end expansions related to pragma Pack,
-- so disable handling of pragma Pack in these cases.
- if CodePeer_Mode or ALFA_Mode then
+ if CodePeer_Mode or Alfa_Mode then
null;
-- Don't attempt any packing for VM targets. We possibly
null;
-- Don't attempt any packing for VM targets. We possibly
-- If it is a named association, treat the selector_name as a
-- proper identifier, and mark the corresponding entity. Ignore
-- If it is a named association, treat the selector_name as a
-- proper identifier, and mark the corresponding entity. Ignore
- -- this reference in ALFA mode, as it refers to an entity not in
+ -- this reference in Alfa mode, as it refers to an entity not in
-- scope at the point of reference, so the reference should be
-- ignored for computing effects of subprograms.
if Nkind (Parent (A)) = N_Parameter_Association
-- scope at the point of reference, so the reference should be
-- ignored for computing effects of subprograms.
if Nkind (Parent (A)) = N_Parameter_Association
then
Set_Entity (Selector_Name (Parent (A)), F);
Generate_Reference (F, Selector_Name (Parent (A)));
then
Set_Entity (Selector_Name (Parent (A)), F);
Generate_Reference (F, Selector_Name (Parent (A)));
procedure Resolve_Quantified_Expression (N : Node_Id; Typ : Entity_Id) is
begin
procedure Resolve_Quantified_Expression (N : Node_Id; Typ : Entity_Id) is
begin
-- If expansion is enabled, analysis is delayed until the expresssion
-- is rewritten as a loop.
-- If expansion is enabled, analysis is delayed until the expresssion
-- is rewritten as a loop.
Resolve (Condition (N), Typ);
Expander_Mode_Restore;
Resolve (Condition (N), Typ);
Expander_Mode_Restore;
- -- In ALFA mode, we need normal expansion in order to properly introduce
+ -- In Alfa mode, we need normal expansion in order to properly introduce
-- the necessary transient scopes.
else
-- the necessary transient scopes.
else
-- In formal verification mode, keep track of all reads and
-- writes through explicit dereferences.
-- In formal verification mode, keep track of all reads and
-- writes through explicit dereferences.
- if ALFA_Mode then
- ALFA.Generate_Dereference (N, 'm');
+ if Alfa_Mode then
+ Alfa.Generate_Dereference (N, 'm');
end if;
if Nkind (P) = N_Selected_Component
end if;
if Nkind (P) = N_Selected_Component