Frama-C WP报错：主入口函数foo存在潜在递归的问题咨询

使用Frama-C的WP prover时执行命令：

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();
}

注释掉main函数中对foo的调用后错误消失，推测WP插件因检测到指定主入口函数foo被其他位置调用，便认定其存在潜在递归。现咨询：

1. 该错误的准确含义是什么？
2. 如何告知插件实际不存在递归？

错误的准确含义 #

WP插件要求通过-main指定的主入口函数只能作为程序起始点被调用，不能被其他函数直接或间接调用。当检测到该函数被其他函数（比如这里的main）调用时，WP会判定存在潜在递归风险——因为它无法通过静态分析完全排除调用链中出现循环调用该入口函数的可能（即便当前代码里没有递归逻辑），因此抛出该错误。

解决方法 #

有两种常用方式让WP插件确认实际无递归：

• 方式一：跳过调用入口函数的代码
  使用-wp-skip-func参数忽略调用foo的函数（如这里的main），修改后的命令为：

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

  这样WP会忽略main函数的代码，仅分析foo作为入口的场景，不会检测到对foo的调用。

• 方式二：添加非递归注解
  在代码中为foo添加Frama-C专属注解，声明其无递归属性：

  /*@ nonrecursive; */
  int foo(void)
  {
      return 1;
  }
  

  之后重新执行原命令，WP会识别该注解，确认foo无递归，不再抛出错误。

内容的提问来源于stack exchange，提问作者invertedPanda