[multiple changes]

2012-03-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_util.adb (Initialized_By_Ctrl_Function): Do not loop over
	selector names as the function call always appears at the top selected
	component.

2012-03-15  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch12.adb (Validate_Access_Subprogram_Instance): keep
	Mode_Conformance check for older versions of the language.

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

	* gnat_ugn.texi Document the extension of option -gnatw.t.
	* sem_ch3.adb (Analyze_Declaration): Check for suspicious
	contracts only after contract cases have been semantically
	analyzed.
	* sem_ch6.adb (Check_Subprogram_Contract): Consider also Ensures
	components of contract cases for detecting suspicious contracts.

From-SVN: r185417

6 files changed, 165 insertions, 48 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f5b141e..e8d4a5b 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,23 @@
+2012-03-15  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_util.adb (Initialized_By_Ctrl_Function): Do not loop over
+	selector names as the function call always appears at the top selected
+	component.
+
+2012-03-15  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch12.adb (Validate_Access_Subprogram_Instance): keep
+	Mode_Conformance check for older versions of the language.
+
+2012-03-15  Yannick Moy  <moy@adacore.com>
+
+	* gnat_ugn.texi Document the extension of option -gnatw.t.
+	* sem_ch3.adb (Analyze_Declaration): Check for suspicious
+	contracts only after contract cases have been semantically
+	analyzed.
+	* sem_ch6.adb (Check_Subprogram_Contract): Consider also Ensures
+	components of contract cases for detecting suspicious contracts.
+
 2012-03-15  Yannick Moy  <moy@adacore.com>
 
 	* aspects.adb, aspects.ads (Aspect_Id): New GNAT aspect
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 8ccf216..ae7f2b9 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -3967,16 +3967,11 @@ package body Exp_Util is
             Expr := Name (Expr);
          end if;
 
-         --  The function call may appear in object.operation format. Strip
-         --  all prefixes and retrieve the function name.
+         --  The function call may appear in object.operation format
 
-         loop
-            if Nkind (Expr) = N_Selected_Component then
-               Expr := Selector_Name (Expr);
-            else
-               exit;
-            end if;
-         end loop;
+         if Nkind (Expr) = N_Selected_Component then
+            Expr := Selector_Name (Expr);
+         end if;
 
          return
            Nkind_In (Expr, N_Expanded_Name, N_Identifier)
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index 08e0649..365a447 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -5696,9 +5696,11 @@ This switch suppresses warnings for tracking of deleted conditional code.
 @emph{Activate warnings on suspicious contracts.}
 @cindex @option{-gnatw.t} (@command{gcc})
 This switch activates warnings on suspicious postconditions (whether a
-pragma @code{Postcondition} or a @code{Post} aspect in Ada 2012). A
-function postcondition is suspicious when it does not mention the result
-of the function. A procedure postcondition is suspicious when it only
+pragma @code{Postcondition} or a @code{Post} aspect in Ada 2012)
+and suspicious contract cases (pragma @code{Contract_Case}). A
+function postcondition or contract case is suspicious when no postcondition
+or contract case for this function mentions the result of the function.
+A procedure postcondition or contract case is suspicious when it only
 refers to the pre-state of the procedure, because in that case it should
 rather be expressed as a precondition. The default is that such warnings
 are not generated. This warning can also be turned on using @option{-gnatwa}.
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index b411b3b..5ab842d 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -10433,17 +10433,29 @@ package body Sem_Ch12 is
             Abandon_Instantiation (Actual);
          end if;
 
-         --  In accordance with AI05-288 (which is an Ada 2012 AI that is a
-         --  binding intepretation to be applied to previous versions of Ada
-         --  as well as Ada 2012), actuals for access_to_subprograms must be
+         --  According to AI05-288, actuals for access_to_subprograms must be
          --  subtype conformant with the generic formal. Previous to AI05-288
          --  only mode conformance was required.
 
