如何在Frama-C中打印循环不变量及获取程序状态P1？

一、打印循环不变量 #

Frama-C的WP插件可直接输出验证过程中使用的循环不变量，通过以下命令实现：

• 基础输出：运行frama-c -wp -wp-print test.c，-wp-print参数会打印你手动标注的loop invariant x <= y，以及WP验证过程中依赖的相关逻辑断言。
• 详细调试信息：若需查看不变量推导细节，添加-wp-debug选项，命令为frama-c -wp -wp-print -wp-debug test.c，会输出更多中间验证步骤的状态和不变量分析过程。

二、获取P1位置的程序状态 #

可通过三种方式获取代码中P1位置的状态：

1. 添加断言触发状态输出
   在P1位置上方添加断言注释，修改后代码如下：

requires x <= y;
ensures x = y;
void test(int x, int y) {
  /*@ loop invariant x <= y;
   */
  while(x <= y) {
    /*@ assert \true; */ // 触发状态输出
    x = x + 1; // P1
  }
}

运行frama-c -wp -wp-print test.c，WP会输出该断言处的程序状态，包含x、y的取值关系（比如此时满足循环条件x <= y，以及赋值前的x值约束等）。

2. 使用EVA值分析插件
   EVA插件通过抽象解释分析程序执行路径，输出指定位置的状态：
   运行命令frama-c -eva -eva-show-states test.c，-eva-show-states会显示P1位置的抽象状态，比如x的取值范围、与y的约束关系等。若需更精准分析，可搭配-eva-level high提升分析精度。

3. 使用幽灵代码打印状态
   在P1位置添加幽灵代码（不影响程序实际执行，仅用于验证时输出）：

requires x <= y;
ensures x = y;
void test(int x, int y) {
  /*@ loop invariant x <= y;
   */
  while(x <= y) {
    /*@ ghost printf("P1位置状态: x=%d, y=%d\n", x, y); */
    x = x + 1; // P1
  }
}

运行frama-c -wp -wp-rte test.c，幽灵代码会在验证过程中打印P1位置的x、y状态信息。

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