[multiple changes]

2014-01-20  Ed Schonberg  <schonberg@adacore.com>

	* sem_attr.adb: Code and comments cleanup.

2014-01-20  Yannick Moy  <moy@adacore.com>

	* debug.adb Free debug flags -gnatd.D, -gnatd.G and -gnatd.V *
	* errout.adb (Compilation_Errors): Remove special handling in
	GNATprove mode.
	* gnat1drv.adb (Adjust_Global_Switches): Remove handling of the
	removed debug flags.
	* gnat_rm.texi: Initial documentation for Abstract_State, Depends,
	Global, Initial_Condition, Initializes and Refined_State pragmas and
	aspects.
	* opt.ads (Frame_Condition_Mode, Formal_Extensions,
	SPARK_Strict_Mode): Remove global flags.
	* sem_ch3.adb (Analyze_Object_Declaration): Check of no hidden state
	always performed now, on packages declaring a null state.
	(Signed_Integer_Type_Declaration): Remove ill-designed attempt
	at providing pedantic mode for bounds of integer types.
	* sem_ch4.adb (Analyze_Quantified_Expression): Warning on suspicious
	"some" quantified expression now issued under control of -gnatw.t,
	like the other warning on unused bound variable.
	* sem_prag.adb (Check_Precondition_Postcondition): Remove useless test
	on removed flag.
	(Analyze_Pragma): Remove tests for SPARK 2014
	pragmas, not officially allowed by GNAT.

From-SVN: r206837

1 files changed, 6 insertions, 19 deletions

diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index bb98c5c..4cc8feb 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -121,10 +121,10 @@ package body Debug is
    --  d.A  Read/write Aspect_Specifications hash table to tree
    --  d.B
    --  d.C  Generate concatenation call, do not generate inline code
-   --  d.D  SPARK strict mode
+   --  d.D
    --  d.E  Turn selected errors into warnings
-   --  d.F  SPARK mode
-   --  d.G  Frame condition mode for gnat2why
+   --  d.F  Debug mode for GNATprove
+   --  d.G
    --  d.H
    --  d.I  Do not ignore enum representation clauses in CodePeer mode
    --  d.J  Disable parallel SCIL generation mode
@@ -139,7 +139,7 @@ package body Debug is
    --  d.S  Force Optimize_Alignment (Space)
    --  d.T  Force Optimize_Alignment (Time)
    --  d.U  Ignore indirect calls for static elaboration
-   --  d.V  Extensions for formal verification
+   --  d.V
    --  d.W  Print out debugging information for Walk_Library_Items
    --  d.X
    --  d.Y
@@ -594,21 +594,12 @@ 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.D  SPARK strict mode. Interpret compiler permissions as strictly as
-   --       possible in SPARK mode.
-
    --  d.E  Turn selected errors into warnings. This debug switch causes a
    --       specific set of error messages into warnings. Setting this switch
    --       causes Opt.Error_To_Warning to be set to True.
 
-   --  d.F  SPARK 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. Note that ALI files
-   --       are only written when option d.G is also given.
-
-   --  d.G  Frame condition mode for gnat2why. In this mode, gnat2why will
-   --       generate ALI files with an extra section which contains the effects
-   --       of subprograms.
+   --  d.F  Sets GNATprove_Mode to True. This allows debugging the frontend in
+   --       the special mode used by GNATprove.
 
    --  d.I  Do not ignore enum representation clauses in CodePeer mode.
    --       The default of ignoring representation clauses for enumeration
@@ -657,10 +648,6 @@ package body Debug is
    --       reverts to the behavior of earlier compilers, which ignored
    --       indirect calls.
 
-   --  d.V  Extensions for formal verification. New attributes/aspects/pragmas
-   --       defined in GNAT for formal verification with the tool GNATprove are
-   --       only accepted under this switch.
-
    --  d.W  Print out debugging information for Walk_Library_Items, including
    --       the order in which units are walked. This is primarily for use in
    --       debugging CodePeer mode.