[multiple changes]

2011-09-02  Robert Dewar  <dewar@adacore.com>

	* prj-dect.adb, prj-env.adb, prj-nmsc.adb, prj-proc.adb, prj-tree.adb,
	prj.adb, prj.ads, sem_ch5.adb: Minor reformatting.

2011-09-02  Thomas Quinot  <quinot@adacore.com>

	* sem_attr.adb (Analyze_Attribute, case Unrestriced_Access):
	Guard against a prefix that is an N_Has_Entity but has no
	associated entity.

2011-09-02  Yannick Moy  <moy@adacore.com>

	* lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa
	references.

2011-09-02  Yannick Moy  <moy@adacore.com>

	* opt.ads (Warn_On_Suspicious_Contract): New warning flag.
	* sem_ch3.adb (Analyze_Declarations): Call checker for suspicious
	contracts.
	* sem_ch6.adb, sem_ch6.ads (Check_Subprogram_Contract): New
	procedure looking for suspicious postconditions.
	* usage.adb (Usage): New options -gnatw.t and -gnatw.T.
	* warnsw.adb (Set_Dot_Warning_Switch): Take into account new
	options -gnatw.t and -gnatw.T.

From-SVN: r178448

17 files changed, 318 insertions, 54 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9a5fdea..6abbf34 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,30 @@
+2011-09-02  Robert Dewar  <dewar@adacore.com>
+
+	* prj-dect.adb, prj-env.adb, prj-nmsc.adb, prj-proc.adb, prj-tree.adb,
+	prj.adb, prj.ads, sem_ch5.adb: Minor reformatting.
+
+2011-09-02  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_attr.adb (Analyze_Attribute, case Unrestriced_Access):
+	Guard against a prefix that is an N_Has_Entity but has no
+	associated entity.
+
+2011-09-02  Yannick Moy  <moy@adacore.com>
+
+	* lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa
+	references.
+
+2011-09-02  Yannick Moy  <moy@adacore.com>
+
+	* opt.ads (Warn_On_Suspicious_Contract): New warning flag.
+	* sem_ch3.adb (Analyze_Declarations): Call checker for suspicious
+	contracts.
+	* sem_ch6.adb, sem_ch6.ads (Check_Subprogram_Contract): New
+	procedure looking for suspicious postconditions.
+	* usage.adb (Usage): New options -gnatw.t and -gnatw.T.
+	* warnsw.adb (Set_Dot_Warning_Switch): Take into account new
+	options -gnatw.t and -gnatw.T.
+
 2011-09-02  Pascal Obry  <obry@adacore.com>
 
 	* prj.adb: Minor code refactoring. Move check for null project in
diff --git a/gcc/ada/lib-xref-alfa.adb b/gcc/ada/lib-xref-alfa.adb
index 74d1421..ce95463 100644
--- a/gcc/ada/lib-xref-alfa.adb
+++ b/gcc/ada/lib-xref-alfa.adb
@@ -608,11 +608,20 @@ package body Alfa is
             --  On non-callable entities, the only references of interest are
             --  reads and writes.
 
-            if Ekind (E) in Overloadable_Kind then
-               return Typ = 's';
-            else
-               return Typ = 'r' or else Typ = 'm';
-            end if;
+            case Ekind (E) is
+               when Overloadable_Kind =>
+                  return Typ = 's';
+
+               --  References to IN parameters are not considered in Alfa
+               --  section, as these will be translated as constants in the
+               --  intermediate language for formal verification.
+
+               when E_In_Parameter =>
+                  return False;
+
+               when others =>
+                  return Typ = 'r' or else Typ = 'm';
+            end case;
          end Is_Alfa_Reference;
 
          -------------------
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index d2874d4..9e4ee4a 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1550,6 +1550,12 @@ package Opt is
    --  clauses that are affected by non-standard bit-order. The default is
    --  that this warning is enabled.
 
