使用E-ACSL包装脚本时如何引入头文件？（Frama-C 24.0）

对于Frama-C的E-ACSL包装脚本e-acsl-gcc.sh，你可以通过-fc选项传递Frama-C所需的预处理参数，具体操作如下：

• 使用-fc将-cpp-extra-args参数传递给Frama-C，命令格式示例：

  e-acsl-gcc.sh --rte=all -c main.c -fc "-cpp-extra-args=\"-I src/include -I ...\""
  

  这里的-fc选项专门用于向底层调用的Frama-C实例传递参数，引号转义是为了确保shell将整个-cpp-extra-args参数正确传递给Frama-C。

• 原理说明：e-acsl-gcc.sh在处理流程中会先调用Frama-C完成E-ACSL的插桩和分析，你遇到的头文件找不到错误正是Frama-C的kernel模块在预处理阶段抛出的，因此通过-fc传递头文件路径参数，和你之前使用frama-c -rte时的逻辑完全一致，就能解决问题。

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