使用E-ACSL包装脚本分析代码时的头文件包含问题求助

错误核心在于：e-acsl-gcc.sh执行流程分为两步——先调用Frama-C完成E-ACSL转换，再调用gcc编译原始的doubly_linked.c。你仅将头文件路径参数-Iinclude/传给了Frama-C，未传递给后续的gcc编译阶段，导致gcc无法找到doubly.h。

方案1：同时向Frama-C和gcc传递头文件路径 #

使用--分隔Frama-C参数与gcc参数，确保两边都能获取到头文件包含路径：

e-acsl-gcc.sh -E "-Iinclude/" -- -Iinclude/ doubly_linked.c -c

也可以直接在命令末尾追加gcc的头文件参数：

e-acsl-gcc.sh -E "-Iinclude/" doubly_linked.c -c -Iinclude/

方案2：仅生成E-ACSL转换代码，跳过gcc编译 #

若你仅需要转换后的代码而非可执行文件，可添加--no-compile参数，让脚本只执行Frama-C的转换步骤：

e-acsl-gcc.sh -E "-Iinclude/" doubly_linked.c --no-compile

转换后的代码会输出到a.out.frama.c，后续自行编译时需为gcc添加-Iinclude/及E-ACSL依赖库参数。

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