Patchwork [Ada] Remove spurious warning with -gnatw.t on trivial postconditions

login
register
mail settings
Submitter Arnaud Charlet
Date March 19, 2012, 4:31 p.m.
Message ID <20120319163136.GA19507@adacore.com>
Download mbox | patch
Permalink /patch/147576/
State New
Headers show

Comments

Arnaud Charlet - March 19, 2012, 4:31 p.m.
It may be useful to have trivial postconditions of "True" or "False" on some
subprograms. The first is essentially a confirming postcondition, while the
second indicates that a procedure will not return (if postconditions are
checked). Do not emit warnings on such postconditions. Similarly for Ensures
components of contract-cases. GNAT does not issue warnings on the following
code:

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

     1. package P is
     2.    function Func return Boolean with
     3.      Post => True,
     4.      Contract_Case => (Name    => "all",
     5.                        Mode    => Nominal,
     6.                        Ensures => True);
     7.    procedure Proc with
     8.      Post => False,
     9.      Contract_Case => (Name    => "all",
    10.                        Mode    => Nominal,
    11.                        Ensures => False);
    12. end P;

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

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

	* sem_ch6.adb (Check_Subprogram_Contract): Do not emit warnings
	on trivially True or False postconditions and Ensures components
	of contract-cases.

Patch

Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 185520)
+++ sem_ch6.adb	(working copy)
@@ -6927,23 +6927,29 @@ 
 --                      Inherited_Subprograms (Spec_Id);
 --        --  List of subprograms inherited by this subprogram
 
+      --  We ignore postconditions "True" or "False" and contract-cases which
+      --  have similar Ensures components, which we call "trivial", when
+      --  issuing warnings, since these postconditions and contract-cases
+      --  purposedly ignore the post-state.
+
       Last_Postcondition : Node_Id := Empty;
-      --  Last postcondition on the subprogram, or else Empty if either no
-      --  postcondition or only inherited postconditions.
+      --  Last non-trivial postcondition on the subprogram, or else Empty if
+      --  either no non-trivial postcondition or only inherited postconditions.
 
       Last_Contract_Case : Node_Id := Empty;
-      --  Last contract-case on the subprogram, or else Empty
+      --  Last non-trivial contract-case on the subprogram, or else Empty
 
       Attribute_Result_Mentioned : Boolean := False;
-      --  Whether attribute 'Result is mentioned in a postcondition
+      --  Whether attribute 'Result is mentioned in a non-trivial postcondition
+      --  or contract-case.
 
       No_Warning_On_Some_Postcondition : Boolean := False;
-      --  Whether there exists a postcondition or a contract-case without a
-      --  corresponding warning.
+      --  Whether there exists a non-trivial postcondition or contract-case
+      --  without a corresponding warning.
 
       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.
+      --  Whether some expression mentioned in a postcondition or contract-case
+      --  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 if N is a reference to the attribute 'Result, and if so set
@@ -6956,6 +6962,9 @@ 
       --  reference to attribute 'Old, in order to ignore its prefix, which
       --  is precisely evaluated in the pre-state. Otherwise return OK.
 
+      function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean;
+      --  Return whether node N is trivially "True" or "False"
+
       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
@@ -7046,13 +7055,26 @@ 
          end if;
       end Check_Post_State;
 
+      --------------------------------
+      -- Is_Trivial_Post_Or_Ensures --
+      --------------------------------
+
+      function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean is
+      begin
+         return Is_Entity_Name (N)
+           and then (Entity (N) = Standard_True
+                       or else
+                     Entity (N) = Standard_False);
+      end Is_Trivial_Post_Or_Ensures;
+
       ----------------------------
       -- Process_Contract_Cases --
       ----------------------------
 
       procedure Process_Contract_Cases (Spec : Node_Id) is
-         Prag    : Node_Id;
-         Arg     : Node_Id;
+         Prag : Node_Id;
+         Arg  : Node_Id;
+
          Ignored : Traverse_Final_Result;
          pragma Unreferenced (Ignored);
 
@@ -7063,8 +7085,12 @@ 
 
             Arg := Get_Ensures_From_CTC_Pragma (Prag);
 
-            if Pragma_Name (Prag) = Name_Contract_Case then
+            --  Ignore trivial contract-case when Ensures component is "True"
+            --  or "False".
 
+            if Pragma_Name (Prag) = Name_Contract_Case
+              and then not Is_Trivial_Post_Or_Ensures (Expression (Arg))
+            then
                --  Since contract-cases are listed in reverse order, the first
                --  contract-case in the list is the last in the source.
 
@@ -7088,8 +7114,8 @@ 
                if Post_State_Mentioned then
                   No_Warning_On_Some_Postcondition := True;
                else
-                  Error_Msg_N ("?`Ensures` component refers only to pre-state",
-                               Prag);
+                  Error_Msg_N
+                    ("?`Ensures` component refers only to pre-state", Prag);
                end if;
             end if;
 
@@ -7116,8 +7142,11 @@ 
          loop
             Arg := First (Pragma_Argument_Associations (Prag));
 
-            if Pragma_Name (Prag) = Name_Postcondition then
+            --  Ignore trivial postcondition of "True" or "False"
 
+            if Pragma_Name (Prag) = Name_Postcondition
+              and then not Is_Trivial_Post_Or_Ensures (Expression (Arg))
+            then
                --  Since pre- and post-conditions are listed in reverse order,
                --  the first postcondition in the list is last in the source.