[Ada] Warning on recursive call within postcondition
authorEd Schonberg <schonberg@adacore.com>
Mon, 28 May 2018 08:53:06 +0000 (08:53 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 28 May 2018 08:53:06 +0000 (08:53 +0000)
commit500b21ddb7ff3546e9b7f100b7414347661c7fb9
tree5f9b0020fa63bc8617650dcc88d3028160ca9795
parentaa76fac75101cd8694cedce1bee6a79f1f465130
[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
gcc/ada/ChangeLog
gcc/ada/sem_util.adb