This project is read-only.

Warning with recursive function definitions

Nov 18, 2010 at 6:02 AM

The page on "Loops and Invariants" shows an iterative program for computing the n'th Fibonacci number, using a recursive definition as the spec for what the function is supposed to compute.  See


However, when I run the (final) program shown on that page, VCC warns about possible unsoundness:

$ vcc fib.c

F:\private\work\cs116\vcc-tests\fib.c(3,1) : warning VC9303: [possible unsoundness]: cycle in pure function calls: fib -> fib

F:\private\work\cs116\vcc-tests\fib.c(3,1) : warning VC9310: [possible unsoundness]: a non-equality postcondition in a pure function (not ensures(result == ...))

Verification of fib succeeded.

Are these warnings expected?  This is with an SVN checkout from a couple of days ago (Nov 15).

Nov 18, 2010 at 8:52 AM


  yes, these warnings are currently expected. For soundness reasons, pure functions must have a witness. For a certain form of pure functions, VCC can guarantee this by construction, and these warnings will go away (see The fib() function doesn't meet this form (it's recursive), so it's currently the users responsibility to make sure it is "terminating". There is an issue (, in which a generalized check is suggested.

Best, Mark