-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Ada_Version_Explicit : Ada_Version_Type := Ada_Version_Default;
-- GNAT
- -- Like Ada_Version, but does not get set implicitly for predefined
- -- or internal units, so it reflects the Ada version explicitly set
- -- using configuration pragmas or compiler switches (or if neither
- -- appears, it remains set to Ada_Version_Default). This is used in
- -- the rare cases (notably for pragmas Preelaborate_05 and Pure_05/12)
- -- where in the run-time we want the explicit version set.
+ -- Like Ada_Version, but does not get set implicitly for predefined or
+ -- internal units, so it reflects the Ada version explicitly set using
+ -- configuration pragmas or compiler switches (or if neither appears, it
+ -- remains set to Ada_Version_Default). This is used in the rare cases
+ -- (notably pragma Obsolescent) where we want the explicit version set.
Ada_Version_Runtime : Ada_Version_Type := Ada_2012;
-- GNAT
-- also repeated error messages for references to undefined identifiers
-- and certain other repeated error messages. Set by use of -gnatf.
+ Allow_Integer_Address : Boolean := False;
+ -- GNAT
+ -- Allow use of integer expression in a context requiring System.Address.
+ -- Set by the use of configuration pragma Allow_Integer_Address Also set
+ -- in relaxed semantics mode for use by CodePeer or when -gnatd.M is used.
+
All_Sources : Boolean := False;
-- GNATBIND
-- Set to True to require all source files to be present. This flag is
CodePeer_Mode : Boolean := False;
-- GNAT, GNATBIND, GPRBUILD
-- Enable full CodePeer mode (SCIL generation, disable switches that
- -- interact badly with it, etc...).
+ -- interact badly with it, etc...). This is turned on by -gnatC.
Commands_To_Stdout : Boolean := False;
-- GNATMAKE
-- set to True to delete only the files produced by the compiler but not
-- the library files or the executable files.
+ Compiler_Unit : Boolean := False;
+ -- GNAT1
+ -- Set True by an occurrence of pragma Compiler_Unit_Warning (or of the
+ -- obsolete pragma Compiler_Unit) in the main unit. Once set True, stays
+ -- True, since any units that are with'ed directly or indirectly by
+ -- a Compiler_Unit_Warning main unit are subject to the same restrictions.
+ -- Such units really should have their own pragmas, but we do not bother to
+ -- check for that, so this transitivity provides extra checking.
+
Config_File : Boolean := True;
-- GNAT
-- Set to False to inhibit reading and processing of gnat.adc file
-- to trigger the activation of the remote debugging interface.
-- Is this still true ???
+ Default_Exit_Status : Int := 0;
+ -- GNATBIND
+ -- Set the default exit status value. Set by the -Xnnn switch for the
+ -- binder.
+
Debug_Generated_Code : Boolean := False;
-- GNAT
-- Set True (-gnatD switch) to debug generated expanded code instead
-- of the original source code. Causes debugging information to be
-- written with respect to the generated code file that is written.
- Default_Exit_Status : Int := 0;
- -- GNATBIND
- -- Set the default exit status value. Set by the -Xnnn switch for the
- -- binder.
-
+ Default_Pool : Node_Id := Empty;
+ -- GNAT
+ -- Used to record the storage pool name (or null literal) that is the
+ -- argument of an applicable pragma Default_Storage_Pool.
+ -- Empty: No pragma Default_Storage_Pool applies.
+ -- N_Null node: "pragma Default_Storage_Pool (null);" applies.
+ -- otherwise: "pragma Default_Storage_Pool (X);" applies, and
+ -- this points to the name X.
+ -- Push_Scope and Pop_Scope in Sem_Ch8 save and restore this value.
Default_Stack_Size : Int := -1;
-- GNATBIND
-- Set to default primary stack size in units of bytes. Set by
-- default was set by the binder, and that the default should be the
-- initial value of System.Secondary_Stack.Default_Secondary_Stack_Size.
- Default_Pool : Node_Id := Empty;
+ Default_SSO : Character := ' ';
-- GNAT
- -- Used to record the storage pool name (or null literal) that is the
- -- argument of an applicable pragma Default_Storage_Pool.
- -- Empty: No pragma Default_Storage_Pool applies.
- -- N_Null node: "pragma Default_Storage_Pool (null);" applies.
- -- otherwise: "pragma Default_Storage_Pool (X);" applies, and
- -- this points to the name X.
- -- Push_Scope and Pop_Scope in Sem_Ch8 save and restore this value.
+ -- Set if a pragma Default_Scalar_Storage_Order has been given. The value
+ -- of ' ' indicates that no default has been set, otherwise the value is
+ -- either 'H' for High_Order_First or 'L' for Lower_Order_First.
Detect_Blocking : Boolean := False;
-- GNAT
Do_Not_Execute : Boolean := False;
-- GNATMAKE
- -- Set to True if no actual compilations should be undertaken.
+ -- Set to True if no actual compilations should be undertaken
Dump_Source_Text : Boolean := False;
-- GNAT
-- GNATBIND
-- Set to True to output chosen elaboration order
+ Elab_Info_Messages : Boolean := False;
+ -- GNAT
+ -- Set to True to output info messages for static elabmodel (-gnatel)
+
Elab_Warnings : Boolean := False;
-- GNAT
- -- Set to True to generate full elaboration warnings (-gnatwl)
+ -- Set to True to generate elaboration warnings (-gnatwl)
Error_Msg_Line_Length : Nat := 0;
-- GNAT
-- the name is of the form .xxx, then to name.xxx where name is the source
-- file name with extension stripped.
+ Generate_CodePeer_Messages : Boolean := False;
+ -- GNAT
+ -- Generate CodePeer messages. Ignored if CodePeer_Mode is false.
+ -- This is turned on by -gnateC.
+
Generate_Processed_File : Boolean := False;
-- GNAT
-- True when switch -gnateG is used. When True, create in a file
-- GNAT
-- This variable indicates the character set to be used for identifiers.
-- The possible settings are:
- -- '1' Latin-5 (ISO-8859-1)
- -- '2' Latin-5 (ISO-8859-2)
- -- '3' Latin-5 (ISO-8859-3)
- -- '4' Latin-5 (ISO-8859-4)
- -- '5' Latin-5 (ISO-8859-5, Cyrillic)
- -- '9' Latin-5 (ISO-8859-9)
+ -- '1' Latin-1 (ISO-8859-1)
+ -- '2' Latin-2 (ISO-8859-2)
+ -- '3' Latin-3 (ISO-8859-3)
+ -- '4' Latin-4 (ISO-8859-4)
+ -- '5' Latin-Cyrillic (ISO-8859-5)
+ -- '9' Latin-9 (ISO-8859-15)
-- 'p' PC (US, IBM page 437)
-- '8' PC (European, IBM page 850)
-- 'f' Full upper set (all distinct)
Init_Or_Norm_Scalars : Boolean := False;
-- GNAT, GANTBIND
-- Set True if a pragma Initialize_Scalars applies to the current unit.
- -- Also set True if a pragma Normalize_Scalars applies.
+ -- Also set True if a pragma Restriction (Normalize_Scalars) applies.
Initialize_Scalars : Boolean := False;
-- GNAT
List_Closure : Boolean := False;
-- GNATBIND
- -- List all sources in the closure of a main (-R gnatbind switch)
+ -- List all sources in the closure of a main (-R or -Ra gnatbind switch)
+
+ List_Closure_All : Boolean := False;
+ -- GNATBIND
+ -- List all sources in closure of main including run-time units (-Ra
+ -- gnatbind switch).
List_Dependencies : Boolean := False;
-- GNATMAKE
-- GNATMAKE
-- Set to True if minimal recompilation mode requested
+ Modify_Tree_For_C : Boolean := False;
+ -- GNAT
+ -- If this switch is set True (currently it is set only by -gnatd.V), then
+ -- certain meaning-preserving transformations are applied to the tree to
+ -- make it easier to interface with back ends that implement C semantics.
+ -- There is a section in Sinfo which describes the transformations made.
+
Multiple_Unit_Index : Int := 0;
-- GNAT
-- This is set non-zero if the current unit is being compiled in multiple
No_Backup : Boolean := False;
-- GNATNAME
- -- Set by switch --no-backup.
- -- Do not create backup copies of project files.
+ -- Do not create backup copies of project files. Set by switch --no-backup.
No_Deletion : Boolean := False;
-- GNATPREP
No_Split_Units : Boolean := False;
-- GPRBUILD
-- Set to True with switch --no-split-units. When True, unit sources, spec,
- -- body and subunits, must all be in the same project.This is checked after
- -- each compilation.
+ -- body and subunits, must all be in the same project. This is checked
+ -- after each compilation.
No_Stdinc : Boolean := False;
-- GNAT, GNATBIND, GNATMAKE, GNATFIND, GNATXREF
- -- Set to True if no default source search dirs added to search list
+ -- Set to True if no default source search dirs added to search list.
No_Stdlib : Boolean := False;
-- GNATMAKE, GNATBIND, GNATFIND, GNATXREF
- -- Set to True if no default library search dirs added to search list
+ -- Set to True if no default library search dirs added to search list.
No_Strict_Aliasing : Boolean := False;
-- GNAT
- -- Set True if pragma No_Strict_Aliasing with no parameters encountered
+ -- Set True if pragma No_Strict_Aliasing with no parameters encountered.
Normalize_Scalars : Boolean := False;
-- GNAT, GNATBIND
-- object directory, if project files are used.
type Operating_Mode_Type is (Check_Syntax, Check_Semantics, Generate_Code);
+ pragma Ordered (Operating_Mode_Type);
Operating_Mode : Operating_Mode_Type := Generate_Code;
-- GNAT
-- Indicates the operating mode of the compiler. The default is generate
-- only mode. Operating_Mode can also be modified as a result of detecting
-- errors during the compilation process. In particular if any serious
-- error is detected then this flag is reset from Generate_Code to
- -- Check_Semantics after generating an error message.
+ -- Check_Semantics after generating an error message. This is an ordered
+ -- type with the semantics that each value does more than the previous one.
Optimize_Alignment : Character := 'O';
-- Setting of Optimize_Alignment, set to T/S/O for time/space/off. Can
Replace_In_Comments : Boolean := False;
-- GNATPREP
- -- Set to True if -C switch used
+ -- Set to True if -C switch used.
RTS_Lib_Path_Name : String_Ptr := null;
RTS_Src_Path_Name : String_Ptr := null;
-- GNAT
-- Set True if a pragma Short_Descriptors applies to the current unit.
+ type SPARK_Mode_Type is (None, Off, On);
+ -- Possible legal modes that can be set by aspect/pragma SPARK_Mode, as
+ -- well as the value None, which indicates no such pragma/aspect applies.
+
+ SPARK_Mode : SPARK_Mode_Type := None;
+ -- GNAT
+ -- Current SPARK mode setting.
+
+ SPARK_Mode_Pragma : Node_Id := Empty;
+ -- GNAT
+ -- If the current SPARK_Mode (above) was set by a pragma, this records
+ -- the pragma that set this mode.
+
+ SPARK_Switches_File_Name : String_Ptr := null;
+ -- GNAT
+ -- Set to non-null file name by use of the -gnates switch to specify
+ -- SPARK (gnat2why) specific switches in the given file name.
+
Special_Exception_Package_Used : Boolean := False;
-- GNAT
-- Set to True if either of the unit GNAT.Most_Recent_Exception or
Sprint_Line_Limit : Nat := 72;
-- GNAT
- -- Limit values for chopping long lines in Sprint output, can be reset
- -- by use of NNN parameter with -gnatG or -gnatD switches.
+ -- Limit values for chopping long lines in Cprint/Sprint output, can be
+ -- reset by use of NNN parameter with -gnatG or -gnatD switches.
- Stack_Checking_Enabled : Boolean;
+ Stack_Checking_Enabled : Boolean := False;
-- GNAT
- -- Set to indicate if -fstack-check switch is set for the compilation. True
- -- means that the switch is set, so that stack checking is enabled. False
- -- means that the switch is not set (no stack checking). This value is
- -- obtained from the external imported value flag_stack_check in the gcc
- -- backend (see Frontend) and may be referenced throughout the compilation
- -- phases.
+ -- Set to indicate if stack checking is enabled for the compilation. This
+ -- is set directly from the value in the gcc back end in the body of the
+ -- gcc version of back_end.adb.
Style_Check : Boolean := False;
-- GNAT
-- initialized by Osint.Initialize, and further initialized by the
-- Adjust_Global_Switches flag in Gnat1drv.
- Suppress_Back_Annotation : Boolean := False;
- -- GNAT
- -- This flag is set True if back annotation of representation information
- -- is to be suppressed. This is set if neither -gnatt or -gnatR0-3 is set.
- -- This avoids unnecessary time being spent on back annotation.
-
Table_Factor : Int := 1;
-- GNAT
-- Factor by which all initial table sizes set in Alloc are multiplied.
Treat_Categorization_Errors_As_Warnings : Boolean := False;
-- Normally categorization errors are true illegalities. If this switch
-- is set, then such errors result in warning messages rather than error
- -- messages. Set True by -gnateP (P for Pure/Preelaborate).
+ -- messages. Set True by -gnateP (P for Pure/Preelaborate). Also set in
+ -- Relaxed_RM_Semantics mode since some old Ada 83 compilers treated
+ -- pragma Preelaborate differently.
Treat_Restrictions_As_Warnings : Boolean := False;
-- GNAT
-- file for the compiler. Indicates that while preprocessing sources,
-- symbols that are not defined have the value FALSE.
+ Uneval_Old : Character := 'E';
+ -- GNAT
+ -- Set to 'E'/'W'/'A' for use of Error/Warn/Allow in a valid pragma
+ -- Unevaluated_Use_Of_Old.
+
Unique_Error_Tag : Boolean := Tag_Errors;
-- GNAT
-- Indicates if error messages are to be prefixed by the string error:
-- GNAT
-- Set to True to generate warnings for use of Pragma Warnings (Off, ent),
-- where either the pragma is never used, or it could be replaced by a
- -- pragma Unmodified or Unreferenced. Modified by use of -gnatw.w/.W.
+ -- pragma Unmodified or Unreferenced. Also generates warnings for pragma
+ -- Warning (Off, string) which either has no matching pragma Warning On,
+ -- or where no warning has been suppressed by the use of the pragma.
+ -- Modified by use of -gnatw.w/.W.
type Warning_Mode_Type is (Suppress, Normal, Treat_As_Error);
Warning_Mode : Warning_Mode_Type := Normal;
-- GNAT, GNATBIND
-- Controls treatment of warning messages. If set to Suppress, warning
-- messages are not generated at all. In Normal mode, they are generated
- -- but do not count as errors. In Treat_As_Error mode, warning messages
- -- are generated and are treated as errors.
+ -- but do not count as errors. In Treat_As_Error mode, warning messages are
+ -- generated and are treated as errors. Note that Warning_Mode = Suppress
+ -- causes pragma Warnings to be ignored (except for legality checks),
+ -- unless we are in GNATprove_Mode, which requires pragma Warnings to
+ -- be stored for the formal verification backend.
+
+ Warnings_As_Errors_Count : Natural;
+ -- GNAT
+ -- Number of entries stored in Warnings_As_Errors table
Wide_Character_Encoding_Method : WC_Encoding_Method := WCEM_Brackets;
-- GNAT, GNATBIND
-- These are settings that are used to establish the mode at the start of
-- each unit. The values defined below can be affected either by command
-- line switches, or by the use of appropriate configuration pragmas in a
- -- configuration pragma file.
+ -- configuration pragma file (but NOT by a local use of a configuration
+ -- pragma in a single file).
Ada_Version_Config : Ada_Version_Type;
-- GNAT
-- Same as Default_Pool above, except this is only for Default_Storage_Pool
-- pragmas that are configuration pragmas.
+ Default_SSO_Config : Character := ' ';
+ -- GNAT
+ -- Set if a pragma Default_Scalar_Storage_Order appears as a configuration
+ -- pragma. A value of ' ' means that no pragma was given, otherwise the
+ -- value is 'H' for High_Order_First or 'L' for Low_Order_First.
+
Dynamic_Elaboration_Checks_Config : Boolean := False;
-- GNAT
-- Set True for dynamic elaboration checking mode, as set by the -gnatE
-- This flag is used to set the initial value for Short_Descriptors at the
-- start of analyzing each unit.
+ SPARK_Mode_Config : SPARK_Mode_Type := None;
+ -- GNAT
+ -- The setting of SPARK_Mode from configuration pragmas
+
+ SPARK_Mode_Pragma_Config : Node_Id := Empty;
+ -- If a SPARK_Mode pragma appeared in the configuration pragmas (setting
+ -- SPARK_Mode_Config appropriately), then this points to the N_Pragma node.
+
+ Uneval_Old_Config : Character;
+ -- GNAT
+ -- The setting of Uneval_Old from configuration pragmas
+
Use_VADS_Size_Config : Boolean;
-- GNAT
-- This is the value of the configuration switch that controls the use of
-- is ignored for internal and predefined units (which are always compiled
-- with the standard Size semantics).
+ Warnings_As_Errors_Count_Config : Natural;
+ -- GNAT
+ -- Count of pattern strings stored from Warning_As_Error pragmas
+
type Config_Switches_Type is private;
-- Type used to save values of the switches set from Config values
-- This procedure sets the switches to the appropriate initial values. The
-- parameter Internal_Unit is True for an internal or predefined unit, and
-- affects the way the switches are set (see above). Main_Unit is true if
- -- switches are being set for the main unit (this affects setting of the
- -- assert/debug pragma switches, which are normally set false by default
- -- for an internal unit, except when the internal unit is the main unit,
- -- in which case we use the command line settings).
+ -- switches are being set for the main unit or for the spec of the main
+ -- unit. This affects setting of the assert/debug pragma switches, which
+ -- are normally set false by default for an internal unit, except when the
+ -- internal unit is the main unit, in which case we use the command line
+ -- settings).
procedure Restore_Opt_Config_Switches (Save : Config_Switches_Type);
-- This procedure restores a set of switch values previously saved by a
- -- call to Save_Opt_Switches.
+ -- call to Save_Opt_Config_Switches (Save).
procedure Register_Opt_Config_Switches;
-- This procedure is called after processing the gnat.adc file and other
-- this flag, see package Expander. Indeed this flag might more logically
-- be in the spec of Expander, but it is referenced by Errout, and it
-- really seems wrong for Errout to depend on Expander.
- --
- -- Note: for many purposes, it is more appropriate to test the flag
- -- Full_Expander_Active, which also checks that SPARK mode is not active.
Static_Dispatch_Tables : Boolean := True;
-- This flag indicates if the backend supports generation of statically
-- Modes for Formal Verification --
-----------------------------------
- Frame_Condition_Mode : Boolean := False;
- -- Specific mode to be used in combination with SPARK_Mode. If set to
- -- true, ALI files containing the frame conditions (global effects) are
- -- generated, and Why files are *not* generated. If not true, Why files
- -- are generated. Set by debug flag -gnatd.G.
-
- Formal_Extensions : Boolean := False;
- -- When this flag is set, new aspects/pragmas/attributes are accepted,
- -- whose main purpose is to facilitate formal verification. Set by debug
- -- flag -gnatd.V.
-
- Global_SPARK_Mode : SPARK_Mode_Id := None;
- -- The mode applicable to the whole compilation. The global mode can be set
- -- in a configuration file such as gnat.adc.
-
- SPARK_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 SPARK 2014 subset of Ada. Set True by the gnat2why executable or by
- -- use of the -gnatd.F debug switch. Note that this is completely separate
- -- from the SPARK restriction defined in GNAT to detect violations of a
- -- subset of SPARK 2005 rules.
-
- SPARK_Strict_Mode : Boolean := False;
- -- Interpret compiler permissions as strictly as possible. E.g. base ranges
- -- for integers are limited to the strict minimum with this option. Set by
- -- debug flag -gnatd.D.
-
- function Full_Expander_Active return Boolean;
- pragma Inline (Full_Expander_Active);
- -- Returns the value of (Expander_Active and not SPARK_Mode). This "flag"
- -- indicates that expansion is fully active, that is, not in the reduced
- -- mode for SPARK (True) or that expansion is either deactivated, or active
- -- in the reduced mode for SPARK (False). For more information on full
- -- expansion, see package Expander. For more information on reduced
- -- SPARK expansion, see package Exp_SPARK.
+ GNATprove_Mode : Boolean := False;
+ -- Specific compiling mode targeting formal verification for those parts
+ -- of the input code that belong to the SPARK 2014 subset of Ada. Set True
+ -- by the gnat2why executable or by use of the -gnatd.F debug switch. Note
+ -- that this is completely separate from the SPARK restriction defined in
+ -- GNAT to detect violations of a subset of SPARK 2005 rules.
+
+ ---------------------------
+ -- Error/Warning Control --
+ ---------------------------
+
+ -- The following array would more reasonably be located in Err_Vars or
+ -- Errour, but but we put them here to deal with licensing issues (we need
+ -- this to have the GPL exception licensing, since these variables and
+ -- subprograms are accessed from units with this licensing).
+
+ Warnings_As_Errors : array (1 .. 10_000) of String_Ptr;
+ -- Table for recording Warning_As_Error pragmas as they are processed.
+ -- It would be nicer to use Table, but there are circular elaboration
+ -- problems if we try to do this, and an attempt to find some other
+ -- appropriately licensed unit to declare this as a Table failed with
+ -- various elaboration circularities. Memory is getting cheap these days!
+
+ --------------------------
+ -- Private Declarations --
+ --------------------------
private
Check_Float_Overflow : Boolean;
Check_Policy_List : Node_Id;
Default_Pool : Node_Id;
+ Default_SSO : Character;
Dynamic_Elaboration_Checks : Boolean;
Exception_Locations_Suppressed : Boolean;
Extensions_Allowed : Boolean;
Persistent_BSS_Mode : Boolean;
Polling_Required : Boolean;
Short_Descriptors : Boolean;
+ SPARK_Mode : SPARK_Mode_Type;
+ SPARK_Mode_Pragma : Node_Id;
+ Uneval_Old : Character;
Use_VADS_Size : Boolean;
+ Warnings_As_Errors_Count : Natural;
end record;
-- The following declarations are for GCC version dependent flags. We do
projects / gcc.git / blobdiff