frama-c - 使用 E-ACSL 插件时如何链接 C 文件？

Question

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

• Insert.c：包含创建链表的所有结构。
• AxiomTest.c：包括主要功能，其中指示了它必须满足的断言。所有功能和结构都根据Insert.c文件

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

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

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

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

Answer 1

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

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

-l         pass additional options to the linker