-         Check_Subtype_Conformant
-           (Designated_Type (Act_T),
-            Designated_Type (A_Gen_T),
-            Actual,
-            Get_Inst => True);
+         --  This is a binding interpretation that applies to previous versions
+         --  of the language, but for now we retain the milder check in order
+         --  to preserve ACATS tests.
+         --  These will be protested eventually ???
+
+         if Ada_Version < Ada_2012 then
+            Check_Mode_Conformant
+              (Designated_Type (Act_T),
+               Designated_Type (A_Gen_T),
+               Actual,
+               Get_Inst => True);
+
+         else
+            Check_Subtype_Conformant
+              (Designated_Type (Act_T),
+               Designated_Type (A_Gen_T),
+               Actual,
+               Get_Inst => True);
+         end if;
 
          if Ekind (Base_Type (Act_T)) = E_Access_Protected_Subprogram_Type then
             if Ekind (A_Gen_T) = E_Access_Subprogram_Type then
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 9d66884..71b1fb4 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2196,19 +2196,26 @@ package body Sem_Ch3 is
                Spec := Specification (Original_Node (Decl));
                Sent := Defining_Unit_Name (Spec);
 
+               --  Analyze preconditions and postconditions
+
                Prag := Spec_PPC_List (Contract (Sent));
                while Present (Prag) loop
                   Analyze_PPC_In_Decl_Part (Prag, Sent);
                   Prag := Next_Pragma (Prag);
                end loop;
 
-               Check_Subprogram_Contract (Sent);
+               --  Analyze contract-cases and test-cases
 
                Prag := Spec_CTC_List (Contract (Sent));
                while Present (Prag) loop
                   Analyze_CTC_In_Decl_Part (Prag, Sent);
                   Prag := Next_Pragma (Prag);
                end loop;
+
+               --  At this point, entities have been attached to identifiers.
+               --  This is required to be able to detect suspicious contracts.
+
+               Check_Subprogram_Contract (Sent);
             end if;
 
             Next (Decl);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 6adcaa3..13fc5ab 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -6953,6 +6953,9 @@ package body Sem_Ch6 is
       --  Last postcondition on the subprogram, or else Empty if either no
       --  postcondition or only inherited postconditions.
 
+      Last_Contract_Case : Node_Id := Empty;
+      --  Last contract-case on the subprogram, or else Empty
+
       Attribute_Result_Mentioned : Boolean := False;
       --  Whether attribute 'Result is mentioned in a postcondition
 
@@ -6971,9 +6974,14 @@ package body Sem_Ch6 is
       --  reference to attribute 'Old, in order to ignore its prefix, which
       --  is precisely evaluated in the pre-state. Otherwise return OK.
 
+      procedure Process_Contract_Cases (Spec : Node_Id);
+      --  This processes the Spec_CTC_List from Spec, processing any contract
+      --  case from the list. The caller has checked that Spec_CTC_List is
+      --  non-Empty.
+
       procedure Process_Post_Conditions (Spec : Node_Id; Class : Boolean);
       --  This processes the Spec_PPC_List from Spec, processing any
-      --  postconditions from the list. If Class is True, then only
+      --  postcondition 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.
 
@@ -7056,6 +7064,57 @@ package body Sem_Ch6 is
          end if;
       end Check_Post_State;
 
+      ----------------------------
+      -- Process_Contract_Cases --
+      ----------------------------
+
+      procedure Process_Contract_Cases (Spec : Node_Id) is
+         Prag    : Node_Id;
+         Arg     : Node_Id;
+         Ignored : Traverse_Final_Result;
+         pragma Unreferenced (Ignored);
+
+      begin
+         Prag := Spec_CTC_List (Contract (Spec));
+
+         loop
+            --  Retrieve the Ensures component of the contract-case, if any
+
+            Arg := Get_Ensures_From_Case_Pragma (Prag);
+
+            if Pragma_Name (Prag) = Name_Contract_Case then
+
+               --  Since contract-cases are listed in reverse order, the first
+               --  contract-case in the list is the last in the source.
+
+               if No (Last_Contract_Case) then
+                  Last_Contract_Case := Prag;
+               end if;
+
+               --  For functions, look for presence of 'Result in Ensures
+
+               if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+                  Ignored := Find_Attribute_Result (Arg);
+               end if;
+
+               --  For each individual contract-case, look for presence
+               --  of an expression that could be evaluated differently
+               --  in post-state.
+
+               Post_State_Mentioned := False;
+               Ignored := Find_Post_State (Arg);
+
+               if not Post_State_Mentioned then
+                  Error_Msg_N ("?`Ensures` component refers only to pre-state",
+                               Prag);
+               end if;
+            end if;
+
+            Prag := Next_Pragma (Prag);
+            exit when No (Prag);
+         end loop;
+      end Process_Contract_Cases;
+
       -----------------------------
       -- Process_Post_Conditions --
       -----------------------------
