frama-c

Main entry point function is (potentially) recursive

When attempting to use Frama-C's WP prover, by passing in the following:

frama-c -lib-entry -main foo -wp foo.c

I am given the error: [wp] User Error: Main entry point function 'foo' is (potentially) recursive.

Here are the contents of foo.c:

int foo(void)
{
    return 1;
}

int main(/*int argc, char *argv[]*/)
{
    return foo();
}

It seems that the WP plugin detects that the elected main function foo is called elsewhere, and thus assumes a potential for recursion. When the call to foo in main is commented out, there is no such error.

My question is thus: what is the precise meaning of this error? Furthermore, how may I inform the plugin that this is in-fact not the case?

Solution

  • The message appears because the function that is known to be the main entry point (foo) is called in the program (syntactically). Currently, it is not possible to silence this warning.

    I'd suggest creating an issue for this on the public GitLab of Frama-C.