Frama-C 24.0中E-ACSL脚本加-I选项后无法生成文件求助

1. 修正-E选项的参数格式 #

你当前用-E "-I src/include -I ..."的写法有问题——e-acsl-gcc.sh会把引号内的整段内容当作单个参数传递给预处理器，导致预处理器无法识别-I选项。正确的做法是去掉外层引号，直接拆分多个-I参数：

e-acsl-gcc.sh -E -I src/include -I ... main.c

如果路径包含空格，只给单个路径加引号即可，比如-I "src/my include dir"，别把所有-I参数包在一个引号里。

2. 开启调试输出排查问题 #

给脚本加-v（verbose）选项，能看到执行过程的详细日志，包括预处理器调用、Frama-C分析的错误信息：

e-acsl-gcc.sh -v -E -I src/include -I ... main.c

很多时候无输出是因为预处理器报错但脚本没捕获，或者Frama-C因头文件的语法/注解问题静默退出，调试日志能直接帮你定位根源。

3. 验证头文件与预处理流程 #

先单独用gcc完成预处理，再用脚本处理预处理后的文件，排查是头文件引入问题还是脚本参数解析问题：

# 先生成预处理后的代码
gcc -E -I src/include -I ... main.c > preprocessed.c
# 用脚本处理预处理文件
e-acsl-gcc.sh preprocessed.c

如果这一步能正常生成a.out.e-acsl，说明问题出在e-acsl-gcc.sh对-E参数的解析上，回到第一步调整格式即可。

另外要检查头文件的兼容性：

• 避免头文件里有Frama-C不支持的非标准语法或复杂宏
• 确保头文件里的ACSL注解符合规范，错误注解会导致Frama-C异常退出

4. 绕过包装脚本直接调用插件 #

Frama-C 24.0的E-ACSL包装脚本存在参数解析的小问题，你可以直接调用Frama-C插件完成流程，更透明也更容易排查错误：

# 用E-ACSL生成带 instrumentation 的代码
frama-c -e-acsl -cpp-extra-args="-I src/include -I ..." main.c -then -print -ocode main.e-acsl.c
# 编译生成可执行文件
gcc main.e-acsl.c -o a.out.e-acsl

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