-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- case of some binder variables, Gnatbind.Scan_Bind_Arg may modify
-- the default values.
- Ada_Bind_File : Boolean := True;
- -- GNATBIND, GNATLINK
- -- Set True if binder file to be generated in Ada rather than C
-
type Ada_Version_Type is (Ada_83, Ada_95, Ada_2005, Ada_2012);
pragma Ordered (Ada_Version_Type);
-- Versions of Ada for Ada_Version below. Note that these are ordered,
-- 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)
+ -- the rare cases (notably for pragmas Preelaborate_05 and Pure_05/12)
-- where in the run-time we want the explicit version set.
Ada_Version_Runtime : Ada_Version_Type := Ada_2012;
-- of withing a package and using none of the entities in the package.
CodePeer_Mode : Boolean := False;
- -- GNAT
+ -- GNAT, GNATBIND
-- Enable full CodePeer mode (SCIL generation, disable switches that
-- interact badly with it, etc...).
-- GNAT
-- Enable debug statements from pragma Debug
+ Debug_Pragmas_Disabled : Boolean := False;
+ -- GNAT
+ -- Debug pragmas completely disabled (no semantic checking)
+
subtype Debug_Level_Value is Nat range 0 .. 3;
Debugger_Level : Debug_Level_Value := 0;
-- GNATBIND
Front_End_Setjmp_Longjmp_Exceptions;
-- GNAT
-- Set to the appropriate value depending on the default as given in
- -- system.ads (ZCX_By_Default, GCC_ZCX_Support). The C convention is there
- -- to make this variable accessible to gigi.
+ -- system.ads (ZCX_By_Default). The C convention is there to make this
+ -- variable accessible to gigi.
Exception_Tracebacks : Boolean := False;
-- GNATBIND
-- Force generation of ALI file even if errors are encountered.
-- Also forces generation of tree file if -gnatt is also set.
+ Disable_ALI_File : Boolean := False;
+ -- GNAT
+ -- Disable generation of ALI file
+
Force_Checking_Of_Elaboration_Flags : Boolean := False;
-- GNATBIND
-- True if binding with forced checking of the elaboration flags
-- Set to True to skip compile and bind steps (except when Bind_Only is
-- set to True).
- List_Inherited_Aspects : Boolean := True;
+ List_Inherited_Aspects : Boolean := False;
-- GNAT
-- List inherited invariants, preconditions, and postconditions from
- -- Invariant'Class, Pre'Class, and Post'Class aspects.
+ -- Invariant'Class, Pre'Class, and Post'Class aspects. Also list inherited
+ -- subtype predicates. Set True by use of -gnatw.l and False by use of
+ -- -gnatw.L.
List_Restrictions : Boolean := False;
-- GNATBIND
-- with literals or S'Length, presumably assuming a lower bound of one. Set
-- False by -gnatwW.
+ Warn_On_Atomic_Synchronization : Boolean := False;
+ -- GNAT
+ -- Set to True to generate information messages for atomic synchronization.
+ -- Set True by use of -gnatw.n.
+
Warn_On_Bad_Fixed_Value : Boolean := False;
-- GNAT
-- Set to True to generate warnings for static fixed-point expression
-- clauses that are affected by non-standard bit-order. The default is
-- that this warning is enabled.
+ Warn_On_Suspicious_Contract : Boolean := False;
+ -- GNAT
+ -- Set to True to generate warnings for suspicious contracts expressed as
+ -- pragmas or aspects precondition and postcondition. The default is that
+ -- this warning is disabled.
+
Warn_On_Suspicious_Modulus_Value : Boolean := True;
-- GNAT
-- Set to True to generate warnings for suspicious modulus values. The
-- GNAT
-- This is the value of the configuration switch for the Ada 83 mode, as
-- set by the command line switches -gnat83/95/05, and possibly modified by
- -- the use of configuration pragmas Ada_83/Ada95/Ada05. This switch is used
- -- to set the initial value for Ada_Version mode at the start of analysis
- -- of a unit. Note however, that the setting of this flag is ignored for
- -- internal and predefined units (which are always compiled in the most up
- -- to date version of Ada).
+ -- the use of configuration pragmas Ada_*. This switch is used to set the
+ -- initial value for Ada_Version mode at the start of analysis of a unit.
+ -- Note however that the setting of this flag is ignored for internal and
+ -- predefined units (which are always compiled in the most up to date
+ -- version of Ada).
Ada_Version_Explicit_Config : Ada_Version_Type;
-- GNAT
-- terminated by Empty. The order is most recently processed first. This
-- list includes only those pragmas in configuration pragma files.
+ Debug_Pragmas_Disabled_Config : Boolean;
+ -- GNAT
+ -- This is the value of the configuration switch for debug pragmas disabled
+ -- mode, as possibly set by use of the configuration pragma Debug_Policy.
+
Debug_Pragmas_Enabled_Config : Boolean;
-- GNAT
-- This is the value of the configuration switch for debug pragmas enabled
-- used to set the initial value of Fast_Math at the start of each new
-- compilation unit.
- Init_Or_Norm_Scalars_Config : Boolean;
- -- GNAT
- -- This is the value of the configuration switch that is set by one
- -- of the pragmas Initialize_Scalars or Normalize_Scalars.
-
Initialize_Scalars_Config : Boolean;
-- GNAT
-- This is the value of the configuration switch that is set by the
-- 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 Alfa mode is not active.
Static_Dispatch_Tables : Boolean := True;
-- This flag indicates if the backend supports generation of statically
-- Modes for Formal Verification --
-----------------------------------
- -- These modes are currently defined through debug flags
-
- Formal_Verification_Mode : Boolean := False;
- -- Set True if ALFA_Mode or SPARK_Mode
-
- ALFA_Mode : Boolean := False;
- -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
-
- ALFA_Through_SPARK_Mode : Boolean := False;
- -- Specific compiling mode targeting formal verification through
- -- the generation of SPARK code for those parts of the input code that
- -- belong to the ALFA subset of Ada. Set by debug flag -gnatd.E.
-
- ALFA_Through_Why_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 debuf flag -gnatd.F.
-
- SPARK_Mode : Boolean := False;
- -- Reject constructs not allowed by SPARK. Set by flag -gnatd.D or
- -- by pragma SPARK_95.
+ 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.
+
+ Strict_Alfa_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 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
+ -- expansion, see package Expander. For more information on reduced
+ -- Alfa expansion, see package Exp_Alfa.
private
Assertions_Enabled : Boolean;
Assume_No_Invalid_Values : Boolean;
Check_Policy_List : Node_Id;
+ Debug_Pragmas_Disabled : Boolean;
Debug_Pragmas_Enabled : Boolean;
Default_Pool : Node_Id;
Dynamic_Elaboration_Checks : Boolean;
External_Name_Exp_Casing : External_Casing_Type;
External_Name_Imp_Casing : External_Casing_Type;
Fast_Math : Boolean;
- Init_Or_Norm_Scalars : Boolean;
Initialize_Scalars : Boolean;
+ Normalize_Scalars : Boolean;
Optimize_Alignment : Character;
Optimize_Alignment_Local : Boolean;
Persistent_BSS_Mode : Boolean;