aspects.adb, [...] (Aspect_Id): New GNAT aspect Aspect_Contract_Case.

2012-03-15  Yannick Moy  <moy@adacore.com>

	* aspects.adb, aspects.ads (Aspect_Id): New GNAT aspect
	Aspect_Contract_Case.
	* gnat_rm.texi Document the new pragma/aspect
	Contract_Case. Correct the documentation of the existing
	pragma/aspect Test_Case with the new semantics.
	* sem_attr.adb (Analyze_Attribute): Allow use of 'Result in the
	Ensures component of a Contract_Case pragma.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Check new aspect
	and translate it into a pragma.
	(Check_Aspect_At_Freeze_Point): Take into account the new aspect.
	* sem_ch3.adb, sinfo.adb, sinfo.ads Renaming of TC (for test case)
	into CTC (for contract and test case).
	* sem_ch6.adb (Process_PPCs): Generate Check pragmas from
	Contract_Case pragmas, similarly to what is done already for
	postconditions.
	* sem_prag.adb, sem_prag.ads (Check_Contract_Or_Test_Case):
	Renaming of Check_Test_Case.
	(Analyze_Pragma, Sig_Flags): Take into account the new pragma.
	* sem_util.adb, sem_util.ads Renaming to take into account the
	new pragma, so that functions which applied only to Test_Case
	now apply to both Test_Case and Contract_Case.
	* par-prag.adb, sem_warn.adb, snames.ads-tmpl Take into account
	the new pragma.

From-SVN: r185415

17 files changed, 496 insertions, 196 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 7ef46d5..f5b141e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,29 @@
+2012-03-15  Yannick Moy  <moy@adacore.com>
+
+	* aspects.adb, aspects.ads (Aspect_Id): New GNAT aspect
+	Aspect_Contract_Case.
+	* gnat_rm.texi Document the new pragma/aspect
+	Contract_Case. Correct the documentation of the existing
+	pragma/aspect Test_Case with the new semantics.
+	* sem_attr.adb (Analyze_Attribute): Allow use of 'Result in the
+	Ensures component of a Contract_Case pragma.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Check new aspect
+	and translate it into a pragma.
+	(Check_Aspect_At_Freeze_Point): Take into account the new aspect.
+	* sem_ch3.adb, sinfo.adb, sinfo.ads Renaming of TC (for test case)
+	into CTC (for contract and test case).
+	* sem_ch6.adb (Process_PPCs): Generate Check pragmas from
+	Contract_Case pragmas, similarly to what is done already for
+	postconditions.
+	* sem_prag.adb, sem_prag.ads (Check_Contract_Or_Test_Case):
+	Renaming of Check_Test_Case.
+	(Analyze_Pragma, Sig_Flags): Take into account the new pragma.
+	* sem_util.adb, sem_util.ads Renaming to take into account the
+	new pragma, so that functions which applied only to Test_Case
+	now apply to both Test_Case and Contract_Case.
+	* par-prag.adb, sem_warn.adb, snames.ads-tmpl Take into account
+	the new pragma.
+
 2012-03-15  Robert Dewar  <dewar@adacore.com>
 
 	* sem_ch6.ads: Minor comment updates.
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 51f468c..b155a08 100755
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -249,6 +249,7 @@ package body Aspects is
     Aspect_Bit_Order                    => Aspect_Bit_Order,
     Aspect_Component_Size               => Aspect_Component_Size,
     Aspect_Constant_Indexing            => Aspect_Constant_Indexing,
+    Aspect_Contract_Case                => Aspect_Contract_Case,
     Aspect_CPU                          => Aspect_CPU,
     Aspect_Default_Component_Value      => Aspect_Default_Component_Value,
     Aspect_Default_Iterator             => Aspect_Default_Iterator,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 84548a9..781651f 100755
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -50,6 +50,7 @@ package Aspects is
       Aspect_Bit_Order,
       Aspect_Component_Size,
       Aspect_Constant_Indexing,
+      Aspect_Contract_Case,                 -- GNAT
       Aspect_CPU,
       Aspect_Default_Component_Value,
       Aspect_Default_Iterator,
