2011-08-05 Robert Dewar <dewar@adacore.com>

[pf3gnuchains/gcc-fork.git] / gcc / ada / opt.ads

diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index b05dda4..a9c2d9f 100644 (file)
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 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- --
@@ -112,10 +112,6 @@ package Opt is
    --  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,
@@ -328,7 +324,7 @@ package Opt is
    --  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...).
 
@@ -378,6 +374,10 @@ package Opt is
    --  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
@@ -606,6 +606,10 @@ package Opt is
    --  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
@@ -1661,6 +1665,11 @@ package Opt is
    --  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
@@ -1718,11 +1727,6 @@ package Opt is
    --  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
@@ -1864,31 +1868,16 @@ package Opt is
    --  Used to store the ASIS version number read from a tree file to check if
    --  it is the same as stored in the ASIS version number in Tree_IO.
 
-   -----------------------------------
-   -- Modes for Formal Verification --
-   -----------------------------------
-
-   --  These modes are currently defined through debug flags
+   ----------------------------------
+   -- Mode for Formal Verification --
+   ----------------------------------
 
-   Formal_Verification_Mode : Boolean := False;
-   --  Set True if ALFA_Mode or SPARK_Mode
+   --  This mode is currently defined through a debug flag
 
    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.
+   --  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.
 
 private
 
@@ -1905,6 +1894,7 @@ 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;
@@ -1913,8 +1903,8 @@ private
       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;