diff mbox

[Ada] Add GNAT-specific Test_Case aspect and pragma for unit verification

Message ID 20110804133537.GA9110@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2011, 1:35 p.m. UTC
A new aspect Test_Case is defined, which applies to the same declarations as
the Pre and Post aspects: entries and [generic] subprogram declarations.
A corresponding pragma Test_Case is defined, which can be used in all Ada modes
(whereas the aspect is only defined in Ada 2012 mode).

The purpose of this aspect/pragma is to allow users to specify test-cases at
the unit level, next to the pre/post entry or subprogram contract.

A new kind of node N_Contract is defined in the AST, which is not present in
the tree directly, but only pointed by an entry or subprogram entity. This node
contains both the pre/postconditions of an entity and its test-cases.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-04  Yannick Moy  <moy@adacore.com>

	* gnat_rm.texi: Document new pragma and aspect.
	* aspects.adb, aspects.ads (Aspect_Id): new value Aspect_Test_Case
	(No_Duplicates_Allowed): new constant array defining whether duplicates
	aspects of each kind can appear on the same declaration.
	* einfo.adb, einfo.ads (Spec_PPC_List): replace field with Contract
	field, which points to a node holding the previous Spec_PPC_List.
	* exp_ch9.adb, sem_ch6.adb, sem_prag.adb: Reach to Spec_PPC_List
	through the indirection with Contract.
	* exp_util.adb (Insert_Actions): raise Program_Error on N_Contract node
	* par-prag.adb (Prag): do nothing on Test_Case pragma
	* sem.adb (Analyze): abort on N_Contract, on which Analyze should not
	be called directly.
	* sem_attr.adb (Analyze_Attribute): allow attribute 'Result in
	component Ensures of Test_Case.
	* sem_ch12.adb, sem_ch6.adb, sem_ch9.adb
	(Analyze_Generic_Subprogram_Declaration,
	Analyze_Subprogram_Instantiation,
	Analyze_Abstract_Subprogram_Declaration,
	Analyze_Subprogram_Body_Helper,
	Analyze_Subprogram_Specification, Analyze_Entry_Declaration):
	insert contract in subprogram node at point of definition
	* sem_ch13.adb
	(Aspect_Loop): do not raise error on duplicate Test_Case aspect
	(Analyze_Aspect_Specifications): analyze Test_Case aspect and create
	corresponding pragma
	(Check_Aspect_At_Freeze_Point): raise Program_Error on Test_Case aspect
	* sem_ch3.adb (Analyze_Declarations): insert analysis of test-cases,
	similar to the analysis of pre/post
	(Derive_Subprogram): insert contract in subprogram node at point of
	derivation.
	* sem_prag.adb, sem_prag.ads
	(Check_Arg_Is_String_Literal, Check_Identifier):
	new checking procedures to be called in treatment of pragmas
	(Check_Test_Case): new procedure to check that a Test_Case aspect or
	pragma is well-formed. This does not check currently that 'Result is
	used only in the Ensures component of a Test_Case.
	(Analyze_Pragma): add case for Test_Case
	(Analyze_TC_In_Decl_Part): pre-analyze the Requires and Ensures
	components of a Test_Case.
	(Preanalyze_TC_Args): new procedure to preanalyze the boolean
	expressions in the 3rd (and 4th if present) arguments of a Test_Case
	pragma, treated as spec expressions.
	(Sig_Flags): add value -1 for Test_Case.
	* sem_util.adb, sem_util.ads (Get_Ensures_From_Test_Case_Pragma,
	Get_Requires_From_Test_Case_Pragma): getters for both expression
	components of a Test_Case.
	* sinfo.adb, sinfo.ads (N_Contract): new kind of node used as
	indirection between an entry or [generic] subprogram entity and its
	pre/post + test-cases.
	(Spec_PPC_List, Spec_TC_List, Set_Spec_PPC_List, Set_Spec_TC_List):
	get/set for fields of an N_Contract node.
	* snames.ads-tmpl (Name_Test_Case, Name_Ensures, Name_Mode,
	Name_Normal, Name_Requires, Name_Robustness, Pragma_Test_Case): new
	names and pragma for Test_Case.
	* sprint.adb (Sprint_Node): raise Program_Error on N_Contract node
diff mbox

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 177378)
+++ sem_ch3.adb	(working copy)
@@ -2180,11 +2180,18 @@ 
             if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
                Spec := Specification (Original_Node (Decl));
                Sent := Defining_Unit_Name (Spec);
-               Prag := Spec_PPC_List (Sent);
+
+               Prag := Spec_PPC_List (Contract (Sent));
                while Present (Prag) loop
                   Analyze_PPC_In_Decl_Part (Prag, Sent);
                   Prag := Next_Pragma (Prag);
                end loop;
+
+               Prag := Spec_TC_List (Contract (Sent));
+               while Present (Prag) loop
+                  Analyze_TC_In_Decl_Part (Prag, Sent);
+                  Prag := Next_Pragma (Prag);
+               end loop;
             end if;
 
             Next (Decl);
@@ -13001,6 +13008,7 @@ 
       New_Subp :=
          New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type));
       Set_Ekind (New_Subp, Ekind (Parent_Subp));
+      Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp)));
 
       --  Check whether the inherited subprogram is a private operation that
       --  should be inherited but not yet made visible. Such subprograms can
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 177371)
+++ gnat_rm.texi	(working copy)
@@ -203,6 +203,7 @@ 
 * Pragma Task_Info::
 * Pragma Task_Name::
 * Pragma Task_Storage::
+* Pragma Test_Case::
 * Pragma Thread_Local_Storage::
 * Pragma Time_Slice::
 * Pragma Title::
@@ -835,6 +836,7 @@ 
 * Pragma Task_Info::
 * Pragma Task_Name::
 * Pragma Task_Storage::
+* Pragma Test_Case::
 * Pragma Thread_Local_Storage::
 * Pragma Time_Slice::
 * Pragma Title::
@@ -3967,7 +3969,7 @@ 
 must be true may contain references to function'Result in the case
 of a function to refer to the returned value.
 
