Patchwork [Ada] Issue warning on suspicious contract cases when -gnatw.t is set

login
register
mail settings
Submitter Arnaud Charlet
Date March 15, 2012, 9:06 a.m.
Message ID <20120315090653.GA1516@adacore.com>
Download mbox | patch
Permalink /patch/146861/
State New
Headers show

Comments

Arnaud Charlet - March 15, 2012, 9:06 a.m.
The warning option -gnatw.t already issued warnings on suspicious
postconditions. This extends it to contract cases, which is a GNAT
pragma/aspect allowing to express fine-grain contracts. GNAT now detects
these cases on the following code:

$ gcc -c -gnatc -gnatw.t -gnat12 p.ads

     1. package P is
     2.    function A_Is_Positive (X : Integer) return Boolean with
     3.      Contract_Case => (Name    => "normal case",
             |
        >>> warning: "Ensures" component refers only to pre-state
        >>> warning: contract cases do not mention result

     4.                        Mode    => Nominal,
     5.                        Ensures => X >= 0);
     6.    procedure A_Incr (X : in Integer; Y : out Integer) with
     7.      Contract_Case => (Name    => "normal case",
             |
        >>> warning: "Ensures" component refers only to pre-state

     8.                        Mode    => Nominal,
     9.                        Ensures => X = X + 1);
    10. end P;

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

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.

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 185415)
+++ sem_ch3.adb	(working copy)
@@ -2196,19 +2196,26 @@ 
                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);
Index: gnat_ugn.texi
===================================================================
--- gnat_ugn.texi	(revision 185410)
+++ gnat_ugn.texi	(working copy)
@@ -5696,9 +5696,11 @@ 
 @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}.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 185415)
+++ sem_ch6.adb	(working copy)
@@ -6953,6 +6953,9 @@ 
       --  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 @@ 
       --  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 @@ 
          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 @@ 
          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 @@ 
          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 @@ 
 --           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;