[multiple changes]

2012-10-29  Yannick Moy  <moy@adacore.com>

	* debug.adb Associate debug switch -gnatd.V to extensions for
	formal verification.
	* gnat1drv.adb (Adjust_Global_Switches): Set flag S14_Extensions
	when -gnatd.V is set.
	* gnat_rm.texi: Remove doc for Assert_And_Cut.
	* opt.ads Declare new flag S14_Extensions, to be set when new
	aspects/pragmas/attributes for formal verification should be
	accepted.
	* sem_prag.adb (Analyze_Pragma): Check that S14_Extensions is
	set when treating pragma Assert_And_Cut.

2012-10-29  Tristan Gingold  <gingold@adacore.com>

	* s-tarest.ads, s-tassta.adb: Add a pragma Partition_Elaboration_Policy.

From-SVN: r192931

8 files changed, 53 insertions, 38 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cb3f6ab..c200a06 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,20 @@
+2012-10-29  Yannick Moy  <moy@adacore.com>
+
+	* debug.adb Associate debug switch -gnatd.V to extensions for
+	formal verification.
+	* gnat1drv.adb (Adjust_Global_Switches): Set flag S14_Extensions
+	when -gnatd.V is set.
+	* gnat_rm.texi: Remove doc for Assert_And_Cut.
+	* opt.ads Declare new flag S14_Extensions, to be set when new
+	aspects/pragmas/attributes for formal verification should be
+	accepted.
+	* sem_prag.adb (Analyze_Pragma): Check that S14_Extensions is
+	set when treating pragma Assert_And_Cut.
+
+2012-10-29  Tristan Gingold  <gingold@adacore.com>
+
+	* s-tarest.ads, s-tassta.adb: Add a pragma Partition_Elaboration_Policy.
+
 2012-10-29  Robert Dewar  <dewar@adacore.com>
 
 	* freeze.adb: Minor reformatting.
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index f6f24f9..02f04bc 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -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
+   --  d.V  Extensions for formal verification
    --  d.W  Print out debugging information for Walk_Library_Items
    --  d.X  Use Expression_With_Actions
    --  d.Y  Do not use Expression_With_Actions
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index a8eb320..39d008e 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -418,6 +418,10 @@ procedure Gnat1drv is
 
       --  Set switches for formal verification mode
 
+      if Debug_Flag_Dot_VV then
+         S14_Extensions := True;
+      end if;
+
       if Debug_Flag_Dot_FF then
          Alfa_Mode := True;
 
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 3561ced..36202bd 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -105,7 +105,6 @@ Implementation Defined Pragmas
 * Pragma Ada_2012::
 * Pragma Annotate::
 * Pragma Assert::
-* Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Ast_Entry::
@@ -844,7 +843,6 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Ada_2012::
 * Pragma Annotate::
 * Pragma Assert::
-* Pragma Assert_And_Cut::
 * Pragma Assertion_Policy::
 * Pragma Assume_No_Invalid_Values::
 * Pragma Ast_Entry::
@@ -1197,40 +1195,6 @@ of Ada from 2005 on. In GNAT, it is implemented in all versions
 of Ada, and the DISABLE policy is an implementation-defined
 addition.
 
-@node Pragma Assert_And_Cut
-@unnumberedsec Pragma Assert_And_Cut
-@findex Assert_And_Cut
-@noindent
-Syntax:
-@smallexample @c ada
-pragma Assert_And_Cut (
-  boolean_EXPRESSION
-  [, string_EXPRESSION]);
-@end smallexample
-
-@noindent
-The effect of this pragma for compilation is exactly the same as the one
-of pragma @code{Assert}. This pragma is used to help formal verification
-tools by marking program points where the tool can simplify precise
-knowledge about execution based on the assertion given. For example, in
-the procedure below, all that is needed to prove that the code using X
-is free from run-time errors is that X is positive. Without the pragma,
-GNATprove considers all execution paths through P, which may be
-many. With the pragma, GNATprove only needs to consider the paths from
-the start of the procedure to the pragma, and the paths from the pragma
-to the end of the procedure, hence many fewer paths. For more details,
-see the GNATprove User's Guide.
-
-@smallexample @c ada
-procedure P is
-   X : Integer;
-begin
-   --  complex computation that sets X
-   pragma Assert_And_Cut (X > 0);
-   --  complex computation that uses X
-end P;
-@end smallexample
-
 @node Pragma Assertion_Policy
 @unnumberedsec Pragma Assertion_Policy
 @findex Debug_Policy
@@ -7986,7 +7950,7 @@ features are used, as defined in Annex J of the Ada Reference Manual.
 wide types
 appear, and that no wide or wide wide string or character literals
 appear in the program (that is literals representing characters not in
-type @code{Character}.
+type @code{Character}).
 
 @node SPARK
 @unnumberedsubsec SPARK
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 17c9317..b832c1f 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1936,6 +1936,11 @@ package Opt is
    --  for integers are limited to the strict minimum with this option. Set by
    --  debug flag -gnatd.D.
 
+   S14_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"
diff --git a/gcc/ada/s-tarest.ads b/gcc/ada/s-tarest.ads
index b6639b1..c876975 100644
--- a/gcc/ada/s-tarest.ads
+++ b/gcc/ada/s-tarest.ads
@@ -43,6 +43,10 @@
 --  The restricted GNARLI is also composed of System.Protected_Objects and
 --  System.Protected_Objects.Single_Entry
 
+pragma Partition_Elaboration_Policy (Sequential);
+--  This package only implements the sequential elaboration policy. This pragma
+--  will enforce it (and detect conflicts with user specified policy).
+
 with System.Task_Info;
 with System.Parameters;
 
diff --git a/gcc/ada/s-tassta.adb b/gcc/ada/s-tassta.adb
index 08886c1..ab75b23 100644
--- a/gcc/ada/s-tassta.adb
+++ b/gcc/ada/s-tassta.adb
@@ -33,6 +33,10 @@ pragma Polling (Off);
 --  Turn off polling, we do not want ATC polling to take place during tasking
 --  operations. It causes infinite loops and other problems.
 
+pragma Partition_Elaboration_Policy (Concurrent);
+--  This package only implements the concurrent elaboration policy. This pragma
+--  will enforce it (and detect conflicts with user specified policy).
+
 with Ada.Exceptions;
 with Ada.Unchecked_Deallocation;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index e5dfde9..7f098ab 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -782,6 +782,10 @@ 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.
+
       function Is_Before_First_Decl
         (Pragma_Node : Node_Id;
          Decls       : List_Id) return Boolean;
@@ -1280,6 +1284,7 @@ package body Sem_Prag is
             Error_Pragma_Arg ("invalid argument for pragma%", Argx);
          end if;
       end Check_Arg_Is_One_Of;
+
       ---------------------------------
       -- Check_Arg_Is_Queuing_Policy --
       ---------------------------------
@@ -6419,6 +6424,17 @@ package body Sem_Prag is
          end if;
       end Set_Ravenscar_Profile;
 
+      ----------------
+      -- S14_Pragma --
+      ----------------
+
+      procedure S14_Pragma is
+      begin
+         if not S14_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
@@ -6800,6 +6816,7 @@ package body Sem_Prag is
                Ada_2005_Pragma;
             else -- Pragma_Assert_And_Cut
                GNAT_Pragma;
+               S14_Pragma;
             end if;
 
             Check_At_Least_N_Arguments (1);