-@code{Postcondition} pragmas may appear either immediate following the
+@code{Postcondition} pragmas may appear either immediately following the
 (separate) declaration of a subprogram, or at the start of the
 declarations of a subprogram body. Only other pragmas may intervene
 (that is appear between the subprogram declaration and its
@@ -4133,7 +4135,7 @@ 
 @end smallexample
 
 @noindent
-@code{Precondition} pragmas may appear either immediate following the
+@code{Precondition} pragmas may appear either immediately following the
 (separate) declaration of a subprogram, or at the start of the
 declarations of a subprogram body. Only other pragmas may intervene
 (that is appear between the subprogram declaration and its
@@ -5007,6 +5009,58 @@ 
 @code{Storage_Size} attribute definition clause is allowed for a task
 type.
 
+@node Pragma Test_Case
+@unnumberedsec Pragma Test_Case
+@cindex Test cases
+@findex Test_Case
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Test_Case (
+   [Name     =>] String_Expression
+  ,[Mode     =>] (Normal | Robustness)
+ [, Requires =>  Boolean_Expression]
+ [, Ensures  =>  Boolean_Expression]);
+@end smallexample
+
+@noindent
+The @code{Test_Case} pragma applies to the same entities as pragmas
+@code{Precondition} and @code{Postcondition}. In particular, the
+placement and visibility rules are identical to those described for pre-
+and postconditions. But the presence of pragma @code{Test_Case} does not
+lead to any modification of the code generated by the compiler. Rather,
+its purpose is to document finer-grain specifications for use by testing
+and verification tools.
+
+The compiler checks that boolean expression 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 Test_Case (Name     => ``Test_1``,
+                     Mode     => Normal,
+                     Requires => Arg < 100,
+                     Ensures  => Sqrt'Result < 10);
+   ...
+end Math_Functions;
+@end smallexample
+
+@noindent
+@code{Test_Case} pragmas may appear either immediately following the
+(separate) declaration of a subprogram, or at the start of the
+declarations of a subprogram body. Only other pragmas may intervene
+(that is appear between the subprogram declaration and its test cases,
+or appear before the test case in the declaration sequence in a
+subprogram body).
+
 @node Pragma Thread_Local_Storage
 @unnumberedsec Pragma Thread_Local_Storage
 @findex Thread_Local_Storage
@@ -16589,6 +16643,7 @@ 
 @item @code{Stream_Size} @tab
 @item @code{Suppress} @tab
 @item @code{Suppress_Debug_Info} @tab           -- GNAT
+@item @code{Test_Case} @tab                     -- GNAT
 @item @code{Unchecked_Union} @tab
 @item @code{Universal_Aliasing} @tab            -- GNAT
 @item @code{Unmodified} @tab                    -- GNAT
Index: exp_util.adb
===================================================================
--- exp_util.adb	(revision 177378)
+++ exp_util.adb	(working copy)
@@ -3186,6 +3186,11 @@ 
                      null;
                   end if;
 
+            --  A contract node should not belong to the tree
+
+            when N_Contract =>
+               raise Program_Error;
+
             --  For all other node types, keep climbing tree
 
             when
Index: sinfo.adb
===================================================================
--- sinfo.adb	(revision 177349)
+++ sinfo.adb	(working copy)
@@ -2766,6 +2766,22 @@ 
       return Node1 (N);
    end Source_Type;
 
+   function Spec_PPC_List
+      (N : Node_Id) return Node_Id is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Contract);
+      return Node1 (N);
+   end Spec_PPC_List;
+
+   function Spec_TC_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;
+
    function Specification
       (N : Node_Id) return Node_Id is
    begin
@@ -5792,6 +5808,22 @@ 
       Set_Node1 (N, Val); -- semantic field, no parent set
    end Set_Source_Type;
 
+   procedure Set_Spec_PPC_List
+      (N : Node_Id; Val : Node_Id) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Contract);
+      Set_Node1 (N, Val); -- semantic field, no parent set
+   end Set_Spec_PPC_List;
+
+   procedure Set_Spec_TC_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;
+
    procedure Set_Specification
       (N : Node_Id; Val : Node_Id) is
    begin
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 177379)
+++ sinfo.ads	(working copy)
@@ -1694,12 +1694,12 @@ 
    --    which gigi must do size validation for.
 
    --  Split_PPC (Flag17)
-   --     When a Pre or Postaspect specification is processed, it is broken
-   --     into AND THEN sections. The left most section has Split_PPC set to
-   --     False, indicating that it is the original specification (e.g. for
-   --     posting errors). For other sections, Split_PPC is set to True.
-   --     This flag is set in both the N_Aspect_Specification node itself,
-   --     and in the pragma which is generated from this node.
+   --    When a Pre or Post aspect specification is processed, it is broken
+   --    into AND THEN sections. The left most section has Split_PPC set to
+   --    False, indicating that it is the original specification (e.g. for
+   --    posting errors). For other sections, Split_PPC is set to True.
+   --    This flag is set in both the N_Aspect_Specification node itself,
+   --    and in the pragma which is generated from this node.
 
    --  Static_Processing_OK (Flag4-Sem)
    --    Present in N_Aggregate nodes. When the Compile_Time_Known_Aggregate
@@ -6894,6 +6894,39 @@ 
       --  Is_Elsif (Flag13) (set if comes from ELSIF)
       --  plus fields for expression
 
+      --------------
+      -- Contract --
+      --------------
+
+      --  This node is used to hold the various parts of an entry or subprogram
+      --  contract, consisting in pre- and postconditions on the one hand, and
+      --  test-cases on the other hand.
+
+      --  It is referenced from an entry, a subprogram or a generic subprogram
+      --  entity.
+
+      --  Sprint syntax:  <none> as the node should not appear in the tree, but
+      --                  only attached to an entry or [generic] subprogram
+      --                  entity.
+
+      --  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_PPC_List points to a list of Precondition and Postcondition
+      --  pragma nodes for preconditions and postconditions 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 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.
+
       -------------------
       -- Expanded_Name --
       -------------------
@@ -7746,6 +7779,7 @@ 
       N_Component_Association,
       N_Component_Definition,
       N_Component_List,
+      N_Contract,
       N_Derived_Type_Definition,
       N_Decimal_Fixed_Point_Definition,
       N_Defining_Program_Unit_Name,
@@ -8850,6 +8884,12 @@ 
    function Source_Type
      (N : Node_Id) return Entity_Id;  -- Node1
 
+   function Spec_PPC_List
+     (N : Node_Id) return Node_Id;    -- Node1
+
+   function Spec_TC_List
+     (N : Node_Id) return Node_Id;    -- Node2
+
    function Specification
      (N : Node_Id) return Node_Id;    -- Node1
 
@@ -9813,6 +9853,12 @@ 
    procedure Set_Source_Type
      (N : Node_Id; Val : Entity_Id);          -- Node1
 
+   procedure Set_Spec_PPC_List
+     (N : Node_Id; Val : Node_Id);            -- Node1
+
+   procedure Set_Spec_TC_List
+     (N : Node_Id; Val : Node_Id);            -- Node2
+
    procedure Set_Specification
      (N : Node_Id; Val : Node_Id);            -- Node1
 
@@ -11447,6 +11493,13 @@ 
         4 => False,   --  unused
         5 => False),  --  Etype (Node5-Sem)
 
+     N_Contract =>
+       (1 => False,   --  Spec_PPC_List (Node1)
+        2 => False,   --  Spec_TC_List (Node2)
+        3 => False,   --  unused
+        4 => False,   --  unused
+        5 => False),  --  unused
+
      N_Expanded_Name =>
        (1 => True,    --  Chars (Name1)
         2 => True,    --  Selector_Name (Node2)
@@ -11931,6 +11984,8 @@ 
    pragma Inline (Selector_Names);
    pragma Inline (Shift_Count_OK);
    pragma Inline (Source_Type);
+   pragma Inline (Spec_PPC_List);
+   pragma Inline (Spec_TC_List);
    pragma Inline (Specification);
    pragma Inline (Split_PPC);
    pragma Inline (Statements);
@@ -12248,6 +12303,8 @@ 
    pragma Inline (Set_Selector_Names);
    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_Specification);
    pragma Inline (Set_Split_PPC);
    pragma Inline (Set_Statements);
Index: exp_ch9.adb
===================================================================
--- exp_ch9.adb	(revision 177355)
+++ exp_ch9.adb	(working copy)
@@ -1660,7 +1660,7 @@ 
          P : Node_Id;
 
       begin
-         P := Spec_PPC_List (E);
+         P := Spec_PPC_List (Contract (E));
          if No (P) then
             return;
          end if;