+   Warn_On_Suspicious_Contract : Boolean := True;
+   --  GNAT
+   --  Set to True to generate warnings for suspicious contracts expressed as
+   --  pragmas or aspects precondition and postcondition. The default is that
+   --  this warning is enabled.
+
    Warn_On_Suspicious_Modulus_Value : Boolean := True;
    --  GNAT
    --  Set to True to generate warnings for suspicious modulus values. The
diff --git a/gcc/ada/prj-dect.adb b/gcc/ada/prj-dect.adb
index dae5480..b1a1738 100644
--- a/gcc/ada/prj-dect.adb
+++ b/gcc/ada/prj-dect.adb
@@ -23,10 +23,6 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with GNAT.Case_Util;        use GNAT.Case_Util;
-with GNAT.Spelling_Checker; use GNAT.Spelling_Checker;
-with GNAT.Strings;
-
 with Err_Vars;    use Err_Vars;
 with Opt;         use Opt;
 with Prj.Attr;    use Prj.Attr;
@@ -37,32 +33,34 @@ with Prj.Tree;    use Prj.Tree;
 with Snames;
 with Uintp;       use Uintp;
 
-package body Prj.Dect is
+with GNAT;                  use GNAT;
+with GNAT.Case_Util;        use GNAT.Case_Util;
+with GNAT.Spelling_Checker; use GNAT.Spelling_Checker;
+with GNAT.Strings;
 
-   use GNAT;
+package body Prj.Dect is
 
    type Zone is (In_Project, In_Package, In_Case_Construction);
-   --  Used to indicate if we are parsing a package (In_Package),
-   --  a case construction (In_Case_Construction) or none of those two
-   --  (In_Project).
+   --  Used to indicate if we are parsing a package (In_Package), a case
+   --  construction (In_Case_Construction) or none of those two (In_Project).
 
    procedure Rename_Obsolescent_Attributes
      (In_Tree         : Project_Node_Tree_Ref;
       Attribute       : Project_Node_Id;
       Current_Package : Project_Node_Id);
-   --  Rename obsolescent attributes in the tree.
-   --  When the attribute has been renamed since its initial introduction in
-   --  the design of projects, we replace the old name in the tree with the
-   --  new name, so that the code does not have to check both names forever.
+   --  Rename obsolescent attributes in the tree. When the attribute has been
+   --  renamed since its initial introduction in the design of projects, we
+   --  replace the old name in the tree with the new name, so that the code
+   --  does not have to check both names forever.
 
    procedure Check_Attribute_Allowed
      (In_Tree   : Project_Node_Tree_Ref;
       Project   : Project_Node_Id;
       Attribute : Project_Node_Id;
       Flags     : Processing_Flags);
-   --  Check whether the attribute is valid in this project.
-   --  In particular, depending on the type of project (qualifier), some
-   --  attributes might be disabled.
+   --  Check whether the attribute is valid in this project. In particular,
+   --  depending on the type of project (qualifier), some attributes might
+   --  be disabled.
 
    procedure Check_Package_Allowed
      (In_Tree         : Project_Node_Tree_Ref;
@@ -244,7 +242,7 @@ package body Prj.Dect is
    begin
       case Qualif is
          when Aggregate | Aggregate_Library =>
-            if Name = Snames.Name_Languages
+            if        Name = Snames.Name_Languages
               or else Name = Snames.Name_Source_Files
               or else Name = Snames.Name_Source_List_File
               or else Name = Snames.Name_Locally_Removed_Files
diff --git a/gcc/ada/prj-env.adb b/gcc/ada/prj-env.adb
index 734ef49..9f29313 100644
--- a/gcc/ada/prj-env.adb
+++ b/gcc/ada/prj-env.adb
@@ -778,10 +778,9 @@ package body Prj.Env is
       In_Tree  : Project_Tree_Ref;
       Name     : out Path_Name_Type)
    is
-      File   : File_Descriptor := Invalid_FD;
-
-      Buffer      : String_Access := new String (1 .. Buffer_Initial);
-      Buffer_Last : Natural := 0;
+      File        : File_Descriptor := Invalid_FD;
+      Buffer      : String_Access   := new String (1 .. Buffer_Initial);
+      Buffer_Last : Natural         := 0;
 
       procedure Put_Name_Buffer;
       --  Put the line contained in the Name_Buffer in the global buffer
