[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

10 files changed, 128 insertions, 167 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cd17e43..8aa7d60 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,31 @@
+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.
+
 2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_prag.adb (Analyze_Pragma): Ensure that
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.
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 0e69062..78193ff 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -233,15 +233,6 @@ package body Errout is
    begin
       if not Finalize_Called then
          raise Program_Error;
-
-      --  In formal verification mode, errors issued when analyzing code
-      --  are not compilation errors, and should not result in exiting with
-      --  an error status. These errors are handled in the driver of the
-      --  verification process instead.
-
-      elsif GNATprove_Mode and not Frame_Condition_Mode then
-         return False;
-
       else
          return Erroutc.Compilation_Errors;
       end if;
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index bc1de74..fd50632 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -298,12 +298,6 @@ procedure Gnat1drv is
          Treat_Categorization_Errors_As_Warnings := True;
       end if;
 
-      --  Set switches for formal verification mode
-
-      if Debug_Flag_Dot_VV then
-         Formal_Extensions := True;
-      end if;
-
       --  Enable GNATprove_Mode when using -gnatd.F switch
 
       if Debug_Flag_Dot_FF then
@@ -315,24 +309,6 @@ procedure Gnat1drv is
 
       if GNATprove_Mode then
 
-         --  Set strict standard interpretation of compiler permissions
-
-         if Debug_Flag_Dot_DD then
-            SPARK_Strict_Mode := True;
-         end if;
-
-         --  Distinguish between the two modes of gnat2why: frame condition
-         --  generation (generation of ALI files) and analysis (no ALI files
-         --  generated). This is done with the switch -gnatd.G, which activates
-         --  frame condition mode. The other changes in behavior depending on
-         --  this switch are done in gnat2why directly.
-
-         if Debug_Flag_Dot_GG then
-            Frame_Condition_Mode := True;
-         else
-            Opt.Disable_ALI_File := True;
-         end if;
-
          --  Turn off inlining, which would confuse formal verification output
          --  and gain nothing.
 
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 64bfce1..aa47b56 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -98,6 +98,7 @@ About This Guide
 Implementation Defined Pragmas
 
 * Pragma Abort_Defer::
+* Pragma Abstract_State::
 * Pragma Ada_83::
 * Pragma Ada_95::
 * Pragma Ada_05::
@@ -137,6 +138,7 @@ Implementation Defined Pragmas
 * Pragma Debug::
 * Pragma Debug_Policy::
 * Pragma Default_Storage_Pool::
+* Pragma Depends::
 * Pragma Detect_Blocking::
 * Pragma Disable_Atomic_Synchronization::
 * Pragma Dispatching_Domain::
@@ -157,6 +159,7 @@ Implementation Defined Pragmas
 * Pragma Favor_Top_Level::
 * Pragma Finalize_Storage_Only::
 * Pragma Float_Representation::
+* Pragma Global::
 * Pragma Ident::
 * Pragma Implementation_Defined::
 * Pragma Implemented::
@@ -168,7 +171,9 @@ Implementation Defined Pragmas
 * Pragma Import_Valued_Procedure::
 * Pragma Independent::
 * Pragma Independent_Components::
+* Pragma Initial_Condition::
 * Pragma Initialize_Scalars::
+* Pragma Initializes::
 * Pragma Inline_Always::
 * Pragma Inline_Generic::
 * Pragma Interface::
@@ -225,6 +230,7 @@ Implementation Defined Pragmas
 * Pragma Pure_12::
 * Pragma Pure_Function::
 * Pragma Ravenscar::
+* Pragma Refined_State::
 * Pragma Relative_Deadline::
 * Pragma Remote_Access_Type::
 * Pragma Restricted_Run_Time::
@@ -277,7 +283,6 @@ Implementation Defined Aspects
 * Aspect Abstract_State::
 * Aspect Ada_2005::
 * Aspect Ada_2012::
-* Pragma Allow_Integer_Address::
 * Aspect Compiler_Unit::
 * Aspect Contract_Cases::
 * Aspect Depends::
@@ -285,6 +290,8 @@ Implementation Defined Aspects
 * Aspect Dimension_System::
 * Aspect Favor_Top_Level::
 * Aspect Global::
+* Aspect Initial_Condition::
+* Aspect Initializes::
 * Aspect Inline_Always::
 * Aspect Invariant::
 * Aspect Object_Size::
@@ -294,6 +301,7 @@ Implementation Defined Aspects
 * Aspect Pure_05::
 * Aspect Pure_12::
 * Aspect Pure_Function::
+* Aspect Refined_State::
 * Aspect Remote_Access_Type::
 * Aspect Scalar_Storage_Order::
 * Aspect Shared::
@@ -923,6 +931,7 @@ consideration, the use of these pragmas should be minimized.
 
 @menu
 * Pragma Abort_Defer::
+* Pragma Abstract_State::
 * Pragma Ada_83::
 * Pragma Ada_95::
 * Pragma Ada_05::
@@ -962,6 +971,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Debug::
 * Pragma Debug_Policy::
 * Pragma Default_Storage_Pool::
+* Pragma Depends::
 * Pragma Detect_Blocking::
 * Pragma Disable_Atomic_Synchronization::
 * Pragma Dispatching_Domain::
@@ -982,6 +992,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Favor_Top_Level::
 * Pragma Finalize_Storage_Only::
 * Pragma Float_Representation::
+* Pragma Global::
 * Pragma Ident::
 * Pragma Implementation_Defined::
 * Pragma Implemented::
@@ -993,7 +1004,9 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Import_Valued_Procedure::
 * Pragma Independent::
 * Pragma Independent_Components::
+* Pragma Initial_Condition::
 * Pragma Initialize_Scalars::
+* Pragma Initializes::
 * Pragma Inline_Always::
 * Pragma Inline_Generic::
 * Pragma Interface::
@@ -1050,6 +1063,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Pure_12::
 * Pragma Pure_Function::
 * Pragma Ravenscar::
+* Pragma Refined_State::
 * Pragma Relative_Deadline::
 * Pragma Remote_Access_Type::
 * Pragma Restricted_Run_Time::
@@ -1115,6 +1129,13 @@ the effect of deferring aborts for the sequence of statements (but not
 for the declarations or handlers, if any, associated with this statement
 sequence).
 
+@node Pragma Abstract_State
+@unnumberedsec Pragma Abstract_State
+@findex Abstract_State
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.4.
+
 @node Pragma Ada_83
 @unnumberedsec Pragma Ada_83
 @findex Ada_83
@@ -2411,6 +2432,13 @@ This pragma is standard in Ada 2012, but is available in all earlier
 versions of Ada as an implementation-defined pragma.
 See Ada 2012 Reference Manual for details.
 
+@node Pragma Depends
+@unnumberedsec Pragma Depends
+@findex Depends
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 6.1.5.
+
 @node Pragma Detect_Blocking
 @unnumberedsec Pragma Detect_Blocking
 @findex Detect_Blocking
@@ -3188,6 +3216,13 @@ For digits values from 10 to 15, G float format will be used.
 Digits values above 15 are not allowed.
 @end itemize
 
+@node Pragma Global
+@unnumberedsec Pragma Global
+@findex Global
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 6.1.4.
+
 @node Pragma Ident
 @unnumberedsec Pragma Ident
 @findex Ident
@@ -3629,6 +3664,13 @@ manipulate separate components in the composite object. This may place
 constraints on the representation of the object (for instance prohibiting
 tight packing).
 
+@node Pragma Initial_Condition
+@unnumberedsec Pragma Initial_Condition
+@findex Initial_Condition
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.6.
+
 @node Pragma Initialize_Scalars
 @unnumberedsec Pragma Initialize_Scalars
 @findex Initialize_Scalars
@@ -3691,6 +3733,13 @@ of stack required, so it is probably a good idea to turn on stack
 checking (see description of stack checking in the @value{EDITION}
 User's Guide) when using this pragma.
 
+@node Pragma Initializes
+@unnumberedsec Pragma Initializes
+@findex Initializes
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.1.5.
+
 @node Pragma Inline_Always
 @unnumberedsec Pragma Inline_Always
 @findex Inline_Always
@@ -5852,6 +5901,13 @@ pragma Profile (Ravenscar);
 @noindent
 which is the preferred method of setting the @code{Ravenscar} profile.
 
+@node Pragma Refined_State
+@unnumberedsec Pragma Refined_State
+@findex Refined_State
+@noindent
+For the description of this pragma, see SPARK 2014 Reference Manual,
+section 7.2.2.
+
 @node Pragma Relative_Deadline
 @unnumberedsec Pragma Relative_Deadline
 @findex Relative_Deadline
@@ -7508,6 +7564,8 @@ clause.
 * Aspect Dimension_System::
 * Aspect Favor_Top_Level::
 * Aspect Global::
+* Aspect Initial_Condition::
+* Aspect Initializes::
 * Aspect Inline_Always::
 * Aspect Invariant::
 * Aspect Lock_Free::
@@ -7518,6 +7576,7 @@ clause.
 * Aspect Pure_05::
 * Aspect Pure_12::
 * Aspect Pure_Function::
+* Aspect Refined_State::
 * Aspect Remote_Access_Type::
 * Aspect Scalar_Storage_Order::
 * Aspect Shared::
@@ -7674,7 +7733,19 @@ This aspect is equivalent to pragma @code{Favor_Top_Level}.
 @unnumberedsec Aspect Global
 @findex Global
 @noindent
-This aspect is equivalent pragma @code{Global}.
+This aspect is equivalent to pragma @code{Global}.
+
+@node Aspect Initial_Condition
+@unnumberedsec Aspect Initial_Condition
+@findex Initial_Condition
+@noindent
+This aspect is equivalent to pragma @code{Initial_Condition}.
+
+@node Aspect Initializes
+@unnumberedsec Aspect Initializes
+@findex Initializes
+@noindent
+This aspect is equivalent to pragma @code{Initializes}.
 
 @node Aspect Inline_Always
 @unnumberedsec Aspect Inline_Always
@@ -7744,6 +7815,12 @@ This aspect is equivalent to pragma @code{Pure_12}.
 @noindent
 This aspect is equivalent to pragma @code{Pure_Function}.
 
+@node Aspect Refined_State
+@unnumberedsec Aspect Refined_State
+@findex Refined_State
+@noindent
+This aspect is equivalent to pragma @code{Refined_State}.
+
 @node Aspect Remote_Access_Type
 @unnumberedsec Aspect Remote_Access_Type
 @findex Remote_Access_Type
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index ea3dd20..28381bf 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -2001,17 +2001,6 @@ package Opt is
    -- Modes for Formal Verification --
    -----------------------------------
 
-   Frame_Condition_Mode : Boolean := False;
-   --  Specific mode to be used in combination with GNATprove_Mode. If set to
-   --  true, ALI files containing the frame conditions (global effects) are
-   --  generated, and analysis is *not* performed. If not true, analysis is
-   --  performed. 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.
@@ -2023,11 +2012,6 @@ package Opt is
    --  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.
-
 private
 
    --  The following type is used to save and restore settings of switches in
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 1750cc3..e434697 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -3039,12 +3039,12 @@ package body Sem_Attr is
                return;
 
             --  For compatibility with Declib code, treat all prefixes as
-            --  legal, including non-discriminated types.
+            --  legal, including non-discriminated types. This is because
+            --  DECLIB uses the obsolescent interpretation of the attribute,
+            --  and applies it to types as well as to objects, while the
+            --  current definition applies to objects of a discriminated type.
 
-            --  ??? this non-conforming language extension needs documenting
-            --  ??? anyway it should not depend on Extend_System!
-
-            elsif Present (System_Extend_Unit) then
+            elsif OpenVMS_On_Target then
                return;
             end if;
          end if;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index dfdc85c..483e2be 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3911,7 +3911,7 @@ package body Sem_Ch3 is
       --  Verify whether the object declaration introduces an illegal hidden
       --  state within a package subject to a null abstract state.
 
-      if Formal_Extensions and then Ekind (Id) = E_Variable then
+      if Ekind (Id) = E_Variable then
          Check_No_Hidden_State (Id);
       end if;
    end Analyze_Object_Declaration;
@@ -20444,65 +20444,7 @@ package body Sem_Ch3 is
       Set_Ekind          (T, E_Signed_Integer_Subtype);
       Set_Etype          (T, Implicit_Base);
 
-      --  In formal verification mode, restrict the base type's range to the
-      --  minimum allowed by RM 3.5.4, namely the smallest symmetric range
-      --  around zero with a possible extra negative value that contains the
-      --  subtype range. Keep Size, RM_Size and First_Rep_Item info, which
-      --  should not be relied upon in formal verification.
-
-      if SPARK_Strict_Mode then
-         declare
-            Sym_Hi_Val : Uint;
-            Sym_Lo_Val : Uint;
-            Dloc       : constant Source_Ptr := Sloc (Def);
-            Lbound     : Node_Id;
-            Ubound     : Node_Id;
-            Bounds     : Node_Id;
-
-         begin
-            --  If the subtype range is empty, the smallest base type range
-            --  is the symmetric range around zero containing Lo_Val and
-            --  Hi_Val.
-
-            if UI_Gt (Lo_Val, Hi_Val) then
-               Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val));
-               Sym_Lo_Val := UI_Negate (Sym_Hi_Val);
-
-               --  Otherwise, if the subtype range is not empty and Hi_Val has
-               --  the largest absolute value, Hi_Val is non negative and the
-               --  smallest base type range is the symmetric range around zero
-               --  containing Hi_Val.
-
-            elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then
-               Sym_Hi_Val := Hi_Val;
-               Sym_Lo_Val := UI_Negate (Hi_Val);
-
-               --  Otherwise, the subtype range is not empty, Lo_Val has the
-               --  strictly largest absolute value, Lo_Val is negative and the
-               --  smallest base type range is the symmetric range around zero
-               --  with an extra negative value Lo_Val.
-
-            else
-               Sym_Lo_Val := Lo_Val;
-               Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1);
-            end if;
-
-            Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val);
-            Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val);
-            Set_Is_Static_Expression (Lbound);
-            Set_Is_Static_Expression (Ubound);
-            Analyze_And_Resolve (Lbound, Any_Integer);
-            Analyze_And_Resolve (Ubound, Any_Integer);
-
-            Bounds := Make_Range (Dloc, Lbound, Ubound);
-            Set_Etype (Bounds, Base_Typ);
-
-            Set_Scalar_Range (Implicit_Base, Bounds);
-         end;
-
-      else
-         Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
-      end if;
+      Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
 
       Set_Size_Info      (T,                (Implicit_Base));
       Set_First_Rep_Item (T, First_Rep_Item (Implicit_Base));
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index c63d423..1a87557 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -3690,20 +3690,21 @@ package body Sem_Ch4 is
          Error_Msg_N ("?T?unused variable &", Loop_Id);
       end if;
 