@@ -10871,7 +10871,7 @@ 
          Ent := First_Entity (Tasktyp);
          while Present (Ent) loop
             if Ekind_In (Ent, E_Entry, E_Entry_Family)
-              and then Present (Spec_PPC_List (Ent))
+              and then Present (Spec_PPC_List (Contract (Ent)))
             then
                Build_PPC_Wrapper (Ent, N);
             end if;
Index: sem_ch9.adb
===================================================================
--- sem_ch9.adb	(revision 177353)
+++ sem_ch9.adb	(working copy)
@@ -885,6 +885,7 @@ 
 
    begin
       Generate_Definition (Def_Id);
+      Set_Contract (Def_Id, Make_Contract (Sloc (Def_Id)));
       Tasking_Used := True;
 
       --  Case of no discrete subtype definition
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 177378)
+++ einfo.adb	(working copy)
@@ -209,7 +209,7 @@ 
 
    --    Finalizer                       Node24
    --    Related_Expression              Node24
-   --    Spec_PPC_List                   Node24
+   --    Contract                        Node24
 
    --    Interface_Alias                 Node25
    --    Interfaces                      Elist25
@@ -982,6 +982,15 @@ 
       return Node18 (Id);
    end Entry_Index_Constant;
 
+   function Contract (Id : E) return N is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Entry, E_Entry_Family)
+          or else Is_Subprogram (Id)
+          or else Is_Generic_Subprogram (Id));
+      return Node24 (Id);
+   end Contract;
+
    function Entry_Parameters_Type (Id : E) return E is
    begin
       return Node15 (Id);
@@ -2650,15 +2659,6 @@ 
       return Node19 (Id);
    end Spec_Entity;
 
-   function Spec_PPC_List (Id : E) return N is
-   begin
-      pragma Assert
-        (Ekind_In (Id,  E_Entry, E_Entry_Family)
-          or else Is_Subprogram (Id)
-          or else Is_Generic_Subprogram (Id));
-      return Node24 (Id);
-   end Spec_PPC_List;
-
    function Static_Predicate (Id : E) return S is
    begin
       pragma Assert (Is_Discrete_Type (Id));
@@ -3451,6 +3451,15 @@ 
       Set_Node18 (Id, V);
    end Set_Entry_Index_Constant;
 
+   procedure Set_Contract (Id : E; V : N) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void)
+          or else Is_Subprogram (Id)
+          or else Is_Generic_Subprogram (Id));
+      Set_Node24 (Id, V);
+   end Set_Contract;
+
    procedure Set_Entry_Parameters_Type (Id : E; V : E) is
    begin
       Set_Node15 (Id, V);
@@ -5189,15 +5198,6 @@ 
       Set_Node19 (Id, V);
    end Set_Spec_Entity;
 
-   procedure Set_Spec_PPC_List (Id : E; V : N) is
-   begin
-      pragma Assert
-        (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void)
-          or else Is_Subprogram (Id)
-          or else Is_Generic_Subprogram (Id));
-      Set_Node24 (Id, V);
-   end Set_Spec_PPC_List;
-
    procedure Set_Static_Predicate (Id : E; V : S) is
    begin
       pragma Assert
@@ -8534,8 +8534,11 @@ 
               Type_Kind                                    =>
             Write_Str ("Related_Expression");
 
-         when Subprogram_Kind                              =>
-            Write_Str ("Spec_PPC_List");
+         when E_Entry                                      |
+              E_Entry_Family                               |
+              Subprogram_Kind                              |
+              Generic_Subprogram_Kind                      =>
+            Write_Str ("Contract");
 
          when others                                       =>
             Write_Str ("Field24???");
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 177378)
+++ einfo.ads	(working copy)
@@ -1009,6 +1009,11 @@ 
 --       accept statement for a member of the family, and in the prefix of
 --       'COUNT when it applies to a family member.
 
+--    Contract (Node24)
+--       Present in entries, and in subprogram and generic subprogram entities.
+--       Points to the contract of the entity, holding both pre- and
+--       postconditions as well as test-cases.
+
 --    Entry_Parameters_Type (Node15)
 --       Present in entries. Points to the access-to-record type that is
 --       constructed by the expander to hold a reference to the parameter
@@ -3641,14 +3646,6 @@ 
 --       case where there is a separate spec, where this field references
 --       the corresponding parameter entities in the spec.
 
---    Spec_PPC_List (Node24)
---       Present in entries, and in subprogram and generic subprogram entities.
---       Points to a list of Precondition and Postcondition pragma nodes for
---       preconditions and postconditions declared in the spec. The last pragma
---       encountered is at the head of this list, so it is in reverse order of
---       textual appearance. Note that this includes precondition/postcondition
---       pragmas generated to correspond to Pre/Post aspects.
-
 --    Static_Predicate (List25)
 --       Present in discrete types/subtypes with predicates (Has_Predicates
 --       set True). Points to a list of expression and N_Range nodes that
@@ -5126,7 +5123,7 @@ 
    --    Accept_Address                      (Elist21)
    --    Scope_Depth_Value                   (Uint22)
    --    Protection_Object                   (Node23)   (protected kind)
-   --    Spec_PPC_List                       (Node24)   (for entry only)
+   --    Contract                            (Node24)   (for entry only)
    --    PPC_Wrapper                         (Node25)
    --    Default_Expressions_Processed       (Flag108)
    --    Entry_Accepted                      (Flag152)
@@ -5226,7 +5223,7 @@ 
    --    Generic_Renamings                   (Elist23)  (for an instance)
    --    Inner_Instances                     (Elist23)  (generic case only)
    --    Protection_Object                   (Node23)   (for concurrent kind)
-   --    Spec_PPC_List                       (Node24)
+   --    Contract                            (Node24)
    --    Interface_Alias                     (Node25)
    --    Overridden_Operation                (Node26)
    --    Wrapped_Entity                      (Node27)   (non-generic case only)
@@ -5490,7 +5487,7 @@ 
    --    Generic_Renamings                   (Elist23)  (for an instance)
    --    Inner_Instances                     (Elist23)  (generic case only)
    --    Protection_Object                   (Node23)   (for concurrent kind)
-   --    Spec_PPC_List                       (Node24)
+   --    Contract                            (Node24)
    --    Interface_Alias                     (Node25)
    --    Static_Initialization               (Node26)   (init_proc only)
    --    Overridden_Operation                (Node26)   (never for init proc)
@@ -6039,6 +6036,7 @@ 
    function Entry_Formal                        (Id : E) return E;
    function Entry_Index_Constant                (Id : E) return E;
    function Entry_Index_Type                    (Id : E) return E;
+   function Contract                            (Id : E) return N;
    function Entry_Parameters_Type               (Id : E) return E;
    function Enum_Pos_To_Rep                     (Id : E) return E;
    function Enumeration_Pos                     (Id : E) return U;
@@ -6333,7 +6331,6 @@ 
    function Size_Depends_On_Discriminant        (Id : E) return B;
    function Small_Value                         (Id : E) return R;
    function Spec_Entity                         (Id : E) return E;
-   function Spec_PPC_List                       (Id : E) return N;
    function Static_Predicate                    (Id : E) return S;
    function Storage_Size_Variable               (Id : E) return E;
    function Static_Elaboration_Desired          (Id : E) return B;
@@ -6626,6 +6623,7 @@ 
    procedure Set_Entry_Component                 (Id : E; V : E);
    procedure Set_Entry_Formal                    (Id : E; V : E);
    procedure Set_Entry_Index_Constant            (Id : E; V : E);
