Warning with recursive function definitions

Nov 18, 2010 at 5: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 7: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 http://vcc.codeplex.com/wikipage?title=Pure%20functions). 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 (http://vcc.codeplex.com/workitem/2973), in which a generalized check is suggested.

Best, Mark