This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Warning on recursive call within postcondition
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Ed Schonberg <schonberg at adacore dot com>
- Date: Mon, 28 May 2018 04:57:53 -0400
- Subject: [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;
Tested on x86_64-pc-linux-gnu, committed on trunk
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.--- gcc/ada/sem_util.adb
+++ 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