+   procedure Set_Contract                        (Id : E; V : N);
    procedure Set_Entry_Parameters_Type           (Id : E; V : E);
    procedure Set_Enum_Pos_To_Rep                 (Id : E; V : E);
    procedure Set_Enumeration_Pos                 (Id : E; V : U);
@@ -6926,7 +6924,6 @@ 
    procedure Set_Size_Known_At_Compile_Time      (Id : E; V : B := True);
    procedure Set_Small_Value                     (Id : E; V : R);
    procedure Set_Spec_Entity                     (Id : E; V : E);
-   procedure Set_Spec_PPC_List                   (Id : E; V : N);
    procedure Set_Static_Predicate                (Id : E; V : S);
    procedure Set_Storage_Size_Variable           (Id : E; V : E);
    procedure Set_Static_Elaboration_Desired      (Id : E; V : B);
@@ -7280,6 +7277,7 @@ 
    pragma Inline (Component_Clause);
    pragma Inline (Component_Size);
    pragma Inline (Component_Type);
+   pragma Inline (Contract);
    pragma Inline (Corresponding_Concurrent_Type);
    pragma Inline (Corresponding_Discriminant);
    pragma Inline (Corresponding_Equality);
@@ -7664,7 +7662,6 @@ 
    pragma Inline (Size_Known_At_Compile_Time);
    pragma Inline (Small_Value);
    pragma Inline (Spec_Entity);
-   pragma Inline (Spec_PPC_List);
    pragma Inline (Static_Predicate);
    pragma Inline (Storage_Size_Variable);
    pragma Inline (Static_Elaboration_Desired);
@@ -7724,6 +7721,7 @@ 
    pragma Inline (Set_Component_Clause);
    pragma Inline (Set_Component_Size);
    pragma Inline (Set_Component_Type);
+   pragma Inline (Set_Contract);
    pragma Inline (Set_Corresponding_Concurrent_Type);
    pragma Inline (Set_Corresponding_Discriminant);
    pragma Inline (Set_Corresponding_Equality);
@@ -8063,7 +8061,6 @@ 
    pragma Inline (Set_Size_Known_At_Compile_Time);
    pragma Inline (Set_Small_Value);
    pragma Inline (Set_Spec_Entity);
-   pragma Inline (Set_Spec_PPC_List);
    pragma Inline (Set_Static_Predicate);
    pragma Inline (Set_Storage_Size_Variable);
    pragma Inline (Set_Static_Elaboration_Desired);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 177353)
+++ sem_prag.adb	(working copy)
@@ -179,6 +179,11 @@ 
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
+   procedure Preanalyze_TC_Args (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).
+
    procedure rv;
    --  This is a dummy function called by the processing for pragma Reviewable.
    --  It is there for assisting front end debugging. By placing a Reviewable
@@ -333,6 +338,10 @@ 
       --  Check the specified argument Arg to make sure that it is an integer
       --  literal. If not give error and raise Pragma_Exit.
 
+      procedure Check_Arg_Is_String_Literal (Arg : Node_Id);
+      --  Check the specified argument Arg to make sure that it is a string
+      --  literal. If not give error and raise Pragma_Exit.
+
       procedure Check_Arg_Is_Library_Level_Local_Name (Arg : Node_Id);
       --  Check the specified argument Arg to make sure that it has the proper
       --  syntactic form for a local name and meets the semantic requirements
@@ -410,6 +419,12 @@ 
       --  Checks that Arg, whose expression is an entity name, references a
       --  first subtype.
 
+      procedure Check_Identifier (Arg : Node_Id; Id : Name_Id);
+      --  Checks that the given argument has an identifier, and if so, requires
+      --  it to match the given identifier name. If there is no identifier, or
+      --  a non-matching identifier, then an error message is given and
+      --  Error_Pragmas raised.
+
       procedure Check_In_Main_Program;
       --  Common checks for pragmas that appear within a main program
       --  (Priority, Main_Storage, Time_Slice, Relative_Deadline, CPU).
@@ -478,6 +493,27 @@ 
       --  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.
+      --  There are three cases:
+      --
+      --    The pragma appears after a subprogram spec
+      --
+      --      The first step is to analyze the pragma, but this is skipped if
+      --      the subprogram spec appears within a package specification
+      --      (because this is the case where we delay analysis till the end of
+      --      the spec). Then (whether or not it was analyzed), the pragma is
+      --      chained to the subprogram in question (using Spec_TC_List and
+      --      Next_Pragma).
+      --
+      --    The pragma appears at the start of subprogram body declarations
+      --
+      --      In this case an immediate return to the caller is made, and the
+      --      pragma is NOT analyzed.
+      --
+      --    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
 
@@ -860,6 +896,19 @@ 
          end if;
       end Check_Arg_Is_Integer_Literal;
 
+      ---------------------------------
+      -- Check_Arg_Is_String_Literal --
+      ---------------------------------
+
+      procedure Check_Arg_Is_String_Literal (Arg : Node_Id) is
+         Argx : constant Node_Id := Get_Pragma_Arg (Arg);
+      begin
+         if Nkind (Argx) /= N_String_Literal then
+            Error_Pragma_Arg
+              ("argument for pragma% must be string literal", Argx);
+         end if;
+      end Check_Arg_Is_String_Literal;
+
       -------------------------------------------
       -- Check_Arg_Is_Library_Level_Local_Name --
       -------------------------------------------
@@ -1036,6 +1085,7 @@ 
             Error_Pragma_Arg ("invalid argument for pragma%", Argx);
          end if;
       end Check_Arg_Is_One_Of;
+
       ---------------------------------
       -- Check_Arg_Is_Queuing_Policy --
       ---------------------------------
@@ -1364,6 +1414,24 @@ 
          end if;
       end Check_First_Subtype;
 
+      ----------------------
+      -- Check_Identifier --
+      ----------------------
+
+      procedure Check_Identifier (Arg : Node_Id; Id : Name_Id) is
+      begin
+         if Present (Arg)
+           and then Nkind (Arg) = N_Pragma_Argument_Association
+         then
+            if Chars (Arg) = No_Name or else Chars (Arg) /= Id then
+               Error_Msg_Name_1 := Pname;
+               Error_Msg_Name_2 := Id;
+               Error_Msg_N ("pragma% argument expects identifier%", Arg);
+               raise Pragma_Exit;
+            end if;
+         end if;
+      end Check_Identifier;
+
       ---------------------------
       -- Check_In_Main_Program --
       ---------------------------
@@ -1571,10 +1639,10 @@ 
          PO : Node_Id;
 
          procedure Chain_PPC (PO : Node_Id);
-         --  If PO is a subprogram declaration node (or a generic subprogram
-         --  declaration node), then the precondition/postcondition applies
-         --  to this subprogram and the processing for the pragma is completed.
-         --  Otherwise the pragma is misplaced.
+         --  If PO is an entry or a [generic] subprogram declaration node, then
+         --  the precondition/postcondition applies to this subprogram and the
+         --  processing for the pragma is completed. Otherwise the pragma is
+         --  misplaced.
 
          ---------------
          -- Chain_PPC --
@@ -1637,7 +1705,7 @@ 
 
             if Pragma_Name (N) = Name_Precondition then
                if not From_Aspect_Specification (N) then
