2012-10-31 Basile Starynkevitch <basile@starynkevitch.net>

	MELT branch merged with trunk rev 193029 using svnmerge.py



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/branches/melt-branch@193030 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 17 insertions, 0 deletions

diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 88194b3023b..9221be94e04 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1085,6 +1085,18 @@ package Opt is
    --  True if output of list of objects is requested (-O switch set). List is
    --  output under the given filename, or standard output if not specified.
 
+   Partition_Elaboration_Policy : Character := ' ';
+   --  GNAT, GNATBIND
+   --  Set to ' ' for the default case (no elaboration policy specified). Reset
+   --  to first character (uppercase) of locking policy name if a valid pragma
+   --  Partition_Elaboration_Policy is encountered.
+
+   Partition_Elaboration_Policy_Sloc : Source_Ptr := No_Location;
+   --  GNAT, GNATBIND
+   --  Remember location of previous Partition_Elaboration_Policy pragma. This
+   --  is used for inconsistency error messages. A value of System_Location is
+   --  used if the policy is set in package System.
+
    Persistent_BSS_Mode : Boolean := False;
    --  GNAT
    --  True if a Persistent_BSS configuration pragma is in effect, causing
@@ -1924,6 +1936,11 @@ package Opt is
    --  for integers are limited to the strict minimum with this option. Set by
    --  debug flag -gnatd.D.
 
+   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.
+
    function Full_Expander_Active return Boolean;
    pragma Inline (Full_Expander_Active);
    --  Returns the value of (Expander_Active and not Alfa_Mode). This "flag"