使用 E-ACSL 插件时如何链接 C 文件？答案

【问题标题】：How can be C files linked when using E-ACSL plugin?使用 E-ACSL 插件时如何链接 C 文件？
【发布时间】：2018-04-26 13:15:00
【问题描述】：

我正在尝试使用 Frama-C E-ACSL 插件生成带注释的文件。我创建了以下文件：

在编译/检测程序时，手册指定了以下终端命令：

$ e-acsl-gcc.sh -c <files> -O <output>

为了成功编译 Insert.c 和 AxiomTest.c 必须链接，但我找不到任何标志。

有什么帮助吗？或者有没有其他方法可以做到这一点？

【问题讨论】：

你试过e-acsl-gcc.sh -c Insert.c AxiomTest.c -O my_executable吗？通常脚本应该接受许多源文件作为参数（因此在手册中是<files> 而不是<file>）。
Doing e-acsl-gcc.sh -c Insert.c AxiomTest.c -O my_executable 链接两个文件，但我仍然收到一条错误消息：unbound function foo。此函数 foo 在 Intert.c 文件中定义，并在 EACSL 的 @ requires 子句中的 AxiomTest.c 中调用注释。可能是 EACSL 不接受注解中的函数并产生错误？
您不能在 ACSL 注释中调用 C 函数（尽管您可以将它们称为函数指针，例如 my_fct_ptr == f1 || my_fct_ptr == f2），实际上：那里只允许使用逻辑函数和谓词。当然，如果在链接阶段之前发生错误，则不会生成任何可执行文件。如果您对 Frama-C/E-ACSL 报告的错误有特定问题，请创建一个新问题，并确保包含 MCVE，向我们展示您所面临的确切问题。

【解决方案1】：

e-acsl-gcc.sh 确实使用选项 -c 编译 和链接 文件，尽管它看起来只编译（这里的 -c 与 GCC 的 -c 选项无关，它只编译，没有链接）。

如果您想为链接器提供额外的标志，man e-acsl-gcc.sh（或e-acsl-gcc.sh -h）将指示选项-l：

-l         pass additional options to the linker

【讨论】：