@@ -7075,35 +7134,36 @@ package body Sem_Ch6 is
          loop
             Arg := First (Pragma_Argument_Associations (Prag));
 
-            --  Since pre- and post-conditions are listed in reverse order, the
-            --  first postcondition in the list is the last in the source.
+            if Pragma_Name (Prag) = Name_Postcondition then
 
-            if Pragma_Name (Prag) = Name_Postcondition
-              and then not Class
-              and then No (Last_Postcondition)
-            then
-               Last_Postcondition := Prag;
-            end if;
+               --  Since pre- and post-conditions are listed in reverse order,
+               --  the first postcondition in the list is the last in the
+               --  source.
 
-            --  For functions, look for presence of 'Result in postcondition
+               if not Class
+                 and then No (Last_Postcondition)
+               then
+                  Last_Postcondition := Prag;
+               end if;
 
-            if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
-               Ignored := Find_Attribute_Result (Arg);
-            end if;
+               --  For functions, look for presence of 'Result in postcondition
 
-            --  For each individual non-inherited postcondition, look for
-            --  presence of an expression that could be evaluated differently
-            --  in post-state.
+               if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+                  Ignored := Find_Attribute_Result (Arg);
+               end if;
 
-            if Pragma_Name (Prag) = Name_Postcondition
-              and then not Class
-            then
-               Post_State_Mentioned := False;
-               Ignored := Find_Post_State (Arg);
+               --  For each individual non-inherited postcondition, look
+               --  for presence of an expression that could be evaluated
+               --  differently in post-state.
 
-               if not Post_State_Mentioned then
-                  Error_Msg_N ("?postcondition refers only to pre-state",
-                               Prag);
+               if not Class then
+                  Post_State_Mentioned := False;
+                  Ignored := Find_Post_State (Arg);
+
+                  if not Post_State_Mentioned then
+                     Error_Msg_N ("?postcondition refers only to pre-state",
+                                  Prag);
+                  end if;
                end if;
             end if;
 
@@ -7119,6 +7179,8 @@ package body Sem_Ch6 is
          return;
       end if;
 
+      --  Process spec postconditions
+
       if Present (Spec_PPC_List (Contract (Spec_Id))) then
          Process_Post_Conditions (Spec_Id, Class => False);
       end if;
@@ -7135,15 +7197,34 @@ package body Sem_Ch6 is
 --           end if;
 --        end loop;
 
+      --  Process contract cases
+
+      if Present (Spec_CTC_List (Contract (Spec_Id))) then
+         Process_Contract_Cases (Spec_Id);
+      end if;
+
       --  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 (Present (Last_Postcondition)
+                    or else Present (Last_Contract_Case))
         and then not Attribute_Result_Mentioned
       then
-         Error_Msg_N ("?function postcondition does not mention result",
-                      Last_Postcondition);
+         if Present (Last_Postcondition) then
+            if Present (Last_Contract_Case) then
+               Error_Msg_N ("?neither function postcondition nor " &
+                              "contract cases do mention result",
+                            Last_Postcondition);
+
+            else
+               Error_Msg_N ("?function postcondition does not mention result",
+                            Last_Postcondition);
+            end if;
+         else
+            Error_Msg_N ("?contract cases do not mention result",
+                         Last_Contract_Case);
+         end if;
       end if;
    end Check_Subprogram_Contract;