-                  P := Spec_PPC_List (S);
+                  P := Spec_PPC_List (Contract (S));
                   while Present (P) loop
                      if Pragma_Name (P) = Name_Precondition
                        and then From_Aspect_Specification (P)
@@ -1666,7 +1734,7 @@ 
 
                begin
                   for J in Inherited'Range loop
-                     P := Spec_PPC_List (Inherited (J));
+                     P := Spec_PPC_List (Contract (Inherited (J)));
                      while Present (P) loop
                         if Pragma_Name (P) = Name_Precondition
                           and then Class_Present (P)
@@ -1691,8 +1759,8 @@ 
 
             --  Chain spec PPC pragma to list for subprogram
 
-            Set_Next_Pragma (N, Spec_PPC_List (S));
-            Set_Spec_PPC_List (S, N);
+            Set_Next_Pragma (N, Spec_PPC_List (Contract (S)));
+            Set_Spec_PPC_List (Contract (S), N);
 
             --  Return indicating spec case
 
@@ -1870,6 +1938,135 @@ 
          end case;
       end Check_Static_Constraint;
 
+      ---------------------
+      -- Check_Test_Case --
+      ---------------------
+
+      procedure Check_Test_Case is
+         P  : Node_Id;
+         PO : Node_Id;
+
+         procedure Chain_TC (PO : Node_Id);
+         --  If PO is an entry or 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.
+
+         --------------
+         -- Chain_TC --
+         --------------
+
+         procedure Chain_TC (PO : Node_Id) is
+            S   : Entity_Id;
+
+         begin
+            if Nkind (PO) = N_Abstract_Subprogram_Declaration then
+               if From_Aspect_Specification (N) then
+                  Error_Pragma
+                    ("aspect% cannot be applied to abstract subprogram");
+               else
+                  Error_Pragma
+                    ("pragma% cannot be applied to abstract subprogram");
+               end if;
+
+            elsif not Nkind_In (PO, N_Subprogram_Declaration,
+                                    N_Generic_Subprogram_Declaration,
+                                    N_Entry_Declaration)
+            then
+               Pragma_Misplaced;
+            end if;
+
+            --  Here if we have [generic] subprogram or entry declaration
+
+            if Nkind (PO) = N_Entry_Declaration then
+               S := Defining_Entity (PO);
+            else
+               S := Defining_Unit_Name (Specification (PO));
+            end if;
+
+            --  Note: we do not analyze the pragma at this point. Instead we
+            --  delay this analysis until the end of the declarative part in
+            --  which the pragma appears. This implements the required delay
+            --  in this analysis, allowing forward references. The analysis
+            --  happens at the end of Analyze_Declarations.
+
+            --  Chain spec TC pragma to list for subprogram
+
+            Set_Next_Pragma (N, Spec_TC_List (Contract (S)));
+            Set_Spec_TC_List (Contract (S), N);
+         end Chain_TC;
+
+      --  Start of processing for Check_Test_Case
+
+      begin
+         if not Is_List_Member (N) then
+            Pragma_Misplaced;
+         end if;
+
+         --  Search prior declarations
+
+         P := N;
+         while Present (Prev (P)) loop
+            P := Prev (P);
+
+            --  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.
+
+            if Nkind (P) not in N_Generic_Declaration then
+               PO := Original_Node (P);
+            else
+               PO := P;
+            end if;
+
+            --  Skip past prior pragma
+
+            if Nkind (PO) = N_Pragma then
+               null;
+
+            --  Skip stuff not coming from source
+
+            elsif not Comes_From_Source (PO) then
+               null;
+
+            --  Only remaining possibility is subprogram declaration
+
+            else
+               Chain_TC (PO);
+               return;
+            end if;
+         end loop;
+
+         --  If we fall through loop, pragma is at start of list, so see if it
+         --  is at the start of declarations of a subprogram body.
+
+         if Nkind (Parent (N)) = N_Subprogram_Body
+           and then List_Containing (N) = Declarations (Parent (N))
+         then
+            if Operating_Mode /= Generate_Code
+              or else Inside_A_Generic
+            then
+               --  Analyze pragma expressions for correctness and for ASIS use
+
+               Preanalyze_TC_Args (Get_Requires_From_Test_Case_Pragma (N),
+                                   Get_Ensures_From_Test_Case_Pragma (N));
+            end if;
+
+            return;
+
+         --  See if it is in the pragmas after a library level subprogram
+
+         elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+            Chain_TC (Unit (Parent (Parent (N))));
+            return;
+         end if;
+
+         --  If we fall through, pragma was misplaced
+
+         Pragma_Misplaced;
+      end Check_Test_Case;
+
       --------------------------------------
       -- Check_Valid_Configuration_Pragma --
       --------------------------------------
@@ -12904,9 +13101,9 @@ 
             end if;
          end;
 
-         --------------
+         ---------------
          -- Task_Info --
-         --------------
+         ---------------
 
          --  pragma Task_Info (EXPRESSION);
 
@@ -13023,6 +13220,38 @@ 
             end if;
          end Task_Storage;
 
+         ---------------
+         -- Test_Case --
+         ---------------
+
+         --  pragma Test_Case ([Name     =>] String_Expression
+         --                   ,[Mode     =>] (Normal | Robustness)
+         --                  [, Requires =>  Boolean_Expression]
+         --                  [, Ensures  =>  Boolean_Expression]);
+
+         when Pragma_Test_Case => Test_Case : declare
+
+         begin
+            GNAT_Pragma;
+            Check_At_Least_N_Arguments (3);
+            Check_At_Most_N_Arguments (4);
+            Check_Arg_Order
+              ((Name_Name, Name_Mode, Name_Requires, Name_Ensures));
+
+            Check_Optional_Identifier (Arg1, Name_Name);
+            Check_Arg_Is_String_Literal (Arg1);
+            Check_Optional_Identifier (Arg2, Name_Mode);
+            Check_Arg_Is_One_Of (Arg2, Name_Normal, Name_Robustness);
+            if Arg_Count = 4 then
+               Check_Identifier (Arg3, Name_Requires);
+               Check_Identifier (Arg4, Name_Ensures);
+            else
+               Check_Arg_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
+            end if;
+
+            Check_Test_Case;
+         end Test_Case;
+
          --------------------------
          -- Thread_Local_Storage --
          --------------------------
@@ -13887,6 +14116,30 @@ 
       when Pragma_Exit => null;
    end Analyze_Pragma;
 
+   -----------------------------
+   -- Analyze_TC_In_Decl_Part --
+   -----------------------------
+
+   procedure Analyze_TC_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.
+
+      Install_Formals (S);
+      Push_Scope (S);
+
+      --  Preanalyze the boolean expressions, we treat these as spec
+      --  expressions (i.e. similar to a default expression).
+
+      Preanalyze_TC_Args (Get_Requires_From_Test_Case_Pragma (N),
+                          Get_Ensures_From_Test_Case_Pragma (N));
+
+      --  Remove the subprogram from the scope stack now that the pre-analysis
+      --  of the expressions in the test-case is done.
+
+      End_Scope;
+   end Analyze_TC_In_Decl_Part;
+
    -------------------
    -- Check_Enabled --
    -------------------
@@ -14214,6 +14467,7 @@ 
       Pragma_Task_Info                     => -1,
       Pragma_Task_Name                     => -1,
       Pragma_Task_Storage                  =>  0,
