[multiple changes]
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
This commit is contained in:
parent
7cda9727ba
commit
56812278e8
@ -1,3 +1,17 @@
|
||||
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,
|
||||
|
@ -50,6 +50,7 @@ int
|
||||
int
|
||||
__gnat_set_affinity_mask (int tid, unsigned mask)
|
||||
{
|
||||
int index;
|
||||
cpuset_t cpuset;
|
||||
|
||||
CPUSET_ZERO(cpuset);
|
||||
|
@ -24,9 +24,9 @@
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Output; use Output;
|
||||
with Put_ALFA;
|
||||
with Put_Alfa;
|
||||
|
||||
package body ALFA is
|
||||
package body Alfa is
|
||||
|
||||
-----------
|
||||
-- dalfa --
|
||||
@ -34,14 +34,14 @@ package body ALFA is
|
||||
|
||||
procedure dalfa is
|
||||
begin
|
||||
-- Dump ALFA file table
|
||||
-- Dump Alfa file table
|
||||
|
||||
Write_Line ("ALFA File Table");
|
||||
Write_Line ("Alfa File Table");
|
||||
Write_Line ("---------------");
|
||||
|
||||
for Index in 1 .. ALFA_File_Table.Last loop
|
||||
for Index in 1 .. Alfa_File_Table.Last loop
|
||||
declare
|
||||
AFR : ALFA_File_Record renames ALFA_File_Table.Table (Index);
|
||||
AFR : Alfa_File_Record renames Alfa_File_Table.Table (Index);
|
||||
|
||||
begin
|
||||
Write_Str (" ");
|
||||
@ -63,15 +63,15 @@ package body ALFA is
|
||||
end;
|
||||
end loop;
|
||||
|
||||
-- Dump ALFA scope table
|
||||
-- Dump Alfa scope table
|
||||
|
||||
Write_Eol;
|
||||
Write_Line ("ALFA Scope Table");
|
||||
Write_Line ("Alfa Scope Table");
|
||||
Write_Line ("----------------");
|
||||
|
||||
for Index in 1 .. ALFA_Scope_Table.Last loop
|
||||
for Index in 1 .. Alfa_Scope_Table.Last loop
|
||||
declare
|
||||
ASR : ALFA_Scope_Record renames ALFA_Scope_Table.Table (Index);
|
||||
ASR : Alfa_Scope_Record renames Alfa_Scope_Table.Table (Index);
|
||||
|
||||
begin
|
||||
Write_Str (" ");
|
||||
@ -103,15 +103,15 @@ package body ALFA is
|
||||
end;
|
||||
end loop;
|
||||
|
||||
-- Dump ALFA cross-reference table
|
||||
-- Dump Alfa cross-reference table
|
||||
|
||||
Write_Eol;
|
||||
Write_Line ("ALFA Xref Table");
|
||||
Write_Line ("Alfa Xref Table");
|
||||
Write_Line ("---------------");
|
||||
|
||||
for Index in 1 .. ALFA_Xref_Table.Last loop
|
||||
for Index in 1 .. Alfa_Xref_Table.Last loop
|
||||
declare
|
||||
AXR : ALFA_Xref_Record renames ALFA_Xref_Table.Table (Index);
|
||||
AXR : Alfa_Xref_Record renames Alfa_Xref_Table.Table (Index);
|
||||
|
||||
begin
|
||||
Write_Str (" ");
|
||||
@ -146,12 +146,12 @@ package body ALFA is
|
||||
-- Initialize --
|
||||
----------------
|
||||
|
||||
procedure Initialize_ALFA_Tables is
|
||||
procedure Initialize_Alfa_Tables is
|
||||
begin
|
||||
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;
|
||||
|
||||
-----------
|
||||
-- palfa --
|
||||
@ -192,12 +192,12 @@ package body ALFA is
|
||||
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
|
||||
Debug_Put_ALFA;
|
||||
Debug_Put_Alfa;
|
||||
end palfa;
|
||||
|
||||
end ALFA;
|
||||
end Alfa;
|
||||
|
@ -23,41 +23,41 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
-- 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;
|
||||
|
||||
package ALFA is
|
||||
package Alfa is
|
||||
|
||||
-- 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.
|
||||
-- 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
|
||||
-- unit.
|
||||
|
||||
-- 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.
|
||||
|
||||
-- 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.
|
||||
|
||||
-- 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.
|
||||
|
||||
---------------------
|
||||
-- ALFA ALI Format --
|
||||
-- Alfa ALI 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.
|
||||
|
||||
-- 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.
|
||||
|
||||
-- -------------------
|
||||
@ -86,7 +86,7 @@ package ALFA is
|
||||
|
||||
-- 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)?
|
||||
@ -186,13 +186,13 @@ package ALFA is
|
||||
-- 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 ALFA_Xref_Record is record
|
||||
type Alfa_Xref_Record is record
|
||||
Entity_Name : String_Ptr;
|
||||
-- Pointer to entity name in ALI file
|
||||
|
||||
@ -232,8 +232,8 @@ package ALFA is
|
||||
-- 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,
|
||||
@ -250,7 +250,7 @@ package ALFA is
|
||||
-- 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
|
||||
|
||||
@ -293,8 +293,8 @@ package ALFA is
|
||||
-- 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,
|
||||
@ -311,7 +311,7 @@ package ALFA is
|
||||
-- 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
|
||||
|
||||
@ -325,8 +325,8 @@ package ALFA is
|
||||
-- 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,
|
||||
@ -344,15 +344,15 @@ package ALFA is
|
||||
-- Subprograms --
|
||||
-----------------
|
||||
|
||||
procedure Initialize_ALFA_Tables;
|
||||
procedure Initialize_Alfa_Tables;
|
||||
-- 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;
|
||||
-- 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.
|
||||
|
||||
end ALFA;
|
||||
end Alfa;
|
||||
|
@ -23,23 +23,23 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
-- 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 utility using:
|
||||
|
||||
-- ALFA_Test file.ali
|
||||
-- Alfa_Test file.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
|
||||
-- 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.
|
||||
|
||||
with Get_ALFA;
|
||||
with Put_ALFA;
|
||||
with Get_Alfa;
|
||||
with Put_Alfa;
|
||||
|
||||
with ALFA; use ALFA;
|
||||
with Alfa; use Alfa;
|
||||
with Types; use Types;
|
||||
|
||||
with Ada.Command_Line; use Ada.Command_Line;
|
||||
@ -47,7 +47,7 @@ with Ada.Streams; use Ada.Streams;
|
||||
with Ada.Streams.Stream_IO; use Ada.Streams.Stream_IO;
|
||||
with Ada.Text_IO;
|
||||
|
||||
procedure ALFA_Test is
|
||||
procedure Alfa_Test is
|
||||
Infile : File_Type;
|
||||
Outfile_1 : File_Type;
|
||||
Outfile_2 : File_Type;
|
||||
@ -133,8 +133,8 @@ begin
|
||||
end if;
|
||||
end Put_Char;
|
||||
|
||||
-- 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;
|
||||
@ -180,7 +180,7 @@ begin
|
||||
C := Getc;
|
||||
end Skipc;
|
||||
|
||||
-- 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);
|
||||
@ -237,10 +237,10 @@ begin
|
||||
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
|
||||
|
||||
@ -267,15 +267,15 @@ begin
|
||||
|
||||
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
|
||||
-- to Outfile_1.
|
||||
|
||||
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
|
||||
|
||||
Put_ALFA_Info;
|
||||
Put_Alfa_Info;
|
||||
|
||||
-- Junk blank line (see comment at end of Lib.Writ)
|
||||
|
||||
@ -329,4 +329,4 @@ begin
|
||||
exception
|
||||
when Stop =>
|
||||
null;
|
||||
end ALFA_Test;
|
||||
end Alfa_Test;
|
||||
|
@ -56,7 +56,7 @@ package body ALI is
|
||||
'S' => True, -- specific dispatching
|
||||
'Y' => True, -- limited_with
|
||||
'C' => True, -- SCO information
|
||||
'F' => True, -- ALFA information
|
||||
'F' => True, -- Alfa information
|
||||
others => False);
|
||||
|
||||
--------------------
|
||||
@ -2442,7 +2442,7 @@ package body ALI is
|
||||
-- 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).
|
||||
|
||||
Check_Unknown_Line;
|
||||
|
||||
|
@ -123,7 +123,7 @@ package body Debug is
|
||||
-- d.C Generate concatenation call, do not generate inline code
|
||||
-- d.D
|
||||
-- d.E
|
||||
-- d.F ALFA mode
|
||||
-- d.F Alfa mode
|
||||
-- d.G Precondition only mode for gnat2why
|
||||
-- d.H Standard package only mode for gnat2why
|
||||
-- d.I SCIL generation mode
|
||||
@ -580,7 +580,7 @@ package body Debug is
|
||||
-- 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.
|
||||
|
||||
|
@ -6922,6 +6922,13 @@ package body Einfo is
|
||||
if Present (Corresponding_Record_Type (Id)) then
|
||||
return Direct_Primitive_Operations
|
||||
(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;
|
||||
|
@ -2849,10 +2849,10 @@ package body Errout is
|
||||
|
||||
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.
|
||||
|
||||
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
|
||||
|
@ -495,8 +495,8 @@ package Errout is
|
||||
-- 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
|
||||
|
@ -955,12 +955,12 @@ package body Erroutc is
|
||||
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
|
||||
Set_Msg_Name_Buffer;
|
||||
|
||||
-- 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);
|
||||
|
@ -6292,7 +6292,7 @@ package body Exp_Ch4 is
|
||||
|
||||
-- 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
|
||||
return;
|
||||
end if;
|
||||
|
||||
|
@ -3504,7 +3504,7 @@ package body Exp_Ch7 is
|
||||
-- this node and enclosed expression are not expanded, so do not apply
|
||||
-- any transformations here.
|
||||
|
||||
elsif ALFA_Mode
|
||||
elsif Alfa_Mode
|
||||
and then Nkind (Wrap_Node) = N_Pragma
|
||||
and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
|
||||
then
|
||||
|
@ -128,13 +128,13 @@ package body Expander is
|
||||
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.
|
||||
|
||||
if ALFA_Mode then
|
||||
if Alfa_Mode then
|
||||
Expand_Alfa (N);
|
||||
|
||||
-- Here for normal non-ALFA mode
|
||||
-- Here for normal non-Alfa mode
|
||||
|
||||
else
|
||||
-- Processing depends on node kind. For full details on the
|
||||
|
@ -2246,13 +2246,13 @@ package body Freeze is
|
||||
|
||||
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.
|
||||
|
||||
and then not (CodePeer_Mode or ALFA_Mode)
|
||||
and then not (CodePeer_Mode or Alfa_Mode)
|
||||
then
|
||||
-- If implicit packing enabled, do it
|
||||
|
||||
@ -3066,7 +3066,7 @@ package body Freeze is
|
||||
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);
|
||||
|
||||
|
@ -23,12 +23,12 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with ALFA; use ALFA;
|
||||
with Alfa; use Alfa;
|
||||
with Types; use Types;
|
||||
|
||||
with Ada.IO_Exceptions; use Ada.IO_Exceptions;
|
||||
|
||||
procedure Get_ALFA is
|
||||
procedure Get_Alfa is
|
||||
C : Character;
|
||||
|
||||
use ASCII;
|
||||
@ -41,10 +41,10 @@ procedure Get_ALFA is
|
||||
-- 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;
|
||||
-- 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;
|
||||
@ -193,17 +193,17 @@ procedure Get_ALFA is
|
||||
end loop;
|
||||
end Skip_Spaces;
|
||||
|
||||
-- Start of processing for Get_ALFA
|
||||
-- Start of processing for Get_Alfa
|
||||
|
||||
begin
|
||||
Initialize_ALFA_Tables;
|
||||
Initialize_Alfa_Tables;
|
||||
|
||||
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;
|
||||
@ -212,7 +212,7 @@ begin
|
||||
|
||||
-- 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;
|
||||
|
||||
@ -226,9 +226,9 @@ begin
|
||||
|
||||
-- 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
|
||||
@ -240,10 +240,10 @@ begin
|
||||
|
||||
-- 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,
|
||||
From_Scope => ALFA_Scope_Table.Last + 1,
|
||||
From_Scope => Alfa_Scope_Table.Last + 1,
|
||||
To_Scope => 0));
|
||||
|
||||
-- Initialize counter for scopes
|
||||
@ -300,7 +300,7 @@ begin
|
||||
-- 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,
|
||||
@ -332,7 +332,7 @@ begin
|
||||
-- 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;
|
||||
@ -348,21 +348,21 @@ begin
|
||||
-- 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
|
||||
|
||||
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;
|
||||
|
||||
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;
|
||||
|
||||
-- Cross reference entry
|
||||
|
||||
@ -437,7 +437,7 @@ begin
|
||||
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,
|
||||
@ -453,7 +453,7 @@ begin
|
||||
end loop;
|
||||
end;
|
||||
|
||||
-- No other ALFA lines are possible
|
||||
-- No other Alfa lines are possible
|
||||
|
||||
when others =>
|
||||
raise Data_Error;
|
||||
@ -468,12 +468,12 @@ begin
|
||||
|
||||
-- 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
|
||||
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;
|
||||
end Get_ALFA;
|
||||
end Get_Alfa;
|
||||
|
@ -23,8 +23,8 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
-- 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
|
||||
@ -46,12 +46,12 @@ generic
|
||||
-- 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
|
||||
-- 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
|
||||
|
@ -390,7 +390,7 @@ procedure Gnat1drv is
|
||||
|
||||
if Debug_Flag_Dot_FF then
|
||||
|
||||
ALFA_Mode := True;
|
||||
Alfa_Mode := True;
|
||||
|
||||
-- Turn off inlining, which would confuse formal verification output
|
||||
-- and gain nothing.
|
||||
@ -406,7 +406,7 @@ procedure Gnat1drv is
|
||||
|
||||
-- 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.
|
||||
|
||||
@ -436,7 +436,7 @@ procedure Gnat1drv is
|
||||
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;
|
||||
@ -464,7 +464,7 @@ procedure Gnat1drv is
|
||||
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;
|
||||
|
||||
|
@ -32,7 +32,7 @@ with Fname; use Fname;
|
||||
with Fname.UF; use Fname.UF;
|
||||
with Lib.Util; use Lib.Util;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
use Lib.Xref.ALFA;
|
||||
use Lib.Xref.Alfa;
|
||||
with Nlists; use Nlists;
|
||||
with Gnatvsn; use Gnatvsn;
|
||||
with Opt; use Opt;
|
||||
@ -1317,11 +1317,11 @@ package body Lib.Writ is
|
||||
SCO_Output;
|
||||
end if;
|
||||
|
||||
-- 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
|
||||
|
@ -712,10 +712,10 @@ package Lib.Writ is
|
||||
-- reference data. See the spec of Par_SCO for full details of the format.
|
||||
|
||||
----------------------
|
||||
-- ALFA Information --
|
||||
-- Alfa Information --
|
||||
----------------------
|
||||
|
||||
-- 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.
|
||||
|
||||
----------------------
|
||||
|
@ -23,23 +23,23 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with ALFA; use ALFA;
|
||||
with Alfa; use Alfa;
|
||||
with Einfo; use Einfo;
|
||||
with Nmake; use Nmake;
|
||||
with Put_ALFA;
|
||||
with Put_Alfa;
|
||||
|
||||
with GNAT.HTable;
|
||||
|
||||
separate (Lib.Xref)
|
||||
package body ALFA is
|
||||
package body Alfa is
|
||||
|
||||
---------------------
|
||||
-- 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,
|
||||
@ -135,8 +135,8 @@ package body ALFA is
|
||||
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,
|
||||
@ -159,25 +159,25 @@ package body ALFA is
|
||||
-- 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 --
|
||||
-----------------------
|
||||
|
||||
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
|
||||
@ -206,10 +206,10 @@ package body ALFA is
|
||||
-- declarations.
|
||||
|
||||
-------------------
|
||||
-- Add_ALFA_File --
|
||||
-- Add_Alfa_File --
|
||||
-------------------
|
||||
|
||||
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);
|
||||
@ -222,9 +222,9 @@ package body ALFA is
|
||||
return;
|
||||
end if;
|
||||
|
||||
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
|
||||
@ -234,14 +234,14 @@ package body ALFA is
|
||||
|
||||
begin
|
||||
Count := 1;
|
||||
for S in From .. ALFA_Scope_Table.Last loop
|
||||
for S in From .. Alfa_Scope_Table.Last loop
|
||||
declare
|
||||
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
|
||||
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;
|
||||
Count := Count + 1;
|
||||
|
||||
else
|
||||
@ -249,7 +249,7 @@ package body ALFA is
|
||||
-- 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;
|
||||
end if;
|
||||
end;
|
||||
end loop;
|
||||
@ -260,34 +260,34 @@ package body ALFA is
|
||||
|
||||
begin
|
||||
Snew := From;
|
||||
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
|
||||
|
||||
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;
|
||||
|
||||
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));
|
||||
|
||||
ALFA_File_Table.Append (
|
||||
Alfa_File_Table.Append (
|
||||
(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;
|
||||
|
||||
--------------------
|
||||
-- Add_ALFA_Scope --
|
||||
-- Add_Alfa_Scope --
|
||||
--------------------
|
||||
|
||||
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;
|
||||
@ -344,7 +344,7 @@ package body ALFA is
|
||||
-- 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,
|
||||
@ -356,13 +356,13 @@ package body ALFA is
|
||||
From_Xref => 1,
|
||||
To_Xref => 0,
|
||||
Scope_Entity => E));
|
||||
end Add_ALFA_Scope;
|
||||
end Add_Alfa_Scope;
|
||||
|
||||
--------------------
|
||||
-- Add_ALFA_Xrefs --
|
||||
-- Add_Alfa_Xrefs --
|
||||
--------------------
|
||||
|
||||
procedure Add_ALFA_Xrefs is
|
||||
procedure Add_Alfa_Xrefs is
|
||||
Cur_Scope_Idx : Scope_Index;
|
||||
From_Xref_Idx : Xref_Index;
|
||||
Cur_Entity : Entity_Id;
|
||||
@ -528,12 +528,12 @@ package body ALFA is
|
||||
|
||||
Heap : Entity_Id;
|
||||
|
||||
-- Start of processing for Add_ALFA_Xrefs
|
||||
-- Start of processing for Add_Alfa_Xrefs
|
||||
|
||||
begin
|
||||
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
|
||||
@ -569,31 +569,31 @@ package body ALFA is
|
||||
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;
|
||||
|
||||
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
|
||||
-- reads in ALFA.
|
||||
-- reads in Alfa.
|
||||
|
||||
-------------------
|
||||
-- Is_ALFA_Scope --
|
||||
-- Is_Alfa_Scope --
|
||||
-------------------
|
||||
|
||||
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;
|
||||
end Is_ALFA_Scope;
|
||||
end Is_Alfa_Scope;
|
||||
|
||||
------------------------
|
||||
-- Is_Global_Constant --
|
||||
@ -612,10 +612,10 @@ package body ALFA is
|
||||
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;
|
||||
@ -686,7 +686,7 @@ package body ALFA is
|
||||
From_Xref_Idx := 1;
|
||||
Cur_Entity := Empty;
|
||||
|
||||
if ALFA_Scope_Table.Last = 0 then
|
||||
if Alfa_Scope_Table.Last = 0 then
|
||||
return;
|
||||
end if;
|
||||
|
||||
@ -701,17 +701,17 @@ package body ALFA is
|
||||
|
||||
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;
|
||||
-- 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;
|
||||
-- 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.
|
||||
|
||||
---------------
|
||||
@ -720,7 +720,7 @@ package body ALFA is
|
||||
|
||||
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;
|
||||
|
||||
---------------------
|
||||
@ -745,8 +745,8 @@ package body ALFA is
|
||||
|
||||
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;
|
||||
@ -766,8 +766,8 @@ package body ALFA is
|
||||
|
||||
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;
|
||||
@ -783,7 +783,7 @@ package body ALFA 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.
|
||||
|
||||
@ -794,16 +794,16 @@ package body ALFA is
|
||||
-- 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 :=
|
||||
From_Xref_Idx;
|
||||
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;
|
||||
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
|
||||
@ -812,7 +812,7 @@ package body ALFA is
|
||||
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),
|
||||
@ -824,7 +824,7 @@ package body ALFA is
|
||||
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),
|
||||
@ -840,23 +840,23 @@ package body ALFA is
|
||||
|
||||
-- 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;
|
||||
|
||||
------------------
|
||||
-- Collect_ALFA --
|
||||
-- Collect_Alfa --
|
||||
------------------
|
||||
|
||||
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);
|
||||
|
||||
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
|
||||
|
||||
@ -865,7 +865,7 @@ package body ALFA is
|
||||
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);
|
||||
end if;
|
||||
end loop;
|
||||
|
||||
@ -884,9 +884,9 @@ package body ALFA is
|
||||
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
|
||||
declare
|
||||
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;
|
||||
@ -894,9 +894,9 @@ package body ALFA is
|
||||
|
||||
-- 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
|
||||
declare
|
||||
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);
|
||||
@ -911,24 +911,24 @@ package body ALFA is
|
||||
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;
|
||||
Srec.Spec_Scope_Num :=
|
||||
ALFA_Scope_Table.Table (Spec_Scope).Scope_Num;
|
||||
Alfa_Scope_Table.Table (Spec_Scope).Scope_Num;
|
||||
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,
|
||||
@ -936,9 +936,9 @@ package body ALFA is
|
||||
N_Package_Declaration,
|
||||
N_Package_Body)
|
||||
then
|
||||
Add_ALFA_Scope (N);
|
||||
Add_Alfa_Scope (N);
|
||||
end if;
|
||||
end Detect_And_Add_ALFA_Scope;
|
||||
end Detect_And_Add_Alfa_Scope;
|
||||
|
||||
-------------------------------------
|
||||
-- Enclosing_Subprogram_Or_Package --
|
||||
@ -1376,4 +1376,4 @@ package body ALFA is
|
||||
(Handled_Statement_Sequence (N), Process, Inside_Stubs);
|
||||
end Traverse_Subprogram_Body;
|
||||
|
||||
end ALFA;
|
||||
end Alfa;
|
||||
|
@ -81,7 +81,7 @@ package body Lib.Xref is
|
||||
-- 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
|
||||
@ -103,10 +103,10 @@ package body Lib.Xref is
|
||||
Table_Name => "Xrefs");
|
||||
|
||||
----------------------
|
||||
-- ALFA Information --
|
||||
-- Alfa Information --
|
||||
----------------------
|
||||
|
||||
package body ALFA is separate;
|
||||
package body Alfa is separate;
|
||||
|
||||
------------------------
|
||||
-- Local Subprograms --
|
||||
@ -865,8 +865,8 @@ package body Lib.Xref is
|
||||
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;
|
||||
|
@ -28,7 +28,7 @@
|
||||
|
||||
with Einfo; use Einfo;
|
||||
with Lib.Util; use Lib.Util;
|
||||
with Put_ALFA;
|
||||
with Put_Alfa;
|
||||
|
||||
package Lib.Xref is
|
||||
|
||||
@ -582,13 +582,13 @@ package Lib.Xref is
|
||||
-- in the pragma is "there".
|
||||
|
||||
----------------------
|
||||
-- ALFA Information --
|
||||
-- Alfa Information --
|
||||
----------------------
|
||||
|
||||
-- This package defines procedures for collecting ALFA information and
|
||||
-- This package defines procedures for collecting Alfa information and
|
||||
-- printing in ALI files.
|
||||
|
||||
package ALFA is
|
||||
package Alfa is
|
||||
|
||||
function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id;
|
||||
-- Return the closest enclosing subprogram of package
|
||||
@ -610,17 +610,17 @@ package Lib.Xref is
|
||||
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
|
||||
-- called ALFA.
|
||||
-- called Alfa.
|
||||
|
||||
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
|
||||
-- routines in Lib.Util.
|
||||
|
||||
end ALFA;
|
||||
end Alfa;
|
||||
|
||||
-----------------
|
||||
-- Subprograms --
|
||||
|
@ -44,7 +44,7 @@ package body Opt is
|
||||
|
||||
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;
|
||||
|
||||
----------------------------------
|
||||
|
@ -1872,14 +1872,14 @@ package Opt is
|
||||
-- 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
|
||||
-- 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);
|
||||
-- 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
|
||||
|
@ -23,15 +23,15 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with ALFA; use ALFA;
|
||||
with Alfa; use Alfa;
|
||||
|
||||
procedure Put_ALFA is
|
||||
procedure Put_Alfa is
|
||||
begin
|
||||
-- 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
|
||||
declare
|
||||
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;
|
||||
|
||||
@ -60,7 +60,7 @@ begin
|
||||
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');
|
||||
@ -98,11 +98,11 @@ begin
|
||||
end;
|
||||
end loop;
|
||||
|
||||
-- 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
|
||||
declare
|
||||
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;
|
||||
@ -121,7 +121,7 @@ begin
|
||||
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;
|
||||
@ -166,8 +166,8 @@ begin
|
||||
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
|
||||
@ -229,4 +229,4 @@ begin
|
||||
end loop;
|
||||
end;
|
||||
end loop;
|
||||
end Put_ALFA;
|
||||
end Put_Alfa;
|
||||
|
@ -23,8 +23,8 @@
|
||||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
-- 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.
|
||||
|
||||
@ -52,7 +52,7 @@ generic
|
||||
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.
|
||||
|
@ -375,12 +375,12 @@ package body Restrict is
|
||||
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.
|
||||
|
||||
if CodePeer_Mode or ALFA_Mode then
|
||||
if CodePeer_Mode or Alfa_Mode then
|
||||
return;
|
||||
end if;
|
||||
|
||||
|
@ -1365,7 +1365,9 @@ package body System.Task_Primitives.Operations is
|
||||
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
|
||||
|
@ -3436,7 +3436,7 @@ package body Sem_Ch12 is
|
||||
or else Might_Inline_Subp)
|
||||
and then not Is_Actual_Pack
|
||||
and then not Inline_Now
|
||||
and then not ALFA_Mode
|
||||
and then not Alfa_Mode
|
||||
and then (Operating_Mode = Generate_Code
|
||||
or else (Operating_Mode = Check_Semantics
|
||||
and then ASIS_Mode));
|
||||
|
@ -2009,10 +2009,10 @@ package body Sem_Ch13 is
|
||||
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
|
||||
-- contexts).
|
||||
|
||||
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
|
||||
@ -2032,7 +2032,7 @@ package body Sem_Ch13 is
|
||||
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
|
||||
|
@ -19722,7 +19722,7 @@ package body Sem_Ch3 is
|
||||
-- and First_Rep_Item info, which should not be relied upon in formal
|
||||
-- verification.
|
||||
|
||||
if ALFA_Mode then
|
||||
if Alfa_Mode then
|
||||
|
||||
-- If the range of the type is already symmetric with a possible
|
||||
-- extra negative value, leave it this way.
|
||||
|
@ -1763,8 +1763,8 @@ package body Sem_Ch4 is
|
||||
-- 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);
|
||||
end if;
|
||||
|
||||
Analyze (P);
|
||||
|
@ -2023,7 +2023,7 @@ package body Sem_Ch5 is
|
||||
|
||||
if Nkind (D_Copy) = N_Function_Call
|
||||
or else
|
||||
(ALFA_Mode
|
||||
(Alfa_Mode
|
||||
and then (Nkind (D_Copy) = N_Attribute_Reference
|
||||
and then
|
||||
(Attribute_Name (D_Copy) = Name_Result
|
||||
|
@ -978,7 +978,7 @@ package body Sem_Ch6 is
|
||||
-- than inserted in the code, in order to facilitate a distinct
|
||||
-- treatment for them.
|
||||
|
||||
if not ALFA_Mode then
|
||||
if not Alfa_Mode then
|
||||
Process_PPCs (N, Gen_Id, Body_Id);
|
||||
end if;
|
||||
|
||||
@ -2699,7 +2699,7 @@ package body Sem_Ch6 is
|
||||
-- than inserted in the code, in order to facilitate a distinct
|
||||
-- treatment for them.
|
||||
|
||||
if not ALFA_Mode then
|
||||
if not Alfa_Mode then
|
||||
Process_PPCs (N, Spec_Id, Body_Id);
|
||||
end if;
|
||||
|
||||
|
@ -2022,7 +2022,7 @@ package body Sem_Ch8 is
|
||||
-- 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;
|
||||
|
@ -1877,7 +1877,7 @@ package body Sem_Prag is
|
||||
-- In formal verification mode, analyze pragma expression for
|
||||
-- correctness, as it is not expanded later.
|
||||
|
||||
if ALFA_Mode then
|
||||
if Alfa_Mode then
|
||||
Analyze_PPC_In_Decl_Part
|
||||
(N, Defining_Entity (Unit (Parent (Parent (N)))));
|
||||
end if;
|
||||
@ -5090,9 +5090,9 @@ package body Sem_Prag is
|
||||
-- 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
|
||||
return;
|
||||
end if;
|
||||
|
||||
@ -5314,11 +5314,11 @@ package body Sem_Prag is
|
||||
-- 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
|
||||
|
||||
if (CodePeer_Mode or ALFA_Mode)
|
||||
if (CodePeer_Mode or Alfa_Mode)
|
||||
and then Comes_From_Source (N)
|
||||
then
|
||||
return;
|
||||
@ -9501,11 +9501,11 @@ package body Sem_Prag is
|
||||
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)
|
||||
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;
|
||||
@ -9532,10 +9532,10 @@ package body Sem_Prag is
|
||||
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.
|
||||
|
||||
if not (CodePeer_Mode or ALFA_Mode) then
|
||||
if not (CodePeer_Mode or Alfa_Mode) then
|
||||
Process_Inline (True);
|
||||
end if;
|
||||
|
||||
@ -10975,10 +10975,10 @@ package body Sem_Prag is
|
||||
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
|
||||
-- in these modes.
|
||||
|
||||
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;
|
||||
@ -11347,7 +11347,7 @@ package body Sem_Prag is
|
||||
-- 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
|
||||
|
@ -4006,12 +4006,12 @@ package body Sem_Res is
|
||||
|
||||
-- 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
|
||||
and then not ALFA_Mode
|
||||
and then not Alfa_Mode
|
||||
then
|
||||
Set_Entity (Selector_Name (Parent (A)), F);
|
||||
Generate_Reference (F, Selector_Name (Parent (A)));
|
||||
@ -8083,7 +8083,7 @@ package body Sem_Res is
|
||||
|
||||
procedure Resolve_Quantified_Expression (N : Node_Id; Typ : Entity_Id) is
|
||||
begin
|
||||
if not ALFA_Mode then
|
||||
if not Alfa_Mode then
|
||||
|
||||
-- If expansion is enabled, analysis is delayed until the expresssion
|
||||
-- is rewritten as a loop.
|
||||
@ -8101,7 +8101,7 @@ package body Sem_Res is
|
||||
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
|
||||
|
@ -10632,8 +10632,8 @@ package body Sem_Util is
|
||||
-- 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
|
||||
|
Loading…
Reference in New Issue
Block a user