[Ada] Warning on recursive call within postcondition

This patch adds a warning to a function call that appears within a
postcondition for said function. This may mean an omission of an attribute
reference 'Result, and may lead to an infinite loop on a call to that function.

Compiling post_error.ads must yield:

post_error.ads:3:11:
        warning: postcondition does not mention function result
post_error.ads:3:19:
       warning: call to "Foo" within its postcondition will lead
         to infinite recursion
----
package Post_Error is
   function Foo (A : out Integer) return Integer
     with Post => Foo (A)  /= 0;
   pragma Import (C, Foo);
end Post_Error;

2018-05-28  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* sem_util.adb (Is_Function_Result): Add a warning if a postcondition
	includes a call to function to which it applies. This may mean an
	omission of an attribute reference 'Result, in particular if the
	function is pqrameterless.

From-SVN: r260818

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 10b2c21fa38541634f35a33bf711752b90ab40f1..6f08ad2efff0ee57a5ef2d3414f06808bb9c886b 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2018-05-28  Ed Schonberg  <schonberg@adacore.com>
+
+       * sem_util.adb (Is_Function_Result): Add a warning if a postcondition
+       includes a call to function to which it applies. This may mean an
+       omission of an attribute reference 'Result, in particular if the
+       function is pqrameterless.
+
 2018-05-28  Justin Squirek  <squirek@adacore.com>
 
        * sem_ch8.adb (Find_Expanded_Name): Add extra guard to make sure the

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 033903c09eadd0e83f3b08865092f2957628726e..facacbea21353cee3da9ccc76419e481539e836c 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -3880,6 +3880,17 @@ package body Sem_Util is
                Result_Seen := True;
                return Abandon;
 
+            --  Warn on infinite recursion if call is to current function.
+
+            elsif Nkind (N) = N_Function_Call
+              and then Is_Entity_Name (Name (N))
+              and then Entity (Name (N)) = Subp_Id
+              and then not Is_Potentially_Unevaluated (N)
+            then
+               Error_Msg_NE ("call to & within its postcondition "
+                 & "will lead to infinite recursion?", N, Subp_Id);
+               return OK;
+
             --  Continue the traversal
 
             else