+      Pragma_Test_Case                     => -1,
       Pragma_Thread_Local_Storage          =>  0,
       Pragma_Time_Slice                    => -1,
       Pragma_Title                         => -1,
@@ -14355,6 +14609,26 @@ 
       end if;
    end Is_Pragma_String_Literal;
 
+   ------------------------
+   -- Preanalyze_TC_Args --
+   ------------------------
+
+   procedure Preanalyze_TC_Args (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).
+
+      if Present (Arg_Req) then
+         Preanalyze_Spec_Expression
+           (Get_Pragma_Arg (Arg_Req), Standard_Boolean);
+      end if;
+
+      if Present (Arg_Ens) then
+         Preanalyze_Spec_Expression
+           (Get_Pragma_Arg (Arg_Ens), Standard_Boolean);
+      end if;
+   end Preanalyze_TC_Args;
+
    --------------------------------------
    -- Process_Compilation_Unit_Pragmas --
    --------------------------------------
Index: sem_prag.ads
===================================================================
--- sem_prag.ads	(revision 177274)
+++ sem_prag.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -46,6 +46,14 @@ 
    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...").
+
    function Check_Enabled (Nam : Name_Id) return Boolean;
    --  This function is used in connection with pragmas Assertion, Check,
    --  Precondition, and Postcondition to determine if Check pragmas (or
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 177378)
+++ sem_ch12.adb	(working copy)
@@ -2839,6 +2839,7 @@ 
       Spec := Specification (N);
       Id := Defining_Entity (Spec);
       Generate_Definition (Id);
+      Set_Contract (Id, Make_Contract (Sloc (Id)));
 
       if Nkind (Id) = N_Defining_Operator_Symbol then
          Error_Msg_N
@@ -4367,6 +4368,8 @@ 
          end if;
 
          Generate_Definition (Act_Decl_Id);
+         Set_Contract (Anon_Id, Make_Contract (Sloc (Anon_Id))); -- ??? needed?
+         Set_Contract (Act_Decl_Id, Make_Contract (Sloc (Act_Decl_Id)));
 
          Set_Is_Inlined (Act_Decl_Id, Is_Inlined (Gen_Unit));
          Set_Is_Inlined (Anon_Id,     Is_Inlined (Gen_Unit));
Index: sem.adb
===================================================================
--- sem.adb	(revision 177274)
+++ sem.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -650,6 +650,7 @@ 
            N_Component_Definition                   |
            N_Component_List                         |
            N_Constrained_Array_Definition           |
+           N_Contract                               |
            N_Decimal_Fixed_Point_Definition         |
            N_Defining_Character_Literal             |
            N_Defining_Identifier                    |
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 177383)
+++ sem_util.adb	(working copy)
@@ -4223,6 +4223,28 @@ 
       end if;
    end Get_Enum_Lit_From_Pos;
 
+   ---------------------------------------
+   -- Get_Ensures_From_Test_Case_Pragma --
+   ---------------------------------------
+
+   function Get_Ensures_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+      Args : constant List_Id := Pragma_Argument_Associations (N);
+      Res  : Node_Id;
+
+   begin
+      if List_Length (Args) = 4 then
+         Res := Pick (Args, 4);
+
+      else
+         Res := Pick (Args, 3);
+         if Chars (Res) /= Name_Ensures then
+            Res := Empty;
+         end if;
+      end if;
+
+      return Res;
+   end Get_Ensures_From_Test_Case_Pragma;
+
    ------------------------
    -- Get_Generic_Entity --
    ------------------------
@@ -4352,6 +4374,23 @@ 
       return R;
    end Get_Renamed_Entity;
 
+   ----------------------------------------
+   -- Get_Requires_From_Test_Case_Pragma --
+   ----------------------------------------
+
+   function Get_Requires_From_Test_Case_Pragma (N : Node_Id) return Node_Id is
+      Args : constant List_Id := Pragma_Argument_Associations (N);
+      Res  : Node_Id;
+
+   begin
+      Res := Pick (Args, 3);
+      if Chars (Res) /= Name_Requires then
+         Res := Empty;
+      end if;
+
+      return Res;
+   end Get_Requires_From_Test_Case_Pragma;
+
    -------------------------
    -- Get_Subprogram_Body --
    -------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 177383)
+++ sem_util.ads	(working copy)
@@ -484,6 +484,9 @@ 
    --  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 components of 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
    --  instantiation is a renaming, the function returns the renamed generic.
@@ -530,6 +533,9 @@ 
    --  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 components of 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
    --  accept statement node. This procedure finds the Entity_Id of the related
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 177367)
+++ sem_attr.adb	(working copy)
@@ -4046,12 +4046,32 @@ 
                Prag := Parent (Prag);
             end loop;
 
-            if Nkind (Prag) /= N_Pragma
-              or else Get_Pragma_Id (Prag) /= Pragma_Postcondition
-            then
+            if Nkind (Prag) /= N_Pragma then
                Error_Attr
                  ("% attribute can only appear in postcondition of function",
                   P);
+
+            elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
+               declare
+                  Arg_Ens : constant Node_Id :=
+                              Get_Ensures_From_Test_Case_Pragma (Prag);
+                  Arg     : Node_Id;
+
+               begin
+                  Arg := N;
+                  while Arg /= Prag and Arg /= Arg_Ens loop
+                     Arg := Parent (Arg);
+                  end loop;
+
+                  if Arg /= Arg_Ens then
+                     Error_Attr ("% attribute misplaced inside Test_Case", P);
+                  end if;
+               end;
+
+            elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then
+               Error_Attr
+                 ("% attribute can only appear in postcondition of function",
+                  P);
             end if;
 
             --  The attribute reference is a primary. If expressions follow,
Index: aspects.adb
===================================================================
--- aspects.adb	(revision 177274)
+++ aspects.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---            Copyright (C) 2010, Free Software Foundation, Inc.            --
+--          Copyright (C) 2010-2011, 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- --
@@ -222,6 +222,7 @@ 
     Aspect_Stream_Size                  => Aspect_Stream_Size,
     Aspect_Suppress                     => Aspect_Suppress,
     Aspect_Suppress_Debug_Info          => Aspect_Suppress_Debug_Info,
+    Aspect_Test_Case                    => Aspect_Test_Case,
     Aspect_Type_Invariant               => Aspect_Invariant,
     Aspect_Unchecked_Union              => Aspect_Unchecked_Union,
     Aspect_Universal_Aliasing           => Aspect_Universal_Aliasing,
Index: aspects.ads
===================================================================
--- aspects.ads	(revision 177274)
+++ aspects.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---            Copyright (C) 2010, Free Software Foundation, Inc.            --
+--         Copyright (C) 2010-2011, 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- --
@@ -69,6 +69,7 @@ 
       Aspect_Storage_Size,
       Aspect_Stream_Size,
       Aspect_Suppress,
+      Aspect_Test_Case,                     -- GNAT
       Aspect_Type_Invariant,
       Aspect_Unsuppress,
       Aspect_Value_Size,                    -- GNAT
@@ -128,6 +129,13 @@ 
                         Aspect_Post          => True,
                         others               => False);
 
+   --  The following array indicates aspects for which multiple occurrences of
+   --  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);
+
    --  The following subtype defines aspects corresponding to library unit
    --  pragmas, these can only validly appear as aspects for library units,
    --  and result in a corresponding pragma being inserted immediately after
