public inbox for gcc-patches@gcc.gnu.org
 help / color / mirror / Atom feed
* [Ada] Spurious warning on postcondition and result
@ 2021-05-03  9:29 Pierre-Marie de Rodat
  0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-05-03  9:29 UTC (permalink / raw)
  To: gcc-patches; +Cc: Arnaud Charlet

[-- Attachment #1: Type: text/plain, Size: 571 bytes --]

When a function has "in out" parameters and a postcondition which does
not reference 'Result, a potentially spurious warning is emitted. The
necessary logic was actually already there in
Sem_Util.Check_Result_And_Post_State but was using a local
Has_In_Out_Parameter function instead of using simply
Einfo.Has_Out_Or_In_Out_Parameter.

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

gcc/ada/

	* sem_util.adb (Check_Result_And_Post_State): Replace custom
	Has_In_Out_Parameter with existing Has_Out_Or_In_Out_Parameter
	flag which corresponds exactly to what we need.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 2031 bytes --]

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4701,10 +4701,6 @@ package body Sem_Util is
       --  and post-state. Prag is a [refined] postcondition or a contract-cases
       --  pragma. Result_Seen is set when the pragma mentions attribute 'Result
 
-      function Has_In_Out_Parameter (Subp_Id : Entity_Id) return Boolean;
-      --  Determine whether subprogram Subp_Id contains at least one IN OUT
-      --  formal parameter.
-
       -------------------------------------------
       -- Check_Result_And_Post_State_In_Pragma --
       -------------------------------------------
@@ -5093,28 +5089,6 @@ package body Sem_Util is
          end if;
       end Check_Result_And_Post_State_In_Pragma;
 
-      --------------------------
-      -- Has_In_Out_Parameter --
-      --------------------------
-
-      function Has_In_Out_Parameter (Subp_Id : Entity_Id) return Boolean is
-         Formal : Entity_Id;
-
-      begin
-         --  Traverse the formals looking for an IN OUT parameter
-
-         Formal := First_Formal (Subp_Id);
-         while Present (Formal) loop
-            if Ekind (Formal) = E_In_Out_Parameter then
-               return True;
-            end if;
-
-            Next_Formal (Formal);
-         end loop;
-
-         return False;
-      end Has_In_Out_Parameter;
-
       --  Local variables
 
       Items        : constant Node_Id := Contract (Subp_Id);
@@ -5194,10 +5168,10 @@ package body Sem_Util is
          null;
 
       --  Regardless of whether the function has postconditions or contract
-      --  cases, or whether they mention attribute 'Result, an IN OUT formal
+      --  cases, or whether they mention attribute 'Result, an [IN] OUT formal
       --  parameter is always treated as a result.
 
-      elsif Has_In_Out_Parameter (Spec_Id) then
+      elsif Has_Out_Or_In_Out_Parameter (Spec_Id) then
          null;
 
       --  The function has both a postcondition and contract cases and they do



^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2021-05-03  9:29 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-05-03  9:29 [Ada] Spurious warning on postcondition and result Pierre-Marie de Rodat

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).