主要入口点函数是（可能）递归的

Question

当尝试使用 Frama-C 的 WP 证明器时，通过传递以下内容：

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

我收到错误：

[wp] User Error: Main entry point function 'foo' is (potentially) recursive.

以下是

foo.c

的内容：

int foo(void)
{
    return 1;
}

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

WP 插件似乎检测到所选的主函数

foo

在其他地方被调用，因此假定存在递归的可能性。当main中对

foo

的调用被注释掉后，就不存在这样的错误了

我的问题是：这个错误的确切含义是什么？此外，我如何告知插件事实上并非如此？

Answer 1

出现该消息是因为程序中调用了已知为主入口点 (

foo

) 的函数（语法上）。目前，无法消除此警告。

我建议在 Frama-C 的公共 GitLab 上为此创建一个问题。