Document recursive functions support in contracts

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

Currently we:

• rename the target function, say f, to original_f
• generate a wrapper function with the same name and insert assumptions & assertions as per the contracts
• all calls to original_f are now replaced with calls to the wrapper f because of renaming

This would result in unsoundness for recursive functions. For example, consider the test.c file below:

int f(int y)
__CPROVER_requires(y >= 0)
__CPROVER_ensures(y >= 0)
{
    if (y < 0)
        return y;
    else
    {
        f(-1);
        assert(0);
    }
}

• Running cbmc --function f test.c reports a failure, as expected
• However, running goto-cc --function f test.c -o test.goto && goto-instrument --enforce-contract f test.goto test_enforced.goto && cbmc test_enforced.goto reports success!

A Possible Fix

As discussed, one way to fix this would be to:

• preserve the name for the original function, no original_f
• create a new name for the wrapper function f_enforced or something like that
• replace the call to f with a call to f_enforced only at the entry point (the first call in the CFG)

[feliperodri]

@remi-delmas-3000 haven't you address this issue with the latest DFCC work?

[remi-delmas-3000]

contract checking with DFCC has basic support for recursive functions (without termination proofs however) but it is not properly documented. I'll create a PR to update the documentation.