-      --  Diagnose a possible misuse of the "some" existential quantifier. When
+      --  Diagnose a possible misuse of the SOME existential quantifier. When
       --  we have a quantified expression of the form:
 
       --    for some X => (if P then Q [else True])
 
-      --  the if expression will not hold and render the quantified expression
-      --  trivially True.
+      --  any value for X that makes P False results in the if expression being
+      --  trivially True, and so also results in the the quantified expression
+      --  being trivially True.
 
-      if Formal_Extensions
+      if Warn_On_Suspicious_Contract
         and then not All_Present (N)
         and then Nkind (Cond) = N_If_Expression
         and then No_Else_Or_Trivial_True (Cond)
       then
-         Error_Msg_N ("?suspicious expression", N);
+         Error_Msg_N ("?T?suspicious expression", N);
          Error_Msg_N ("\\did you mean (for all X ='> (if P then Q))", N);
          Error_Msg_N ("\\or (for some X ='> P and then Q) instead'?", N);
       end if;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 097fb13..9055ba8 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -2998,12 +2998,6 @@ package body Sem_Prag is
       --  Called for all GNAT defined pragmas to check the relevant restriction
       --  (No_Implementation_Pragmas).
 
-      procedure S14_Pragma;
-      --  Called for all pragmas defined for formal verification to check that
-      --  the S14_Extensions flag is set.
-      --  This name needs fixing ??? There is no such thing as an
-      --  "S14_Extensions" flag ???
-
       function Is_Before_First_Decl
         (Pragma_Node : Node_Id;
          Decls       : List_Id) return Boolean;