@@ -833,7 +832,7 @@ package body Prj.Env is
             if Source.Replaced_By = No_Source
               and then Source.Path.Name /= No_Path
               and then (Source.Language.Config.Kind = File_Based
-                        or else Source.Unit /= No_Unit_Index)
+                         or else Source.Unit /= No_Unit_Index)
             then
                if Source.Unit /= No_Unit_Index then
 
@@ -1141,7 +1140,7 @@ package body Prj.Env is
 
             if not Main_Project_Only
               or else (Unit.File_Names (Spec) /= null
-                       and then Unit.File_Names (Spec).Project = The_Project)
+                        and then Unit.File_Names (Spec).Project = The_Project)
             then
                declare
                   Current_Name : File_Name_Type;
@@ -1668,7 +1667,7 @@ package body Prj.Env is
       --  For the object path, we make a distinction depending on
       --  Including_Libraries.
 
-      if Objects_Path and then Including_Libraries then
+      if Objects_Path and Including_Libraries then
          if Project.Objects_Path_File_With_Libs = No_Path then
             Object_Path_Table.Init (Object_Paths);
             Process_Object_Dirs := True;
@@ -1688,7 +1687,7 @@ package body Prj.Env is
       --  If there is something to do, set Seen to False for all projects,
       --  then call the recursive procedure Add for Project.
 
-      if Process_Source_Dirs or else Process_Object_Dirs then
+      if Process_Source_Dirs or Process_Object_Dirs then
          For_All_Projects (Project, In_Tree, Dummy);
       end if;
 
diff --git a/gcc/ada/prj-nmsc.adb b/gcc/ada/prj-nmsc.adb
index 63b434f..2c8d96a 100644
--- a/gcc/ada/prj-nmsc.adb
+++ b/gcc/ada/prj-nmsc.adb
@@ -36,8 +36,9 @@ with Sinput.P;
 with Snames;   use Snames;
 with Targparm; use Targparm;
 
+with Ada;                        use Ada;
 with Ada.Characters.Handling;    use Ada.Characters.Handling;
-with Ada.Directories;            use Ada, Ada.Directories;
+with Ada.Directories;            use Ada.Directories;
 with Ada.Strings;                use Ada.Strings;
 with Ada.Strings.Fixed;          use Ada.Strings.Fixed;
 with Ada.Strings.Maps.Constants; use Ada.Strings.Maps.Constants;
@@ -5194,13 +5195,13 @@ package body Prj.Nmsc is
 
       No_Sources : constant Boolean :=
                      ((not Source_Files.Default
-                       and then Source_Files.Values = Nil_String)
+                        and then Source_Files.Values = Nil_String)
                       or else
                         (not Source_Dirs.Default
-                         and then Source_Dirs.Values = Nil_String)
+                          and then Source_Dirs.Values = Nil_String)
                       or else
                         (not Languages.Default
-                         and then Languages.Values = Nil_String))
+                          and then Languages.Values = Nil_String))
                      and then Project.Extends = No_Project;
 
    --  Start of processing for Get_Directories
@@ -5248,6 +5249,7 @@ package body Prj.Nmsc is
                Externally_Built => Project.Externally_Built);
 
             if not Dir_Exists and then not Project.Externally_Built then
+
                --  The object directory does not exist, report an error if the
                --  project is not externally built.
 
@@ -7270,9 +7272,9 @@ package body Prj.Nmsc is
 
       --  Loop through subdirectories
 
-      Source_Dir := Project.Project.Source_Dirs;
       Src_Dir_Rank := Project.Project.Source_Dir_Ranks;
 
+      Source_Dir := Project.Project.Source_Dirs;
       while Source_Dir /= Nil_String loop
          begin
             Num_Nod := Shared.Number_Lists.Table (Src_Dir_Rank);
@@ -7322,7 +7324,7 @@ package body Prj.Nmsc is
 
                      if not Opt.Follow_Links_For_Files
                        or else Is_Regular_File
