aspects.ads, [...]: Removal of references to Contract_Case.

2013-04-22  Yannick Moy  <moy@adacore.com>

	* aspects.ads, aspects.adb, sem_ch13.adb: Removal of references to
	Contract_Case.
	* gnat_ugn.texi, gnat_rm.texi Description of Contract_Case replaced by
	description of Contract_Cases.

From-SVN: r198127

7 files changed, 113 insertions, 138 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e366188..e1d5a5f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2013-04-22  Yannick Moy  <moy@adacore.com>
+
+	* aspects.ads, aspects.adb, sem_ch13.adb: Removal of references to
+	Contract_Case.
+	* gnat_ugn.texi, gnat_rm.texi Description of Contract_Case replaced by
+	description of Contract_Cases.
+
 2013-04-12  Robert Dewar  <dewar@adacore.com>
 
 	* makeutl.adb, prj-nmsc.adb: Minor reformatting.
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 364f857..fc2b3ad 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -301,7 +301,6 @@ package body Aspects is
     Aspect_Compiler_Unit                => Aspect_Compiler_Unit,
     Aspect_Component_Size               => Aspect_Component_Size,
     Aspect_Constant_Indexing            => Aspect_Constant_Indexing,
-    Aspect_Contract_Case                => Aspect_Contract_Case,
     Aspect_Contract_Cases               => Aspect_Contract_Cases,
     Aspect_Convention                   => Aspect_Convention,
     Aspect_CPU                          => Aspect_CPU,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 2194eb3..690b7b1 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -81,7 +81,6 @@ package Aspects is
       Aspect_Bit_Order,
       Aspect_Component_Size,
       Aspect_Constant_Indexing,
-      Aspect_Contract_Case,                 -- GNAT
       Aspect_Contract_Cases,                -- GNAT
       Aspect_Convention,
       Aspect_CPU,
@@ -229,7 +228,6 @@ package Aspects is
                              Aspect_Ada_2005                 => True,
                              Aspect_Ada_2012                 => True,
                              Aspect_Compiler_Unit            => True,
-                             Aspect_Contract_Case            => True,
                              Aspect_Contract_Cases           => True,
                              Aspect_Depends                  => True,
                              Aspect_Dimension                => True,
@@ -267,8 +265,7 @@ package Aspects is
    --  the same aspect attached to the same declaration are allowed.
 
    No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