@@ -185,6 +193,7 @@ 
                         Aspect_Storage_Size            => Expression,
                         Aspect_Stream_Size             => Expression,
                         Aspect_Suppress                => Name,
+                        Aspect_Test_Case               => Expression,
                         Aspect_Type_Invariant          => Expression,
                         Aspect_Unsuppress              => Name,
                         Aspect_Value_Size              => Expression,
@@ -252,6 +261,7 @@ 
      Aspect_Stream_Size                  => Name_Stream_Size,
      Aspect_Suppress                     => Name_Suppress,
      Aspect_Suppress_Debug_Info          => Name_Suppress_Debug_Info,
+     Aspect_Test_Case                    => Name_Test_Case,
      Aspect_Type_Invariant               => Name_Type_Invariant,
      Aspect_Unchecked_Union              => Name_Unchecked_Union,
      Aspect_Universal_Aliasing           => Name_Universal_Aliasing,
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 177382)
+++ sem_ch6.adb	(working copy)
@@ -230,6 +230,7 @@ 
       Check_SPARK_Restriction ("abstract subprogram is not allowed", N);
 
       Generate_Definition (Designator);
+      Set_Contract (Designator, Make_Contract (Sloc (Designator)));
       Set_Is_Abstract_Subprogram (Designator);
       New_Overloaded_Entity (Designator);
       Check_Delayed_Subprogram (Designator);
@@ -2539,6 +2540,7 @@ 
          if Nkind (N) /= N_Subprogram_Body_Stub then
             Set_Acts_As_Spec (N);
             Generate_Definition (Body_Id);
+            Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
             Generate_Reference
               (Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
             Generate_Reference_To_Formals (Body_Id);
@@ -2981,6 +2983,7 @@ 
 
       Designator := Analyze_Subprogram_Specification (Specification (N));
       Generate_Definition (Designator);
+      --  ??? why this call, already in Analyze_Subprogram_Specification
 
       if Debug_Flag_C then
          Write_Str ("==> subprogram spec ");
@@ -3170,6 +3173,7 @@ 
       --  Proceed with analysis
 
       Generate_Definition (Designator);
+      Set_Contract (Designator, Make_Contract (Sloc (Designator)));
 
       if Nkind (N) = N_Function_Specification then
          Set_Ekind (Designator, E_Function);
@@ -7300,7 +7304,8 @@ 
 
          begin
             for J in Inherited'Range loop
-               P := Spec_PPC_List (Inherited (J));
+               P := Spec_PPC_List (Contract (Inherited (J)));
+
                while Present (P) loop
                   Error_Msg_Sloc := Sloc (P);
 
@@ -9193,7 +9198,7 @@ 
          --  the body will be analyzed and converted when we scan the body
          --  declarations below.
 
-         Prag := Spec_PPC_List (Spec_Id);
+         Prag := Spec_PPC_List (Contract (Spec_Id));
          while Present (Prag) loop
             if Pragma_Name (Prag) = Name_Precondition then
 
@@ -9222,7 +9227,7 @@ 
          --  Now deal with inherited preconditions
 
          for J in Inherited'Range loop
-            Prag := Spec_PPC_List (Inherited (J));
+            Prag := Spec_PPC_List (Contract (Inherited (J)));
 
             while Present (Prag) loop
                if Pragma_Name (Prag) = Name_Precondition
@@ -9402,7 +9407,7 @@ 
 
                --  Loop through PPC pragmas from spec
 
-               Prag := Spec_PPC_List (Spec);
+               Prag := Spec_PPC_List (Contract (Spec));
                loop
                   if Pragma_Name (Prag) = Name_Postcondition
                     and then (not Class or else Class_Present (Prag))
@@ -9427,14 +9432,14 @@ 
          --  Start of processing for Spec_Postconditions
 
          begin
-            if Present (Spec_PPC_List (Spec_Id)) then
+            if Present (Spec_PPC_List (Contract (Spec_Id))) then
                Process_Post_Conditions (Spec_Id, Class => False);
             end if;
 
             --  Process inherited postconditions
 
             for J in Inherited'Range loop
-               if Present (Spec_PPC_List (Inherited (J))) then
+               if Present (Spec_PPC_List (Contract (Inherited (J)))) then
                   Process_Post_Conditions (Inherited (J), Class => True);
                end if;
             end loop;
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 177337)
+++ par-prag.adb	(working copy)
@@ -1239,6 +1239,7 @@ 
            Pragma_Task_Info                     |
            Pragma_Task_Name                     |
            Pragma_Task_Storage                  |
+           Pragma_Test_Case                     |
            Pragma_Thread_Local_Storage          |
            Pragma_Time_Slice                    |
            Pragma_Title                         |
Index: sprint.adb
===================================================================
--- sprint.adb	(revision 177274)
+++ sprint.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -1348,6 +1348,12 @@ 
 
             Sprint_Node (Component_Definition (Node));
 
+         --  A contract node should not appear in the tree. It is a semantic
+         --  node attached to entry and [generic] subprogram entities.
+
+         when N_Contract =>
+            raise Program_Error;
+
          when N_Decimal_Fixed_Point_Definition =>
             Write_Str_With_Col_Check_Sloc (" delta ");
             Sprint_Node (Delta_Expression (Node));
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 177371)
+++ sem_ch13.adb	(working copy)
@@ -812,54 +812,57 @@ 
             --  test allows duplicate Pre/Post's that we generate internally
             --  to escape being flagged here.
 
-            Anod := First (L);
-            while Anod /= Aspect loop
-               if Same_Aspect (A_Id, Get_Aspect_Id (Chars (Identifier (Anod))))
-                 and then Comes_From_Source (Aspect)
-               then
-                  Error_Msg_Name_1 := Nam;
-                  Error_Msg_Sloc := Sloc (Anod);
+            if No_Duplicates_Allowed (A_Id) then
+               Anod := First (L);
+               while Anod /= Aspect loop
+                  if Same_Aspect
+                      (A_Id, Get_Aspect_Id (Chars (Identifier (Anod))))
+                    and then Comes_From_Source (Aspect)
+                  then
+                     Error_Msg_Name_1 := Nam;
+                     Error_Msg_Sloc := Sloc (Anod);
 
-                  --  Case of same aspect specified twice
+                     --  Case of same aspect specified twice
 
-                  if Class_Present (Anod) = Class_Present (Aspect) then
-                     if not Class_Present (Anod) then
-                        Error_Msg_NE
-                          ("aspect% for & previously given#",
-                           Id, E);
-                     else
-                        Error_Msg_NE
-                          ("aspect `%''Class` for & previously given#",
-                           Id, E);
-                     end if;
+                     if Class_Present (Anod) = Class_Present (Aspect) then
+                        if not Class_Present (Anod) then
+                           Error_Msg_NE
+                             ("aspect% for & previously given#",
+                              Id, E);
+                        else
+                           Error_Msg_NE
+                             ("aspect `%''Class` for & previously given#",
+                              Id, E);
+                        end if;
 
-                  --  Case of Pre and Pre'Class both specified
+                        --  Case of Pre and Pre'Class both specified
 
-                  elsif Nam = Name_Pre then
-                     if Class_Present (Aspect) then
-                        Error_Msg_NE
-                          ("aspect `Pre''Class` for & is not allowed here",
-                           Id, E);
-                        Error_Msg_NE
-                          ("\since aspect `Pre` previously given#",
-                           Id, E);
+                     elsif Nam = Name_Pre then
+                        if Class_Present (Aspect) then
+                           Error_Msg_NE
+                             ("aspect `Pre''Class` for & is not allowed here",
+                              Id, E);
+                           Error_Msg_NE
+                             ("\since aspect `Pre` previously given#",
+                              Id, E);
 
