| Message ID | 20180528085753.GA68242@adacore.com |
|---|---|
| State | New |
| Headers | show |
| Series | [Ada] Warning on recursive call within postcondition | expand |
--- 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
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.