@@ -176,6 +177,7 @@ package Aspects is
                             (Aspect_Ada_2005                 => True,
                              Aspect_Ada_2012                 => True,
                              Aspect_Compiler_Unit            => True,
+                             Aspect_Contract_Case            => True,
                              Aspect_Dimension                => True,
                              Aspect_Dimension_System         => True,
                              Aspect_Favor_Top_Level          => True,
@@ -206,8 +208,9 @@ package Aspects is
    --  the same aspect attached to the same declaration are allowed.
 
    No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
-                             (Aspect_Test_Case => False,
-                              others           => True);
+                             (Aspect_Contract_Case => False,
+                              Aspect_Test_Case     => False,
+                              others               => True);
 
    --  The following array indicates type aspects that are inherited and apply
    --  to the class-wide type as well.
@@ -259,6 +262,7 @@ package Aspects is
                         Aspect_Bit_Order               => Expression,
                         Aspect_Component_Size          => Expression,
                         Aspect_Constant_Indexing       => Name,
+                        Aspect_Contract_Case           => Expression,
                         Aspect_CPU                     => Expression,
                         Aspect_Default_Component_Value => Expression,
                         Aspect_Default_Iterator        => Name,
@@ -325,6 +329,7 @@ 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_CPU                          => Name_CPU,
      Aspect_Default_Iterator             => Name_Default_Iterator,
      Aspect_Default_Value                => Name_Default_Value,
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 701cc0f..e0ab56f 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -120,6 +120,7 @@ Implementation Defined Pragmas
 * Pragma Complete_Representation::
 * Pragma Complex_Representation::
 * Pragma Component_Alignment::
+* Pragma Contract_Case::
 * Pragma Convention_Identifier::
 * Pragma CPP_Class::
 * Pragma CPP_Constructor::
@@ -855,6 +856,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Complete_Representation::
 * Pragma Complex_Representation::
 * Pragma Component_Alignment::
+* Pragma Contract_Case::
 * Pragma Convention_Identifier::
 * Pragma CPP_Class::
 * Pragma CPP_Constructor::
@@ -1704,6 +1706,108 @@ 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
+@cindex Contract cases
+@findex Contract_Case
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Contract_Case (
+   [Name     =>] static_string_Expression
+  ,[Mode     =>] (Nominal | Robustness)
+ [, Requires =>  Boolean_Expression]
+ [, Ensures  =>  Boolean_Expression]);
+@end smallexample
+
+@noindent
+The @code{Contract_Case} 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
+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
+
+@smallexample @c ada
+pragma Postcondition (not R'Old or else E);
+@end smallexample
+
+@noindent
+which is also equivalent to (in Ada 2012)
+
+@smallexample @c ada
+pragma Postcondition (if R'Old then E);
+@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.
+
+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);
+@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 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
+@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:
+
+@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);
+   ...
+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.
+
 @node Pragma Convention_Identifier
 @unnumberedsec Pragma Convention_Identifier
 @findex Convention_Identifier
@@ -5238,9 +5342,12 @@ pragma Test_Case (
 
 @noindent
 The @code{Test_Case} pragma allows defining fine-grain specifications
-for use by testing and verification tools. The compiler checks its
-validity but the presence of pragma @code{Test_Case} does not lead to
-any modification of the code generated by the compiler.
+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.
+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.
 
 @code{Test_Case} pragmas may only appear immediately following the
 (separate) declaration of a subprogram in a package declaration, inside
@@ -5261,19 +5368,19 @@ package Math_Functions is
    function Sqrt (Arg : Float) return Float;
    pragma Test_Case (Name     => "Test 1",
                      Mode     => Nominal,
-                     Requires => Arg < 100,
+                     Requires => Arg < 10000,
                      Ensures  => Sqrt'Result < 10);
    ...
 end Math_Functions;
 @end smallexample
 
 @noindent
-The meaning of a test case is that, if 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 satisfy the precondition of the
-subprogram, and the output context should then satisfy its
-postcondition. More @code{Robustness} indicates that the pre- and
+The meaning of a test case is that there is at least one context where
+@code{Requires} holds such that, if the associated subprogram is executed in
+that context, then @code{Ensures} holds 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 test case.
 
 @node Pragma Thread_Local_Storage
@@ -17375,6 +17482,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{Discard_Names} @tab
 @item @code{External_Tag} @tab
 @item @code{Favor_Top_Level} @tab               -- GNAT
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 629540a..5a1f469 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1109,6 +1109,7 @@ begin
            Pragma_Compile_Time_Error             |
            Pragma_Compile_Time_Warning           |
            Pragma_Compiler_Unit                  |
+           Pragma_Contract_Case                  |
            Pragma_Convention_Identifier          |
            Pragma_CPP_Class                      |
            Pragma_CPP_Constructor                |
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 8d0a38d..c5ad305 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -4256,10 +4256,12 @@ package body Sem_Attr is
                  ("% attribute can only appear in postcondition of function",
                   P);
 
-            elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
+            elsif Get_Pragma_Id (Prag) = Pragma_Contract_Case
+              or else Get_Pragma_Id (Prag) = Pragma_Test_Case
+            then
                declare
                   Arg_Ens : constant Node_Id :=
-                              Get_Ensures_From_Test_Case_Pragma (Prag);
+                              Get_Ensures_From_Case_Pragma (Prag);
                   Arg     : Node_Id;
 
                begin
@@ -4269,7 +4271,13 @@ package body Sem_Attr is
                   end loop;
 
                   if Arg /= Arg_Ens then
-                     Error_Attr ("% attribute misplaced inside Test_Case", P);
+                     if Get_Pragma_Id (Prag) = Pragma_Contract_Case then
+                        Error_Attr
+                          ("% attribute misplaced inside contract case", P);
+                     else
+                        Error_Attr
+                          ("% attribute misplaced inside test case", P);
+                     end if;
                   end if;
                end;
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 2a92558..52f0545 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1450,83 +1450,87 @@ package body Sem_Ch13 is
                   Set_Is_Delayed_Aspect (Aspect);
                   Delay_Required := True;
 
-               when Aspect_Test_Case => declare
-                  Args      : List_Id;
-                  Comp_Expr : Node_Id;
-                  Comp_Assn : Node_Id;
-                  New_Expr  : Node_Id;
-
-               begin
-                  Args := New_List;
-
-                  if Nkind (Parent (N)) = N_Compilation_Unit then
-                     Error_Msg_N
-                       ("incorrect placement of aspect `Test_Case`", E);
-                     goto Continue;
-                  end if;
+               when Aspect_Contract_Case |
+                    Aspect_Test_Case     =>
+                  declare
+                     Args      : List_Id;
+                     Comp_Expr : Node_Id;
+                     Comp_Assn : Node_Id;
+                     New_Expr  : Node_Id;
 
-                  if Nkind (Expr) /= N_Aggregate then
-                     Error_Msg_NE
-                       ("wrong syntax for aspect `Test_Case` for &", Id, E);
-                     goto Continue;
-                  end if;
+                  begin
+                     Args := New_List;
 
-                  --  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
-                       (Make_Pragma_Argument_Association (Sloc (Comp_Expr),
-                          Expression => New_Expr),
-                       Args);
-                     Next (Comp_Expr);
-                  end loop;
+                     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;
 
-                  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
+                     if Nkind (Expr) /= N_Aggregate then
+                        Error_Msg_Name_1 := Nam;
                         Error_Msg_NE
-                          ("wrong syntax for aspect `Test_Case` for &", Id, E);
+                          ("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 (Make_Pragma_Argument_Association (
-                       Sloc       => Sloc (Comp_Assn),
-                       Chars      => Chars (First (Choices (Comp_Assn))),
-                       Expression => New_Expr),
-                       Args);
-                     Next (Comp_Assn);
-                  end loop;
+                     --  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
+                          (Make_Pragma_Argument_Association (Sloc (Comp_Expr),
+                           Expression => New_Expr),
+                           Args);
+                        Next (Comp_Expr);
+                     end loop;
 
-                  --  Build the test-case pragma
+                     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;
 
-                  Aitem :=
-                    Make_Pragma (Loc,
-                      Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Test_Case),
-                      Pragma_Argument_Associations =>
-                        Args);
+                        New_Expr := Relocate_Node (Expression (Comp_Assn));
+                        Set_Original_Node (New_Expr, Expression (Comp_Assn));
+                        Append (Make_Pragma_Argument_Association (
+                          Sloc       => Sloc (Comp_Assn),
+                          Chars      => Chars (First (Choices (Comp_Assn))),
+                          Expression => New_Expr),
+                          Args);
+                        Next (Comp_Assn);
+                     end loop;
 
-                  Set_From_Aspect_Specification (Aitem, True);
-                  Set_Corresponding_Aspect (Aitem, Aspect);
-                  Set_Is_Delayed_Aspect (Aspect);
+                     --  Build the contract-case or test-case pragma
 
-                  --  Insert immediately after the entity declaration
+                     Aitem :=
+                       Make_Pragma (Loc,
+                                    Pragma_Identifier            =>
+                                      Make_Identifier (Sloc (Id), Nam),
+                                    Pragma_Argument_Associations =>
+                                      Args);
 
-                  Insert_After (N, Aitem);
+                     Set_From_Aspect_Specification (Aitem, True);
+                     Set_Corresponding_Aspect (Aitem, Aspect);
+                     Set_Is_Delayed_Aspect (Aspect);
 
-                  goto Continue;
-               end;
+                     --  Insert immediately after the entity declaration
+
+                     Insert_After (N, Aitem);
+
+                     goto Continue;
+                  end;
 
                when Aspect_Dimension =>
                   Analyze_Aspect_Dimension (N, Id, Expr);
@@ -6158,7 +6162,13 @@ package body Sem_Ch13 is
          when Boolean_Aspects =>
             raise Program_Error;
 
-         --  Test_Case aspect applies to entries and subprograms, hence should
+         --  Contract_Case aspects apply to subprograms, hence should never be
+         --  delayed.
+
+         when Aspect_Contract_Case =>
+            raise Program_Error;
+
+         --  Test_Case aspects apply to entries and subprograms, hence should
          --  never be delayed.
 
          when Aspect_Test_Case =>
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 3e1059f..9d66884 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2204,9 +2204,9 @@ package body Sem_Ch3 is
 
                Check_Subprogram_Contract (Sent);
 
-               Prag := Spec_TC_List (Contract (Sent));
+               Prag := Spec_CTC_List (Contract (Sent));
                while Present (Prag) loop
-                  Analyze_TC_In_Decl_Part (Prag, Sent);
+                  Analyze_CTC_In_Decl_Part (Prag, Sent);
                   Prag := Next_Pragma (Prag);
                end loop;
             end if;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 9b37f46..6adcaa3 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -10932,6 +10932,11 @@ package body Sem_Ch6 is
       Plist : List_Id := No_List;
       --  List of generated postconditions
 
+      function Grab_CC return Node_Id;
+      --  Prag contains an analyzed contract case pragma. This function copies
+      --  relevant components of the pragma, creates the corresponding Check
+      --  pragma and returns the Check pragma as the result.
+
       function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
       --  Prag contains an analyzed precondition or postcondition pragma. This
       --  function copies the pragma, changes it to the corresponding Check
@@ -10954,6 +10959,87 @@ package body Sem_Ch6 is
       --  that an invariant check is required (for an IN OUT parameter, or
       --  the returned value of a function.
 
+      -------------
+      -- Grab_CC --
+      -------------
+
+      function Grab_CC return Node_Id is
+         CP   : Node_Id;
+         Req  : Node_Id;
+         Ens  : Node_Id;
+         Post : Node_Id;
+         Loc  : constant Source_Ptr := Sloc (Prag);
+
+         --  Similarly to postcondition, the string is "failed xx from yy"
+         --  where xx is in all lower case. The reason for this different
+         --  wording compared to other Check cases is that the failure is not
+         --  at the point of occurrence of the pragma, unlike the other Check
+         --  cases.
+
+         Msg  : constant String :=
+                  "failed contract case from " & Build_Location_String (Loc);
+
+      begin
+         --  Copy the Requires and Ensures expressions
+
+         Req  := New_Copy_Tree (
+                   Expression (Get_Requires_From_Case_Pragma (Prag)),
+                   New_Scope => Current_Scope);
+
+         Ens  := New_Copy_Tree (
+                   Expression (Get_Ensures_From_Case_Pragma (Prag)),
+                   New_Scope => Current_Scope);
+
+         --  Build the postcondition (not Requires'Old or else Ensures)
+
+         Post := Make_Or_Else (Loc,
+                   Left_Opnd  => Make_Op_Not (Loc,
+                                   Make_Attribute_Reference (Loc,
+                                     Prefix         => Req,
+                                     Attribute_Name => Name_Old)),
+                   Right_Opnd => Ens);
+
+         --  For a contract case pragma within a generic, generate a
+         --  postcondition pragma for later expansion. This is also used
+         --  when an error was detected, thus setting Expander_Active to False.
+
+         if not Expander_Active then
+            CP := Make_Pragma (Loc,
+                    Chars => Name_Postcondition,
+                    Pragma_Argument_Associations => New_List (
+                      Make_Pragma_Argument_Association (Loc,
+                        Chars      => Name_Check,
+                        Expression => Post),
+
+                      Make_Pragma_Argument_Association (Loc,
+                        Chars      => Name_Message,
+                        Expression => Make_String_Literal (Loc, Msg))));
+
+         --  Otherwise, create the Check pragma
+
+         else
+            CP := Make_Pragma (Loc,
+                    Chars => Name_Check,
+                    Pragma_Argument_Associations => New_List (
+                      Make_Pragma_Argument_Association (Loc,
+                        Chars      => Name_Name,
+                        Expression =>
+                          Make_Identifier (Loc, Name_Postcondition)),
+
+                      Make_Pragma_Argument_Association (Loc,
+                        Chars      => Name_Check,
+                        Expression => Post),
+
+                      Make_Pragma_Argument_Association (Loc,
+                        Chars      => Name_Message,
+                        Expression => Make_String_Literal (Loc, Msg))));
+         end if;
+
+         --  Return the Postcondition or Check pragma
+
+         return CP;
+      end Grab_CC;
+
       --------------
       -- Grab_PPC --
       --------------
@@ -11005,7 +11091,8 @@ package body Sem_Ch6 is
          Set_Comes_From_Source (CP, False);
 
          --  For a postcondition pragma within a generic, preserve the pragma
-         --  for later expansion.
+         --  for later expansion. This is also used when an error was detected,
+         --  thus setting Expander_Active to False.
 
          if Nam = Name_Postcondition
            and then not Expander_Active
@@ -11328,6 +11415,11 @@ package body Sem_Ch6 is
 
       if Present (Spec_Id) then
          Spec_Postconditions : declare
+            procedure Process_Contract_Cases (Spec : Node_Id);
+            --  This processes the Spec_CTC_List from Spec, processing any
+            --  contract-case from the list. The caller has checked that
+            --  Spec_CTC_List is non-Empty.
+
             procedure Process_Post_Conditions
               (Spec  : Node_Id;
                Class : Boolean);
@@ -11336,6 +11428,34 @@ package body Sem_Ch6 is
             --  postconditions marked with Class_Present are considered.
             --  The caller has checked that Spec_PPC_List is non-Empty.
 
+            ----------------------------
+            -- Process_Contract_Cases --
+            ----------------------------
+
+            procedure Process_Contract_Cases (Spec : Node_Id) is
+            begin
+               --  Loop through Contract_Case pragmas from spec
+
+               Prag := Spec_CTC_List (Contract (Spec));
+               loop
+                  if Pragma_Name (Prag) = Name_Contract_Case then
+                     if Plist = No_List then
+                        Plist := Empty_List;
+                     end if;
+
+                     if not Expander_Active then
+                        Prepend (Grab_CC, Declarations (N));
+                     else
+                        Append (Grab_CC, Plist);
+                     end if;
+                  end if;
+
+                  Prag := Next_Pragma (Prag);
+                  exit when No (Prag);
+               end loop;
+
+            end Process_Contract_Cases;
+
             -----------------------------
             -- Process_Post_Conditions --
             -----------------------------
@@ -11380,6 +11500,14 @@ package body Sem_Ch6 is
          --  Start of processing for Spec_Postconditions
 
          begin
+            --  Process postconditions expressed as contract-cases
+
+            if Present (Spec_CTC_List (Contract (Spec_Id))) then
+               Process_Contract_Cases (Spec_Id);
+            end if;
+
+            --  Process spec postconditions
+
             if Present (Spec_PPC_List (Contract (Spec_Id))) then
                Process_Post_Conditions (Spec_Id, Class => False);
             end if;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 39d406e..aa574ee 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -181,10 +181,10 @@ package body Sem_Prag is
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
-   procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id);
+   procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
    --  Preanalyze the boolean expressions in the Requires and Ensures arguments
-   --  of a Test_Case pragma if present (possibly Empty). We treat these as
-   --  spec expressions (i.e. similar to a default expression).
+   --  of a Contract_Case or Test_Case pragma if present (possibly Empty). We
+   --  treat these as spec expressions (i.e. similar to a default expression).
 
    procedure rv;
    --  This is a dummy function called by the processing for pragma Reviewable.
@@ -637,15 +637,16 @@ package body Sem_Prag is
       --  that the constraint is static as required by the restrictions for
       --  Unchecked_Union.
 
-      procedure Check_Test_Case;
-      --  Called to process a test-case pragma. The treatment is similar to the
-      --  one for pre- and postcondition in Check_Precondition_Postcondition,
-      --  except the placement rules for the test-case pragma are stricter.
-      --  This pragma may only occur after a subprogram spec declared directly
-      --  in a package spec unit. In this case, the pragma is chained to the
-      --  subprogram in question (using Spec_TC_List and Next_Pragma) and
-      --  analysis of the pragma is delayed till the end of the spec. In
-      --  all other cases, an error message for bad placement is given.
+      procedure Check_Contract_Or_Test_Case;
+      --  Called to process a contract-case or test-case pragma. The
+      --  treatment is similar to the one for pre- and postcondition in
+      --  Check_Precondition_Postcondition, except the placement rules for the
+      --  contract-case and test-case pragmas are stricter. These pragmas may
+      --  only occur after a subprogram spec declared directly in a package
+      --  spec unit. In this case, the pragma is chained to the subprogram in
+      --  question (using Spec_CTC_List and Next_Pragma) and analysis of the
+      --  pragma is delayed till the end of the spec. In all other cases, an
+      --  error message for bad placement is given.
 
       procedure Check_Valid_Configuration_Pragma;
       --  Legality checks for placement of a configuration pragma
@@ -2113,24 +2114,25 @@ package body Sem_Prag is
          end case;
       end Check_Static_Constraint;
 
-      ---------------------
-      -- Check_Test_Case --
-      ---------------------
+      ---------------------------------
+      -- Check_Contract_Or_Test_Case --
+      ---------------------------------
 
-      procedure Check_Test_Case is
+      procedure Check_Contract_Or_Test_Case is
          P  : Node_Id;
          PO : Node_Id;
 
-         procedure Chain_TC (PO : Node_Id);
+         procedure Chain_CTC (PO : Node_Id);
          --  If PO is a [generic] subprogram declaration node, then the
-         --  test-case applies to this subprogram and the processing for the
-         --  pragma is completed. Otherwise the pragma is misplaced.
+         --  contract-case or test-case applies to this subprogram and the
+         --  processing for the pragma is completed. Otherwise the pragma
+         --  is misplaced.
 
-         --------------
-         -- Chain_TC --
-         --------------
+         ---------------
+         -- Chain_CTC --
+         ---------------
 
-         procedure Chain_TC (PO : Node_Id) is
+         procedure Chain_CTC (PO : Node_Id) is
             S   : Entity_Id;
 
          begin
@@ -2166,21 +2168,21 @@ package body Sem_Prag is
             --  in this analysis, allowing forward references. The analysis
             --  happens at the end of Analyze_Declarations.
 
-            --  There should not be another test case with the same name
-            --  associated to this subprogram.
+            --  There should not be another contract-case or test-case with the
+            --  same name associated to this subprogram.
 
             declare
-               Name : constant String_Id := Get_Name_From_Test_Case_Pragma (N);
-               TC   : Node_Id;
+               Name : constant String_Id := Get_Name_From_Case_Pragma (N);
+               CTC   : Node_Id;
 
             begin
-               TC := Spec_TC_List (Contract (S));
-               while Present (TC) loop
+               CTC := Spec_CTC_List (Contract (S));
+               while Present (CTC) loop
 
                   if String_Equal
-                    (Name, Get_Name_From_Test_Case_Pragma (TC))
+                    (Name, Get_Name_From_Case_Pragma (CTC))
                   then
-                     Error_Msg_Sloc := Sloc (TC);
+                     Error_Msg_Sloc := Sloc (CTC);
 
                      if From_Aspect_Specification (N) then
                         Error_Pragma ("name for aspect% is already used#");
@@ -2189,24 +2191,24 @@ package body Sem_Prag is
                      end if;
                   end if;
 
-                  TC := Next_Pragma (TC);
+                  CTC := Next_Pragma (CTC);
                end loop;
             end;
 
-            --  Chain spec TC pragma to list for subprogram
+            --  Chain spec CTC pragma to list for subprogram
 
-            Set_Next_Pragma (N, Spec_TC_List (Contract (S)));
-            Set_Spec_TC_List (Contract (S), N);
-         end Chain_TC;
+            Set_Next_Pragma (N, Spec_CTC_List (Contract (S)));
+            Set_Spec_CTC_List (Contract (S), N);
+         end Chain_CTC;
 
-      --  Start of processing for Check_Test_Case
+      --  Start of processing for Check_Contract_Or_Test_Case
 
       begin
          if not Is_List_Member (N) then
             Pragma_Misplaced;
          end if;
 
-         --  Test cases should only appear in package spec unit
+         --  Contract-case or test-case should only appear in package spec unit
 
          if Get_Source_Unit (N) = No_Unit
            or else not Nkind_In (Sinfo.Unit (Cunit (Get_Source_Unit (N))),
@@ -2224,9 +2226,9 @@ package body Sem_Prag is
 
             --  If the previous node is a generic subprogram, do not go to to
             --  the original node, which is the unanalyzed tree: we need to
-            --  attach the test-case to the analyzed version at this point.
-            --  They get propagated to the original tree when analyzing the
-            --  corresponding body.
+            --  attach the contract-case or test-case to the analyzed version
+            --  at this point. They get propagated to the original tree when
+            --  analyzing the corresponding body.
 
             if Nkind (P) not in N_Generic_Declaration then
                PO := Original_Node (P);
@@ -2258,7 +2260,7 @@ package body Sem_Prag is
                Pragma_Misplaced;
 
             else
-               Chain_TC (PO);
+               Chain_CTC (PO);
                return;
             end if;
          end loop;
@@ -2266,7 +2268,7 @@ package body Sem_Prag is
          --  If we fall through, pragma was misplaced
 
          Pragma_Misplaced;
-      end Check_Test_Case;
+      end Check_Contract_Or_Test_Case;
 
       --------------------------------------
       -- Check_Valid_Configuration_Pragma --
@@ -13904,18 +13906,21 @@ package body Sem_Prag is
             end if;
          end Task_Storage;
 
-         ---------------
-         -- Test_Case --
-         ---------------
+         -------------------------------
+         -- Contract_Case | Test_Case --
+         -------------------------------
 
-         --  pragma Test_Case ([Name     =>] Static_String_EXPRESSION
+         --  pragma (Contract_Case | Test_Case)
+         --                   ([Name     =>] Static_String_EXPRESSION
          --                   ,[Mode     =>] MODE_TYPE
          --                  [, Requires =>  Boolean_EXPRESSION]
          --                  [, Ensures  =>  Boolean_EXPRESSION]);
 
          --  MODE_TYPE ::= Nominal | Robustness
 
-         when Pragma_Test_Case => Test_Case : declare
+         when Pragma_Contract_Case |
+              Pragma_Test_Case =>
+         Contract_Or_Test_Case : declare
          begin
             GNAT_Pragma;
             Check_At_Least_N_Arguments (2);
@@ -13947,8 +13952,8 @@ package body Sem_Prag is
                Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
             end if;
 
-            Check_Test_Case;
-         end Test_Case;
+            Check_Contract_Or_Test_Case;
+         end Contract_Or_Test_Case;
 
          --------------------------
          -- Thread_Local_Storage --
@@ -14819,11 +14824,11 @@ package body Sem_Prag is
       when Pragma_Exit => null;
    end Analyze_Pragma;
 
-   -----------------------------
-   -- Analyze_TC_In_Decl_Part --
-   -----------------------------
+   ------------------------------
+   -- Analyze_CTC_In_Decl_Part --
+   ------------------------------
 
-   procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
+   procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
    begin
       --  Install formals and push subprogram spec onto scope stack so that we
       --  can see the formals from the pragma.
@@ -14834,15 +14839,15 @@ package body Sem_Prag is
       --  Preanalyze the boolean expressions, we treat these as spec
       --  expressions (i.e. similar to a default expression).
 
-      Preanalyze_TC_Args (N,
-                          Get_Requires_From_Test_Case_Pragma (N),
-                          Get_Ensures_From_Test_Case_Pragma (N));
+      Preanalyze_CTC_Args (N,
+                           Get_Requires_From_Case_Pragma (N),
+                           Get_Ensures_From_Case_Pragma (N));
 
       --  Remove the subprogram from the scope stack now that the pre-analysis
-      --  of the expressions in the test-case is done.
+      --  of the expressions in the contract-case or test-case is done.
 
       End_Scope;
-   end Analyze_TC_In_Decl_Part;
+   end Analyze_CTC_In_Decl_Part;
 
    --------------------
    -- Check_Disabled --
@@ -15077,6 +15082,7 @@ package body Sem_Prag is
       Pragma_Complete_Representation        =>  0,
       Pragma_Complex_Representation         =>  0,
       Pragma_Component_Alignment            => -1,
+      Pragma_Contract_Case                  => -1,
       Pragma_Controlled                     =>  0,
       Pragma_Convention                     =>  0,
       Pragma_Convention_Identifier          =>  0,
@@ -15431,11 +15437,11 @@ package body Sem_Prag is
       end if;
    end Make_Aspect_For_PPC_In_Gen_Sub_Decl;
 
-   ------------------------
-   -- Preanalyze_TC_Args --
-   ------------------------
+   -------------------------
+   -- Preanalyze_CTC_Args --
+   -------------------------
 
-   procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id) is
+   procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id) is
    begin
       --  Preanalyze the boolean expressions, we treat these as spec
       --  expressions (i.e. similar to a default expression).
@@ -15465,7 +15471,7 @@ package body Sem_Prag is
               (Original_Node (Get_Pragma_Arg (Arg_Ens)), Standard_Boolean);
          end if;
       end if;
-   end Preanalyze_TC_Args;
+   end Preanalyze_CTC_Args;
 
    --------------------------------------
    -- Process_Compilation_Unit_Pragmas --
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index ede9d28..23a23d3 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -46,13 +46,13 @@ package Sem_Prag is
    procedure Analyze_Pragma (N : Node_Id);
    --  Analyze procedure for pragma reference node N
 
-   procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id);
-   --  Special analyze routine for test-case pragma that appears within a
-   --  declarative part where the pragma is associated with a subprogram
-   --  specification. N is the pragma node, and S is the entity for the related
-   --  subprogram. This procedure does a preanalysis of the expressions in the
-   --  pragma as "spec expressions" (see section in Sem "Handling of Default
-   --  and Per-Object Expressions...").
+   procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id);
+   --  Special analyze routine for contract-case and test-case pragmas that
+   --  appears within a declarative part where the pragma is associated with
+   --  a subprogram specification. N is the pragma node, and S is the entity
+   --  for the related subprogram. This procedure does a preanalysis of the
+   --  expressions in the pragma as "spec expressions" (see section in Sem
+   --  "Handling of Default and Per-Object Expressions...").
 
    function Check_Disabled (Nam : Name_Id) return Boolean;
    --  This function is used in connection with pragmas Assertion, Check,
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 6886408..1d60030 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4490,11 +4490,11 @@ package body Sem_Util is
       end if;
    end Get_Enum_Lit_From_Pos;
 
-   ---------------------------------------
-   -- Get_Ensures_From_Test_Case_Pragma --
-   ---------------------------------------
+   ----------------------------------
+   -- Get_Ensures_From_Case_Pragma --
+   ----------------------------------
 
-   function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+   function Get_Ensures_From_Case_Pragma (N : Node_Id) return Node_Id is
       Args : constant List_Id := Pragma_Argument_Associations (N);
       Res  : Node_Id;
 
@@ -4514,7 +4514,7 @@ package body Sem_Util is
       end if;
 
       return Res;
-   end Get_Ensures_From_Test_Case_Pragma;
+   end Get_Ensures_From_Case_Pragma;
 
    ------------------------
    -- Get_Generic_Entity --
@@ -4602,16 +4602,16 @@ package body Sem_Util is
       return Entity_Id (Get_Name_Table_Info (Id));
    end Get_Name_Entity_Id;
 
-   ------------------------------------
-   -- Get_Name_From_Test_Case_Pragma --
-   ------------------------------------
+   -------------------------------
+   -- Get_Name_From_Case_Pragma --
+   -------------------------------
 
-   function Get_Name_From_Test_Case_Pragma (N : Node_Id) return String_Id is
+   function Get_Name_From_Case_Pragma (N : Node_Id) return String_Id is
       Arg : constant Node_Id :=
               Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
    begin
       return Strval (Expr_Value_S (Arg));
-   end Get_Name_From_Test_Case_Pragma;
+   end Get_Name_From_Case_Pragma;
 
    -------------------
    -- Get_Pragma_Id --
@@ -4656,11 +4656,11 @@ package body Sem_Util is
       return R;
    end Get_Renamed_Entity;
 
-   ----------------------------------------
-   -- Get_Requires_From_Test_Case_Pragma --
-   ----------------------------------------
+   -----------------------------------
+   -- Get_Requires_From_Case_Pragma --
+   -----------------------------------
 
-   function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+   function Get_Requires_From_Case_Pragma (N : Node_Id) return Node_Id is
       Args : constant List_Id := Pragma_Argument_Associations (N);
       Res  : Node_Id;
 
@@ -4677,7 +4677,7 @@ package body Sem_Util is
       end if;
 
       return Res;
-   end Get_Requires_From_Test_Case_Pragma;
+   end Get_Requires_From_Case_Pragma;
 
    -------------------------
    -- Get_Subprogram_Body --
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 0df5450..93f855f 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -538,8 +538,9 @@ package Sem_Util is
    --  If expression N references a part of an object, return this object.
    --  Otherwise return Empty. Expression N should have been resolved already.
 
-   function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id;
-   --  Return the Ensures component of Test_Case pragma N, or Empty otherwise
+   function Get_Ensures_From_Case_Pragma (N : Node_Id) return Node_Id;
+   --  Return the Ensures component of Contract_Case or Test_Case pragma N, or
+   --  Empty otherwise.
 
    function Get_Generic_Entity (N : Node_Id) return Entity_Id;
    --  Returns the true generic entity in an instantiation. If the name in the
@@ -572,8 +573,8 @@ package Sem_Util is
    --  is the innermost visible entity with the given name. See the body of
    --  Sem_Ch8 for further details on handling of entity visibility.
 
-   function Get_Name_From_Test_Case_Pragma (N : Node_Id) return String_Id;
-   --  Return the Name component of Test_Case pragma N
+   function Get_Name_From_Case_Pragma (N : Node_Id) return String_Id;
+   --  Return the Name component of Contract_Case or Test_Case pragma N
 
    function Get_Pragma_Id (N : Node_Id) return Pragma_Id;
    pragma Inline (Get_Pragma_Id);
@@ -590,8 +591,9 @@ package Sem_Util is
    --  not a renamed entity, returns its argument. It is an error to call this
    --  with any other kind of entity.
 
-   function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id;
-   --  Return the Requires component of Test_Case pragma N, or Empty otherwise
+   function Get_Requires_From_Case_Pragma (N : Node_Id) return Node_Id;
+   --  Return the Requires component of Contract_Case or Test_Case pragma N, or
+   --  Empty otherwise.
 
    function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id;
    --  Nod is either a procedure call statement, or a function call, or an
diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb
index 99b71c0..f4e7092 100644
--- a/gcc/ada/sem_warn.adb
+++ b/gcc/ada/sem_warn.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1999-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1999-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -1749,7 +1749,7 @@ package body Sem_Warn is
 
                      function Within_Postcondition return Boolean;
                      --  Returns True iff N is within a Postcondition or
-                     --  Ensures component in a Test_Case.
+                     --  Ensures component in a Contract_Case or Test_Case.
 
                      --------------------------
                      -- Within_Postcondition --
@@ -1770,9 +1770,11 @@ package body Sem_Warn is
                               P := Parent (Nod);
 
                               if Nkind (P) = N_Pragma
-                                and then Pragma_Name (P) = Name_Test_Case
                                 and then
-                                  Nod = Get_Ensures_From_Test_Case_Pragma (P)
+                                  (Pragma_Name (P) = Name_Contract_Case
+                                     or else Pragma_Name (P) = Name_Test_Case)
+                                and then
+                                  Nod = Get_Ensures_From_Case_Pragma (P)
                               then
                                  return True;
                               end if;
diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb
index 96b4570..a8388b1 100644
--- a/gcc/ada/sinfo.adb
+++ b/gcc/ada/sinfo.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -2812,13 +2812,13 @@ package body Sinfo is
       return Node1 (N);
    end Spec_PPC_List;
 
-   function Spec_TC_List
+   function Spec_CTC_List
       (N : Node_Id) return Node_Id is
    begin
       pragma Assert (False
         or else NT (N).Nkind = N_Contract);
       return Node2 (N);
-   end Spec_TC_List;
+   end Spec_CTC_List;
 
    function Specification
       (N : Node_Id) return Node_Id is
@@ -5892,13 +5892,13 @@ package body Sinfo is
       Set_Node1 (N, Val); -- semantic field, no parent set
    end Set_Spec_PPC_List;
 
-   procedure Set_Spec_TC_List
+   procedure Set_Spec_CTC_List
       (N : Node_Id; Val : Node_Id) is
    begin
       pragma Assert (False
         or else NT (N).Nkind = N_Contract);
       Set_Node2 (N, Val); -- semantic field, no parent set
-   end Set_Spec_TC_List;
+   end Set_Spec_CTC_List;
 
    procedure Set_Specification
       (N : Node_Id; Val : Node_Id) is
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 3d1809b..0972d9c 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -6969,7 +6969,7 @@ package Sinfo is
       --  N_Contract
       --  Sloc points to the subprogram's name
       --  Spec_PPC_List (Node1) (set to Empty if none)
-      --  Spec_TC_List (Node2) (set to Empty if none)
+      --  Spec_CTC_List (Node2) (set to Empty if none)
 
       --  Spec_PPC_List points to a list of Precondition and Postcondition
       --  pragma nodes for preconditions and postconditions declared in the
@@ -6978,11 +6978,12 @@ package Sinfo is
       --  Note that this includes precondition/postcondition pragmas generated
       --  to correspond to Pre/Post aspects.
 
-      --  Spec_TC_List points to a list of Test_Case pragma nodes for
-      --  test-cases declared in the spec of the entry/subprogram. The last
-      --  pragma encountered is at the head of this list, so it is in reverse
-      --  order of textual appearance. Note that this includes test-case
-      --  pragmas generated to correspond to Test_Case aspects.
+      --  Spec_CTC_List points to a list of Contract_Case and Test_Case pragma
+      --  nodes for contract-cases and test-cases declared in the spec of the
+      --  entry/subprogram. The last pragma encountered is at the head of this
+      --  list, so it is in reverse order of textual appearance. Note that
+      --  this includes contract-case and test-case pragmas generated from
+      --  Contract_Case and Test_Case aspects.
 
       -------------------
       -- Expanded_Name --
@@ -8963,7 +8964,7 @@ package Sinfo is
    function Spec_PPC_List
      (N : Node_Id) return Node_Id;    -- Node1
 
-   function Spec_TC_List
+   function Spec_CTC_List
      (N : Node_Id) return Node_Id;    -- Node2
 
    function Specification
@@ -9944,7 +9945,7 @@ package Sinfo is
    procedure Set_Spec_PPC_List
      (N : Node_Id; Val : Node_Id);            -- Node1
 
-   procedure Set_Spec_TC_List
+   procedure Set_Spec_CTC_List
      (N : Node_Id; Val : Node_Id);            -- Node2
 
    procedure Set_Specification
@@ -11590,7 +11591,7 @@ package Sinfo is
 
      N_Contract =>
        (1 => False,   --  Spec_PPC_List (Node1)
-        2 => False,   --  Spec_TC_List (Node2)
+        2 => False,   --  Spec_CTC_List (Node2)
         3 => False,   --  unused
         4 => False,   --  unused
         5 => False),  --  unused
@@ -12084,7 +12085,7 @@ package Sinfo is
    pragma Inline (Shift_Count_OK);
    pragma Inline (Source_Type);
    pragma Inline (Spec_PPC_List);
-   pragma Inline (Spec_TC_List);
+   pragma Inline (Spec_CTC_List);
    pragma Inline (Specification);
    pragma Inline (Split_PPC);
    pragma Inline (Statements);
@@ -12407,7 +12408,7 @@ package Sinfo is
    pragma Inline (Set_Shift_Count_OK);
    pragma Inline (Set_Source_Type);
    pragma Inline (Set_Spec_PPC_List);
-   pragma Inline (Set_Spec_TC_List);
+   pragma Inline (Set_Spec_CTC_List);
    pragma Inline (Set_Specification);
    pragma Inline (Set_Split_PPC);
    pragma Inline (Set_Statements);
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 1557722..fd8acc8 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -448,6 +448,7 @@ package Snames is
    Name_Common_Object                  : constant Name_Id := N + $; -- GNAT
    Name_Complete_Representation        : constant Name_Id := N + $; -- GNAT
    Name_Complex_Representation         : constant Name_Id := N + $; -- GNAT
+   Name_Contract_Case                  : constant Name_Id := N + $; -- GNAT
    Name_Controlled                     : constant Name_Id := N + $;
    Name_Convention                     : constant Name_Id := N + $;
    Name_CPP_Class                      : constant Name_Id := N + $; -- GNAT
@@ -1623,6 +1624,7 @@ package Snames is
       Pragma_Common_Object,
       Pragma_Complete_Representation,
       Pragma_Complex_Representation,
+      Pragma_Contract_Case,
       Pragma_Controlled,
       Pragma_Convention,
       Pragma_CPP_Class,