-                     else
-                        Error_Msg_NE
-                          ("aspect `Pre` for & is not allowed here",
-                           Id, E);
-                        Error_Msg_NE
-                          ("\since aspect `Pre''Class` previously given#",
-                           Id, E);
+                        else
+                           Error_Msg_NE
+                             ("aspect `Pre` for & is not allowed here",
+                              Id, E);
+                           Error_Msg_NE
+                             ("\since aspect `Pre''Class` previously given#",
+                              Id, E);
+                        end if;
                      end if;
+
+                     --  Allowed case of X and X'Class both specified
                   end if;
 
-                  --  Allowed case of X and X'Class both specified
-               end if;
+                  Next (Anod);
+               end loop;
+            end if;
 
-               Next (Anod);
-            end loop;
-
             --  Copy expression for later processing by the procedures
             --  Check_Aspect_At_[Freeze_Point | End_Of_Declarations]
 
@@ -1219,7 +1222,7 @@ 
                     Aspect_Static_Predicate  =>
 
                   --  Construct the pragma (always a pragma Predicate, with
-                  --  flags recording whether
+                  --  flags recording whether it is static/dynamic).
 
                   Aitem :=
                     Make_Pragma (Loc,
@@ -1255,6 +1258,64 @@ 
                   Ensure_Freeze_Node (E);
                   Set_Is_Delayed_Aspect (Aspect);
                   Delay_Required := True;
+
+               when Aspect_Test_Case => declare
+                  Args      : List_Id;
+                  Comp_Expr : Node_Id;
+                  Comp_Assn : Node_Id;
+
+               begin
+                  Args := New_List;
+
+                  if Nkind (Expr) /= N_Aggregate then
+                     Error_Msg_NE
+                       ("wrong syntax for aspect `Test_Case` for &", Id, E);
+                     goto Continue;
+                  end if;
+
+                  Comp_Expr := First (Expressions (Expr));
+                  while Present (Comp_Expr) loop
+                     Append (Relocate_Node (Comp_Expr), Args);
+                     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_NE
+                          ("wrong syntax for aspect `Test_Case` for &", Id, E);
+                        goto Continue;
+                     end if;
+
+                     Append (Make_Pragma_Argument_Association (
+                       Sloc       => Sloc (Comp_Assn),
+                       Chars      => Chars (First (Choices (Comp_Assn))),
+                       Expression => Relocate_Node (Expression (Comp_Assn))),
+                       Args);
+                     Next (Comp_Assn);
+                  end loop;
+
+                  --  Build the test-case pragma
+
+                  Aitem :=
+                    Make_Pragma (Loc,
+                      Pragma_Identifier            =>
+                        Make_Identifier (Sloc (Id), Name_Test_Case),
+                      Pragma_Argument_Associations =>
+                        Args);
+
+                  Set_From_Aspect_Specification (Aitem, True);
+                  Set_Is_Delayed_Aspect (Aspect);
+
+                  --  Insert immediately after the entity declaration
+
+                  Insert_After (N, Aitem);
+
+                  goto Continue;
+               end;
             end case;
 
             --  If a delay is required, we delay the freeze (not much point in
@@ -5330,6 +5391,12 @@ 
          when Boolean_Aspects =>
             raise Program_Error;
 
+         --  Test_Case aspect applies to entries and subprograms, hence should
+         --  never be delayed.
+
+         when Aspect_Test_Case =>
+            raise Program_Error;
+
          --  Default_Value is resolved with the type entity in question
 
          when Aspect_Default_Value =>
@@ -5354,8 +5421,7 @@ 
          when Aspect_Storage_Pool =>
             T := Class_Wide_Type (RTE (RE_Root_Storage_Pool));
 
-         when
-              Aspect_Alignment      |
+         when Aspect_Alignment      |
               Aspect_Component_Size |
               Aspect_Machine_Radix  |
               Aspect_Object_Size    |
@@ -5375,7 +5441,7 @@ 
             Analyze (Expression (ASN));
             return;
 
-         --  Suppress/Unsupress/Warnings should never be delayed
+         --  Suppress/Unsuppress/Warnings should never be delayed
 
          when Aspect_Suppress   |
               Aspect_Unsuppress |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 177328)
+++ snames.ads-tmpl	(working copy)
@@ -544,6 +544,7 @@ 
    Name_Suppress_Debug_Info            : constant Name_Id := N + $; -- GNAT
    Name_Suppress_Initialization        : constant Name_Id := N + $; -- GNAT
    Name_System_Name                    : constant Name_Id := N + $; -- Ada 83
+   Name_Test_Case                      : constant Name_Id := N + $; -- GNAT
    Name_Task_Info                      : constant Name_Id := N + $; -- GNAT
    Name_Task_Name                      : constant Name_Id := N + $; -- GNAT
    Name_Task_Storage                   : constant Name_Id := N + $; -- VMS
@@ -624,6 +625,7 @@ 
    Name_Descriptor                     : constant Name_Id := N + $;
    Name_Dot_Replacement                : constant Name_Id := N + $;
    Name_Dynamic                        : constant Name_Id := N + $;
+   Name_Ensures                        : constant Name_Id := N + $;
    Name_Entity                         : constant Name_Id := N + $;
    Name_Entry_Count                    : constant Name_Id := N + $;
    Name_External_Name                  : constant Name_Id := N + $;
@@ -646,6 +648,7 @@ 
    Name_Mechanism                      : constant Name_Id := N + $;
    Name_Message                        : constant Name_Id := N + $;
    Name_Mixedcase                      : constant Name_Id := N + $;
+   Name_Mode                           : constant Name_Id := N + $;
    Name_Modified_GPL                   : constant Name_Id := N + $;
    Name_Name                           : constant Name_Id := N + $;
    Name_NCA                            : constant Name_Id := N + $;
@@ -657,13 +660,16 @@ 
    Name_No_Requeue_Statements          : constant Name_Id := N + $;
    Name_No_Task_Attributes             : constant Name_Id := N + $;
    Name_No_Task_Attributes_Package     : constant Name_Id := N + $;
+   Name_Normal                         : constant Name_Id := N + $;
    Name_On                             : constant Name_Id := N + $;
    Name_Policy                         : constant Name_Id := N + $;
    Name_Parameter_Types                : constant Name_Id := N + $;
    Name_Reference                      : constant Name_Id := N + $;
+   Name_Requires                       : constant Name_Id := N + $;
    Name_Restricted                     : constant Name_Id := N + $;
    Name_Result_Mechanism               : constant Name_Id := N + $;
    Name_Result_Type                    : constant Name_Id := N + $;
+   Name_Robustness                     : constant Name_Id := N + $;
    Name_Runtime                        : constant Name_Id := N + $;
    Name_SB                             : constant Name_Id := N + $;
    Name_Secondary_Stack_Size           : constant Name_Id := N + $;
@@ -1634,6 +1640,7 @@ 
       Pragma_Suppress_Debug_Info,
       Pragma_Suppress_Initialization,
       Pragma_System_Name,
+      Pragma_Test_Case,
       Pragma_Task_Info,
       Pragma_Task_Name,
       Pragma_Task_Storage,