-                             (Aspect_Contract_Case  => False,
-                              Aspect_Test_Case      => False,
+                             (Aspect_Test_Case      => False,
                               others                => True);
 
    --  The following array indicates type aspects that are inherited and apply
@@ -322,7 +319,6 @@ package Aspects is
                         Aspect_Bit_Order               => Expression,
                         Aspect_Component_Size          => Expression,
                         Aspect_Constant_Indexing       => Name,
-                        Aspect_Contract_Case           => Expression,
                         Aspect_Contract_Cases          => Expression,
                         Aspect_Convention              => Name,
                         Aspect_CPU                     => Expression,
@@ -397,7 +393,6 @@ package Aspects is
      Aspect_Compiler_Unit                => Name_Compiler_Unit,
      Aspect_Component_Size               => Name_Component_Size,
      Aspect_Constant_Indexing            => Name_Constant_Indexing,
-     Aspect_Contract_Case                => Name_Contract_Case,
      Aspect_Contract_Cases               => Name_Contract_Cases,
      Aspect_Convention                   => Name_Convention,
      Aspect_CPU                          => Name_CPU,
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 130ee3c..9c063c6 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -122,7 +122,7 @@ Implementation Defined Pragmas
 * Pragma Complete_Representation::
 * Pragma Complex_Representation::
 * Pragma Component_Alignment::
-* Pragma Contract_Case::
+* Pragma Contract_Cases::
 * Pragma Convention_Identifier::
 * Pragma CPP_Class::
 * Pragma CPP_Constructor::
@@ -877,7 +877,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Complete_Representation::
 * Pragma Complex_Representation::
 * Pragma Component_Alignment::
-* Pragma Contract_Case::
+* Pragma Contract_Cases::
 * Pragma Convention_Identifier::
 * Pragma CPP_Class::
 * Pragma CPP_Constructor::
@@ -1856,107 +1856,88 @@ If the alignment for a record or array type is not specified (using
 pragma @code{Pack}, pragma @code{Component_Alignment}, or a record rep
 clause), the GNAT uses the default alignment as described previously.
 
-@node Pragma Contract_Case
-@unnumberedsec Pragma Contract_Case
+@node Pragma Contract_Cases
+@unnumberedsec Pragma Contract_Cases
 @cindex Contract cases
-@findex Contract_Case
+@findex Contract_Cases
 @noindent
 Syntax:
 
 @smallexample @c ada
-pragma Contract_Case (
-   [Name     =>] static_string_Expression
-  ,[Mode     =>] (Nominal | Robustness)
- [, Requires =>  Boolean_Expression]
- [, Ensures  =>  Boolean_Expression]);
+pragma Contract_Cases (
+   Condition => Consequence
+ @{,Condition => Consequence@});
 @end smallexample
 
 @noindent
-The @code{Contract_Case} pragma allows defining fine-grain specifications
+The @code{Contract_Cases} pragma allows defining fine-grain specifications
 that can complement or replace the contract given by a precondition and a
-postcondition. Additionally, the @code{Contract_Case} pragma can be used
+postcondition. Additionally, the @code{Contract_Cases} pragma can be used
 by testing and formal verification tools. The compiler checks its validity and,
 depending on the assertion policy at the point of declaration of the pragma,
 it may insert a check in the executable. For code generation, the contract
-case
-
-@smallexample @c ada
-pragma Contract_Case (
-   Name     => ...
-   Mode     => ...
-   Requires => R,
-   Ensures  => E);
-@end smallexample
-
-@noindent
-is equivalent to
+cases
 
 @smallexample @c ada
-pragma Postcondition (not R'Old or else E);
+pragma Contract_Cases (
+  Cond1 => Pred1,
+  Cond2 => Pred2);
 @end smallexample
 
 @noindent
-which is also equivalent to (in Ada 2012)
+are equivalent to
 
 @smallexample @c ada
-pragma Postcondition (if R'Old then E);
+C1 : constant Boolean := Cond1;  --  evaluated at subprogram entry
+C2 : constant Boolean := Cond2;  --  evaluated at subprogram entry
+pragma Precondition ((C1 and not C2) or (C2 and not C1));
+pragma Postcondition (if C1 then Pred1);
+pragma Postcondition (if C2 then Pred2);
 @end smallexample
 
 @noindent
-expressing that, whenever condition @code{R} is satisfied on entry to the
-subprogram, condition @code{E} should be fulfilled on exit to the subprogram.
+The precondition expresses that one and only one of the conditions is
+satisfied on entry to the subprogram.
+The postcondition expresses that, whenever condition @code{Ci} is satisfied
+on entry to the subprogram, consequence @code{Predi} should be fulfilled on
+exit to the subprogram.
 
 A precondition @code{P} and postcondition @code{Q} can also be
 expressed as contract cases:
 
 @smallexample @c ada
-pragma Contract_Case (
-   Name     => "Replace precondition",
-   Mode     => Nominal,
-   Requires => not P,
-   Ensures  => False);
-pragma Contract_Case (
-   Name     => "Replace postcondition",
-   Mode     => Nominal,
-   Requires => P,
-   Ensures  => Q);
+pragma Contract_Cases (P => Q);
 @end smallexample
 
-@code{Contract_Case} pragmas may only appear immediately following the
-(separate) declaration of a subprogram in a package declaration, inside
-a package spec unit. Only other pragmas may intervene (that is appear
-between the subprogram declaration and a contract case).
+The placement and visibility rules for @code{Contract_Cases} pragmas are
+identical to those described for preconditions and postconditions.
 
-The compiler checks that boolean expressions given in @code{Requires} and
-@code{Ensures} are valid, where the rules for @code{Requires} are the
-same as the rule for an expression in @code{Precondition} and the rules
-for @code{Ensures} are the same as the rule for an expression in
+The compiler checks that boolean expressions given in conditions and
+consequences are valid, where the rules for conditions are the same as
+the rule for an expression in @code{Precondition} and the rules for
+consequences are the same as the rule for an expression in
 @code{Postcondition}. In particular, attributes @code{'Old} and
-@code{'Result} can only be used within the @code{Ensures}
-expression. The following is an example of use within a package spec:
+@code{'Result} can only be used within consequence expressions.
+The condition for the last contract case may be @code{others}, to denote
+any case not captured by the previous cases. The
+following is an example of use within a package spec:
 
 @smallexample @c ada
 package Math_Functions is
    ...
    function Sqrt (Arg : Float) return Float;
-   pragma Contract_Case (Name     => "Small argument",
-                         Mode     => Nominal,
-                         Requires => Arg < 100,
-                         Ensures  => Sqrt'Result < 10);
+   pragma Contract_Cases ((Arg in 0 .. 99) => Sqrt'Result < 10,
+                          Arg >= 100       => Sqrt'Result >= 10,
+                          others           => Sqrt'Result = 0);
    ...
 end Math_Functions;
 @end smallexample
 
 @noindent
-The meaning of a contract case is that, whenever the associated subprogram is
-executed in a context where @code{Requires} holds, then @code{Ensures}
-should hold when the subprogram returns. Mode @code{Nominal} indicates
-that the input context should also satisfy the precondition of the
-subprogram, and the output context should also satisfy its
-postcondition. More @code{Robustness} indicates that the precondition and
-postcondition of the subprogram should be ignored for this contract case,
-which is mostly useful when testing such a contract using a testing tool
-that understands contract cases.
+The meaning of contract cases is that only one case should apply at each
+call, as determined by the corresponding condition evaluating to True,
+and that the consequence for this case should hold when the subprogram
+returns.
 
 @node Pragma Convention_Identifier
 @unnumberedsec Pragma Convention_Identifier
@@ -5818,12 +5799,10 @@ pragma Test_Case (
 
 @noindent
 The @code{Test_Case} pragma allows defining fine-grain specifications
-for use by testing tools. Its syntax is similar to the syntax of the
-@code{Contract_Case} pragma, which is used for both testing and
-formal verification.
+for use by testing tools.
 The compiler checks the validity of the @code{Test_Case} pragma, but its
 presence does not lead to any modification of the code generated by the
-compiler, contrary to the treatment of the @code{Contract_Case} pragma.
+compiler.
 
 @code{Test_Case} pragmas may only appear immediately following the
 (separate) declaration of a subprogram in a package declaration, inside
@@ -18138,7 +18117,7 @@ A complete description of the AIs may be found in
 @item @code{Atomic_Components} @tab
 @item @code{Bit_Order} @tab
 @item @code{Component_Size} @tab
-@item @code{Contract_Case} @tab                 -- GNAT
+@item @code{Contract_Cases} @tab                 -- GNAT
 @item @code{Discard_Names} @tab
 @item @code{External_Tag} @tab
 @item @code{Favor_Top_Level} @tab               -- GNAT
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index e1cd61a..17f0f84 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -5413,7 +5413,7 @@ This switch suppresses warnings for tracking of deleted conditional code.
 @cindex @option{-gnatw.t} (@command{gcc})
 This switch activates warnings on suspicious postconditions (whether a
 pragma @code{Postcondition} or a @code{Post} aspect in Ada 2012)
-and suspicious contract cases (pragma @code{Contract_Case}). A
+and suspicious contract cases (pragma @code{Contract_Cases}). A
 function postcondition or contract case is suspicious when no postcondition
 or contract case for this function mentions the result of the function.
 A procedure postcondition or contract case is suspicious when it only
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 32f1f6d..1eaaf5d 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -949,7 +949,7 @@ package body Sem_Ch13 is
       --  analyzed right now.
 
       --  Note that there is a special handling for Pre, Post, Test_Case,
-      --  Contract_Case aspects. In these cases, we do not have to worry
+      --  Contract_Cases aspects. In these cases, we do not have to worry
       --  about delay issues, since the pragmas themselves deal with delay
       --  of visibility for the expression analysis. Thus, we just insert
       --  the pragma after the node N.
@@ -1593,8 +1593,8 @@ package body Sem_Ch13 is
 
                --  Case 4: Special handling for aspects
 
-               --  Pre/Post/Test_Case/Contract_Case whose corresponding pragmas
-               --  take care of the delay.
+               --  Pre/Post/Test_Case/Contract_Cases whose corresponding
+               --  pragmas take care of the delay.
 
                --  Aspects Pre/Post generate Precondition/Postcondition pragmas
                --  with a first argument that is the expression, and a second
@@ -1727,77 +1727,74 @@ package body Sem_Ch13 is
                   goto Continue;
                end;
 
-               when Aspect_Contract_Case |
-                    Aspect_Test_Case     =>
+               when Aspect_Test_Case => Test_Case : declare
+                  Args      : List_Id;
+                  Comp_Expr : Node_Id;
+                  Comp_Assn : Node_Id;
+                  New_Expr  : Node_Id;
 
-                  declare
-                     Args      : List_Id;
-                     Comp_Expr : Node_Id;
-                     Comp_Assn : Node_Id;
-                     New_Expr  : Node_Id;
+               begin
+                  Args := New_List;
 
-                  begin
-                     Args := New_List;
+                  if Nkind (Parent (N)) = N_Compilation_Unit then
+                     Error_Msg_Name_1 := Nam;
+                     Error_Msg_N ("incorrect placement of aspect `%`", E);
+                     goto Continue;
+                  end if;
 
-                     if Nkind (Parent (N)) = N_Compilation_Unit then
-                        Error_Msg_Name_1 := Nam;
-                        Error_Msg_N ("incorrect placement of aspect `%`", E);
-                        goto Continue;
-                     end if;
+                  if Nkind (Expr) /= N_Aggregate then
+                     Error_Msg_Name_1 := Nam;
+                     Error_Msg_NE
+                       ("wrong syntax for aspect `%` for &", Id, E);
+                     goto Continue;
+                  end if;
 
-                     if Nkind (Expr) /= N_Aggregate then
+                  --  Make pragma expressions refer to the original aspect
+                  --  expressions through the Original_Node link. This is
+                  --  used in semantic analysis for ASIS mode, so that the
+                  --  original expression also gets analyzed.
+
+                  Comp_Expr := First (Expressions (Expr));
+                  while Present (Comp_Expr) loop
+                     New_Expr := Relocate_Node (Comp_Expr);
+                     Set_Original_Node (New_Expr, Comp_Expr);
+                     Append_To (Args,
+                       Make_Pragma_Argument_Association (Sloc (Comp_Expr),
+                         Expression => New_Expr));
+                     Next (Comp_Expr);
+                  end loop;
+
+                  Comp_Assn := First (Component_Associations (Expr));
+                  while Present (Comp_Assn) loop
+                     if List_Length (Choices (Comp_Assn)) /= 1
+                       or else
+                         Nkind (First (Choices (Comp_Assn))) /= N_Identifier
+                     then
                         Error_Msg_Name_1 := Nam;
                         Error_Msg_NE
                           ("wrong syntax for aspect `%` for &", Id, E);
                         goto Continue;
                      end if;
 
-                     --  Make pragma expressions refer to the original aspect
-                     --  expressions through the Original_Node link. This is
-                     --  used in semantic analysis for ASIS mode, so that the
-                     --  original expression also gets analyzed.
-
-                     Comp_Expr := First (Expressions (Expr));
-                     while Present (Comp_Expr) loop
-                        New_Expr := Relocate_Node (Comp_Expr);
-                        Set_Original_Node (New_Expr, Comp_Expr);
-                        Append_To (Args,
-                          Make_Pragma_Argument_Association (Sloc (Comp_Expr),
-                            Expression => New_Expr));
-                        Next (Comp_Expr);
-                     end loop;
-
-                     Comp_Assn := First (Component_Associations (Expr));
-                     while Present (Comp_Assn) loop
-                        if List_Length (Choices (Comp_Assn)) /= 1
-                          or else
-                            Nkind (First (Choices (Comp_Assn))) /= N_Identifier
-                        then
-                           Error_Msg_Name_1 := Nam;
-                           Error_Msg_NE
-                             ("wrong syntax for aspect `%` for &", Id, E);
-                           goto Continue;
-                        end if;
-
-                        New_Expr := Relocate_Node (Expression (Comp_Assn));
-                        Set_Original_Node (New_Expr, Expression (Comp_Assn));
-                        Append_To (Args,
-                          Make_Pragma_Argument_Association (Sloc (Comp_Assn),
-                          Chars      => Chars (First (Choices (Comp_Assn))),
-                          Expression => New_Expr));
-                        Next (Comp_Assn);
-                     end loop;
+                     New_Expr := Relocate_Node (Expression (Comp_Assn));
+                     Set_Original_Node (New_Expr, Expression (Comp_Assn));
+                     Append_To (Args,
+                       Make_Pragma_Argument_Association (Sloc (Comp_Assn),
+                       Chars      => Chars (First (Choices (Comp_Assn))),
+                       Expression => New_Expr));
+                     Next (Comp_Assn);
+                  end loop;
 
-                     --  Build the contract-case or test-case pragma
+                  --  Build the test-case pragma
 
-                     Aitem :=
-                       Make_Pragma (Loc,
-                         Pragma_Identifier            =>
-                           Make_Identifier (Sloc (Id), Nam),
-                         Pragma_Argument_Associations => Args);
+                  Aitem :=
+                    Make_Pragma (Loc,
+                      Pragma_Identifier            =>
+                        Make_Identifier (Sloc (Id), Nam),
+                      Pragma_Argument_Associations => Args);
 
-                     Delay_Required := False;
-                  end;
+                  Delay_Required := False;
+               end Test_Case;
 
                when Aspect_Contract_Cases => Contract_Cases : declare
                   Case_Guard  : Node_Id;
@@ -7312,7 +7309,6 @@ package body Sem_Ch13 is
          --  Here is the list of aspects that don't require delay analysis
 
          when Aspect_Abstract_State       |
-              Aspect_Contract_Case        |
               Aspect_Contract_Cases       |
               Aspect_Dimension            |
               Aspect_Dimension_System     |
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0636b8e..700de0c 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -8701,7 +8701,6 @@ package body Sem_Prag is
 
          begin
             GNAT_Pragma;
-            S14_Pragma;
             Check_Arg_Count (1);
 
             --  Completely ignore if not enabled