-                         (Display_Source_Directory & Name (1 .. Last))
+                                 (Display_Source_Directory & Name (1 .. Last))
                      then
                         Name_Len := Last;
                         Name_Buffer (1 .. Name_Len) := Name (1 .. Last);
diff --git a/gcc/ada/prj-proc.adb b/gcc/ada/prj-proc.adb
index e8ba991..269bc45 100644
--- a/gcc/ada/prj-proc.adb
+++ b/gcc/ada/prj-proc.adb
@@ -1364,7 +1364,7 @@ package body Prj.Proc is
          Reset_Tree             => Reset_Tree);
 
       if Project_Qualifier_Of
-        (From_Project_Node, From_Project_Node_Tree) /= Configuration
+           (From_Project_Node, From_Project_Node_Tree) /= Configuration
       then
          Process_Project_Tree_Phase_2
            (In_Tree                => In_Tree,
@@ -1566,8 +1566,8 @@ package body Prj.Proc is
                      --  declaration.
 
                      Copy_Package_Declarations
-                       (From       =>
-                          Shared.Packages.Table (Renamed_Package).Decl,
+                       (From       => Shared.Packages.Table
+                                        (Renamed_Package).Decl,
                         To         => Shared.Packages.Table (New_Pkg).Decl,
                         New_Loc    => Location_Of (Current_Item, Node_Tree),
                         Restricted => False,
@@ -2577,6 +2577,7 @@ package body Prj.Proc is
          Loaded_Project : Prj.Tree.Project_Node_Id;
          Success        : Boolean := True;
          Tree           : Project_Tree_Ref;
+
       begin
          if Project.Qualifier not in Aggregate_Project then
             return;
@@ -2711,6 +2712,7 @@ package body Prj.Proc is
          end loop;
 
          if Attribute1 = No_Variable or else Attr_Value1.Value.Default then
+
             --  Attribute Languages is not declared in the extending project.
             --  Check if it is declared in the project being extended.
 
@@ -2754,8 +2756,8 @@ package body Prj.Proc is
             Imported         : Project_List;
             Declaration_Node : Project_Node_Id  := Empty_Node;
 
-            Name      : constant Name_Id :=
-                          Name_Of (From_Project_Node, From_Project_Node_Tree);
+            Name : constant Name_Id :=
+                     Name_Of (From_Project_Node, From_Project_Node_Tree);
 
             Name_Node : constant Tree_Private_Part.Project_Name_And_Node :=
                           Tree_Private_Part.Projects_Htable.Get
@@ -2837,7 +2839,9 @@ package body Prj.Proc is
                Initialize_And_Copy (Child_Env, Copy_From => Env);
 
             elsif Project.Qualifier = Aggregate_Library then
+
                --  The child environment is the same as the current one
+
                Child_Env := Env;
 
             else
@@ -2888,9 +2892,9 @@ package body Prj.Proc is
 
                if Project.Qualifier = Aggregate_Library then
                   declare
-                     L : Aggregated_Project_List :=
-                           Project.Aggregated_Projects;
+                     L : Aggregated_Project_List;
                   begin
+                     L := Project.Aggregated_Projects;
                      while L /= null loop
                         Project.Imported_Projects :=
                           new Project_List_Element'
diff --git a/gcc/ada/prj-tree.adb b/gcc/ada/prj-tree.adb
index 2b420e1..8072c9d 100644
--- a/gcc/ada/prj-tree.adb
+++ b/gcc/ada/prj-tree.adb
@@ -104,6 +104,7 @@ package body Prj.Tree is
       Zone := In_Tree.Project_Nodes.Table (To).Comments;
 
       if No (Zone) then
+
          --  Create new N_Comment_Zones node
 
          Project_Node_Table.Increment_Last (In_Tree.Project_Nodes);
diff --git a/gcc/ada/prj.adb b/gcc/ada/prj.adb
index 3a2ef4e..7795cc9 100644
--- a/gcc/ada/prj.adb
+++ b/gcc/ada/prj.adb
@@ -393,9 +393,7 @@ package body Prj is
       if Iter.Language = No_Language_Index then
          if Iter.All_Projects then
             Iter.Project := Iter.Project.Next;
-
             Project_Changed (Iter);
-
          else
             Iter.Project := null;
          end if;
@@ -582,7 +580,6 @@ package body Prj is
 
       begin
          Iterator := For_Each_Source (In_Tree => Tree, Project => Proj);
-
          while Element (Iterator) /= No_Source loop
             if Element (Iterator).File = Base_Name
               and then (Index = 0 or else Element (Iterator).Index = Index)
@@ -1662,6 +1659,7 @@ package body Prj is
       Root_Tree    : Project_Tree_Ref)
    is
       Agg : Aggregated_Project_List;
+
    begin
       Action (Root_Project, Root_Tree);
 
@@ -1674,6 +1672,8 @@ package body Prj is
       end if;
    end For_Project_And_Aggregated;
 
+--  Package initialization for Prj
+
 begin
    --  Make sure that the standard config and user project file extensions are
    --  compatible with canonical case file naming.
diff --git a/gcc/ada/prj.ads b/gcc/ada/prj.ads
index 0b0dee6..e88455d 100644
--- a/gcc/ada/prj.ads
+++ b/gcc/ada/prj.ads
@@ -77,8 +77,8 @@ package Prj is
    --    Aggregate_Library:    aggregate library project is ...
    --    Configuration:        configuration project is ...
 
-   subtype Aggregate_Project
-     is Project_Qualifier range Aggregate .. Aggregate_Library;
+   subtype Aggregate_Project is
+     Project_Qualifier range Aggregate .. Aggregate_Library;
 
    All_Packages : constant String_List_Access;
    --  Default value of parameter Packages of procedures Parse, in Prj.Pars and
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index d09e3b5..480e9a6 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -4942,7 +4942,10 @@ package body Sem_Attr is
          if Comes_From_Source (N) then
             Check_Restriction (No_Unchecked_Access, N);
 
-            if Nkind (P) in N_Has_Entity and then Is_Object (Entity (P)) then
+            if Nkind (P) in N_Has_Entity
+                 and then Present (Entity (P))
+                 and then Is_Object (Entity (P))
+            then
                Check_Restriction (No_Implicit_Aliasing, N);
             end if;
          end if;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 6a55aa9..4102bea 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2192,6 +2192,8 @@ package body Sem_Ch3 is
                   Prag := Next_Pragma (Prag);
                end loop;
 
+               Check_Subprogram_Contract (Sent);
+
                Prag := Spec_TC_List (Contract (Sent));
                while Present (Prag) loop
                   Analyze_TC_In_Decl_Part (Prag, Sent);
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index b5584e6..5a2d2b3 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2261,9 +2261,9 @@ package body Sem_Ch5 is
          Analyze (Subt);
       end if;
 
-      --  If domain of iteration is an expression, create a declaration for it,
-      --  so that finalization actions are introduced outside of the loop.
-      --  The declaration must be a renaming because the  body of the loop may
+      --  If domain of iteration is an expression, create a declaration for
+      --  it, so that finalization actions are introduced outside of the loop.
+      --  The declaration must be a renaming because the body of the loop may
       --  assign to elements.
 
       if not Is_Entity_Name (Iter_Name) then
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 7b4bf91..648cdcb 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -5454,6 +5454,207 @@ package body Sem_Ch6 is
       end if;
    end Check_Returns;
 
+   -------------------------------
+   -- Check_Subprogram_Contract --
+   -------------------------------
+
+   procedure Check_Subprogram_Contract (Spec_Id : Entity_Id) is
+
+--        Inherited : constant Subprogram_List :=
+--                      Inherited_Subprograms (Spec_Id);
+      --  List of subprograms inherited by this subprogram
+
+      Last_Postcondition         : Node_Id := Empty;
+      --  Last postcondition on the subprogram, or else Empty if either no
+      --  postcondition or only inherited postconditions.
+
+      Attribute_Result_Mentioned : Boolean := False;
+      --  Whether attribute 'Result is mentioned in a postcondition
+
+      Post_State_Mentioned       : Boolean := False;
+      --  Whether some expression mentioned in a postcondition can have a
+      --  different value in the post-state than in the pre-state.
+
+      function Check_Attr_Result (N : Node_Id) return Traverse_Result;
+      --  Check whether N is a reference to the attribute 'Result, and if so
+      --  set Attribute_Result_Mentioned and return Abandon. Otherwise return
+      --  OK.
+
+      function Check_Post_State (N : Node_Id) return Traverse_Result;
+      --  Check whether the value of evaluating N can be different in the
+      --  post-state, compared to the same evaluation in the pre-state, and
+      --  if so set Post_State_Mentioned and return Abandon. Return Skip on
+      --  reference to attribute 'Old, in order to ignore its prefix, which
+      --  is precisely evaluated in the pre-state. Otherwise return OK.
+
+      procedure Process_Post_Conditions
+        (Spec  : Node_Id;
+         Class : Boolean);
+      --  This processes the Spec_PPC_List from Spec, processing any
+      --  postconditions from the list. If Class is True, then only
+      --  postconditions marked with Class_Present are considered. The
+      --  caller has checked that Spec_PPC_List is non-Empty.
+
+      function Find_Attribute_Result is new Traverse_Func (Check_Attr_Result);
+
+      function Find_Post_State is new Traverse_Func (Check_Post_State);
+
+      -----------------------
+      -- Check_Attr_Result --
+      -----------------------
+
+      function Check_Attr_Result (N : Node_Id) return Traverse_Result is
+      begin
+         if Nkind (N) = N_Attribute_Reference
+           and then
+             Get_Attribute_Id (Attribute_Name (N)) = Attribute_Result
+         then
+            Attribute_Result_Mentioned := True;
+            return Abandon;
+         else
+            return OK;
+         end if;
+      end Check_Attr_Result;
+
+      ----------------------
+      -- Check_Post_State --
+      ----------------------
+
+      function Check_Post_State (N : Node_Id) return Traverse_Result is
+         Found : Boolean := False;
+
+      begin
+         case Nkind (N) is
+            when N_Function_Call        |
+                 N_Explicit_Dereference =>
+               Found := True;
+
+            when N_Identifier    |
+                 N_Expanded_Name =>
+               declare
+                  E : constant Entity_Id := Entity (N);
+               begin
+                  if Is_Entity_Name (N)
+                    and then Present (E)
+                    and then Ekind (E) in Assignable_Kind
+                  then
+                     Found := True;
+                  end if;
+               end;
+
+            when N_Attribute_Reference =>
+               case Get_Attribute_Id (Attribute_Name (N)) is
+                  when Attribute_Old =>
+                     return Skip;
+                  when Attribute_Result =>
+                     Found := True;
+                  when others =>
+                     null;
+               end case;
+
+            when others =>
+               null;
+         end case;
+
+         if Found then
+            Post_State_Mentioned := True;
+            return Abandon;
+         else
+            return OK;
+         end if;
+      end Check_Post_State;
+
+      -----------------------------
+      -- Process_Post_Conditions --
+      -----------------------------
+
+      procedure Process_Post_Conditions
+        (Spec  : Node_Id;
+         Class : Boolean)
+      is
+         Prag    : Node_Id;
+         Arg     : Node_Id;
+         Ignored : Traverse_Final_Result;
+         pragma Unreferenced (Ignored);
+
+      begin
+         Prag := Spec_PPC_List (Contract (Spec));
+
+         loop
+            Arg := First (Pragma_Argument_Associations (Prag));
+
+            --  Since pre- and postconditions are listed in reverse order, the
+            --  first postcondition in the list is the last in the source.
+
+            if Pragma_Name (Prag) = Name_Postcondition
+              and then not Class
+              and then No (Last_Postcondition)
+            then
+               Last_Postcondition := Prag;
+            end if;
+
+            --  For functions, look for presence of 'Result in postcondition
+
+            if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+               Ignored := Find_Attribute_Result (Arg);
+            end if;
+
+            --  For each individual non-inherited postcondition, look for
+            --  presence of an expression that could be evaluated differently
+            --  in post-state.
+
+            if Pragma_Name (Prag) = Name_Postcondition
+              and then not Class
+            then
+               Post_State_Mentioned := False;
+               Ignored              := Find_Post_State (Arg);
+
+               if not Post_State_Mentioned then
+                  Error_Msg_N ("?postcondition only refers to pre-state",
+                               Prag);
+               end if;
+            end if;
+
+            Prag := Next_Pragma (Prag);
+            exit when No (Prag);
+         end loop;
+      end Process_Post_Conditions;
+
+   --  Start of processing for Check_Subprogram_Contract
+
+   begin
+      if not Warn_On_Suspicious_Contract then
+         return;
+      end if;
+
+      if Present (Spec_PPC_List (Contract (Spec_Id))) then
+         Process_Post_Conditions (Spec_Id, Class => False);
+      end if;
+
+      --  Process inherited postconditions
+
+      --  Code is currently commented out as, in some cases, it causes crashes
+      --  because Direct_Primitive_Operations is not available for a private
+      --  type. This may cause more warnings to be issued than necessary.
+
+--        for J in Inherited'Range loop
+--           if Present (Spec_PPC_List (Contract (Inherited (J)))) then
+--              Process_Post_Conditions (Inherited (J), Class => True);
+--           end if;
+--        end loop;
+
+      --  Issue warning for functions whose postcondition does not mention
+      --  'Result after all postconditions have been processed.
+
+      if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+        and then Present (Last_Postcondition)
+        and then not Attribute_Result_Mentioned
+      then
+         Error_Msg_N ("?function postcondition does not mention result",
+                      Last_Postcondition);
+      end if;
+   end Check_Subprogram_Contract;
+
    ----------------------------
    -- Check_Subprogram_Order --
    ----------------------------
diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads
index 96d967b..1ca6f3b 100644
--- a/gcc/ada/sem_ch6.ads
+++ b/gcc/ada/sem_ch6.ads
@@ -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- --
@@ -113,6 +113,10 @@ package Sem_Ch6 is
    --  type-conformant subprogram that becomes hidden by the new subprogram.
    --  Is_Primitive indicates whether the subprogram is primitive.
 
+   procedure Check_Subprogram_Contract (Spec_Id : Entity_Id);
+   --  Spec_Id is the spec entity for a subprogram. This routine issues
+   --  warnings on suspicious contracts if Warn_On_Suspicious_Contract is set.
+
    procedure Check_Subtype_Conformant
      (New_Id                   : Entity_Id;
       Old_Id                   : Entity_Id;
diff --git a/gcc/ada/usage.adb b/gcc/ada/usage.adb
index a4f09483..1d79f66 100644
--- a/gcc/ada/usage.adb
+++ b/gcc/ada/usage.adb
@@ -484,6 +484,8 @@ begin
    Write_Line ("        .S*  turn off warnings for overridden size clause");
    Write_Line ("        t    turn on warnings for tracking deleted code");
    Write_Line ("        T*   turn off warnings for tracking deleted code");
+   Write_Line ("        .t*  turn on warnings for suspicious contract");
+   Write_Line ("        .T   turn off warnings for suspicious contract");
    Write_Line ("        u+   turn on warnings for unused entity");
    Write_Line ("        U*   turn off warnings for unused entity");
    Write_Line ("        .u   turn on warnings for unordered enumeration");
diff --git a/gcc/ada/warnsw.adb b/gcc/ada/warnsw.adb
index c226f3b..96a8e8f 100644
--- a/gcc/ada/warnsw.adb
+++ b/gcc/ada/warnsw.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1999-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1999-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- --
@@ -143,6 +143,12 @@ package body Warnsw is
          when 'S' =>
             Warn_On_Overridden_Size             := False;
 
+         when 't' =>
+            Warn_On_Suspicious_Contract         := True;
+
+         when 'T' =>
+            Warn_On_Suspicious_Contract         := False;
+
          when 'u' =>
             Warn_On_Unordered_Enumeration_Type  := True;