Frama-C e-acsl插件未为.i文件中所有断言生成__e_acsl_assert

问题重现 #

• 作为Frama-C新手，使用e-ACSL插件进行代码验证，编写了包含两个断言的first.i文件
• 执行以下命令生成监控代码后，未找到对应x==1的__e_acsl_assert代码：

  frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c
  

• 改用e-ACSL官方脚本生成，问题依旧：

  e-acsl-gcc.sh -c -omonitored_first.i first.i
  

• 运行生成的a.out.e-acsl未触发预期的断言失败提示
• 环境差异表现：
  • Ubuntu 22.04 + Opam 2.1.2 + Frama-C 25.0：执行命令时出现宏重定义警告
  • Ubuntu 20.04 + Opam 2.0.5 + Frama-C 25.0：无警告，但运行结果不符合预期

可能的原因与解决步骤 #

1. 断言语法或位置不符合e-ACSL要求 #

e-ACSL仅识别标准ACSL格式的断言注释，需确保：

• 断言使用/*@ assert <condition>; */格式，而非普通注释或代码语句
• 断言放置在代码的有效位置（如函数内部、语句前后），未被预处理阶段移除（.i文件是预处理后输出，可能已丢失ACSL注释）

2. 补充e-ACSL强制处理所有断言的参数 #

默认情况下，e-ACSL可能跳过部分断言，需添加-e-acsl-assert-all参数强制处理所有断言：

• 使用Frama-C命令生成：

  frama-c -e-acsl -e-acsl-assert-all first.i -then-last -print -ocode monitored_first.c
  

• 使用e-acsl-gcc.sh脚本生成：

  e-acsl-gcc.sh -c -omonitored_first.i -e-acsl-assert-all first.i
  

3. 改用未预处理的.c文件作为输入 #

.i文件是C预处理后的产物，可能已移除ACSL注释或修改代码结构，导致e-ACSL无法识别断言。建议直接使用原始.c文件（保留ACSL断言注释）作为输入重新生成。

4. 解决Ubuntu 22.04的宏重定义警告 #

Ubuntu 22.04的GCC版本较高，可能与e-ACSL生成的监控代码宏冲突，可添加编译参数抑制警告并验证：

frama-c -e-acsl first.c -then-last -print -ocode monitored_first.c -cclib "-Wno-macro-redefined"

5. 检查并修复Frama-C环境依赖 #

不同Opam环境下的依赖可能存在差异，可重新安装e-ACSL插件确保依赖完整：

opam reinstall frama-c-e-acsl

同时验证GCC、Binutils等工具版本与Frama-C 25.0兼容。

验证示例 #

编写标准带ACSL断言的first.c：

#include <stdio.h>

int main() {
    int x = 0;
    /*@ assert x == 0; */
    x = 2;
    /*@ assert x == 1; */ // 预期触发断言失败
    printf("%d\n", x);
    return 0;
}

执行生成与运行命令：

frama-c -e-acsl -e-acsl-assert-all first.c -then-last -print -ocode monitored_first.c
gcc monitored_first.c -o monitored_first
./monitored_first

正常情况下，运行会输出断言失败提示，如__e_acsl_assert failed: file first.c, line 7, function main: x == 1

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