@@ -4651,7 +4645,7 @@ package body Sem_Prag is
             --  N_Contract node.
 
             if Acts_As_Spec (PO)
-              and then (GNATprove_Mode or Formal_Extensions)
+              and then GNATprove_Mode
             then
                declare
                   Prag : constant Node_Id := New_Copy_Tree (N);
@@ -9302,17 +9296,6 @@ package body Sem_Prag is
          end if;
       end Set_Ravenscar_Profile;
 
-      ----------------
-      -- S14_Pragma --
-      ----------------
-
-      procedure S14_Pragma is
-      begin
-         if not Formal_Extensions then
-            Error_Pragma ("pragma% requires the use of debug switch -gnatd.V");
-         end if;
-      end S14_Pragma;
-
    --  Start of processing for Analyze_Pragma
 
    begin
@@ -9700,9 +9683,7 @@ package body Sem_Prag is
                --  Verify whether the state introduces an illegal hidden state
                --  within a package subject to a null abstract state.
 
-               if Formal_Extensions then
-                  Check_No_Hidden_State (Id);
-               end if;
+               Check_No_Hidden_State (Id);
 
                --  Associate the state with its related package
 
@@ -9722,7 +9703,6 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            S14_Pragma;
             Check_Arg_Count (1);
             Ensure_Aggregate_Form (Arg1);
 
@@ -11894,7 +11874,6 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            S14_Pragma;
             Check_Arg_Count (1);
             Ensure_Aggregate_Form (Arg1);
 
@@ -13165,7 +13144,6 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            S14_Pragma;
             Check_Arg_Count (1);
             Ensure_Aggregate_Form (Arg1);
 
@@ -13897,7 +13875,6 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            S14_Pragma;
             Check_Arg_Count (1);
 
             --  Ensure the proper placement of the pragma. Initial_Condition
@@ -14009,7 +13986,6 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            S14_Pragma;
             Check_Arg_Count (1);
             Ensure_Aggregate_Form (Arg1);
 
@@ -17542,7 +17518,6 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            S14_Pragma;
             Check_Arg_Count (1);
 
             --  Ensure the proper placement of the pragma. Refined states must