寻找在frama-c期间覆盖函数的想法

Question

我正在寻找如何在不修改源代码的情况下覆盖函数的想法。就像我在原始源中有foo（）一样，我想用我自己的版本用相同的函数名覆盖它，方法是将它添加到C文件中，该文件也可能包含其他覆盖函数。有点像强/弱编译。目前我必须使用__FRAMAC__进入源文件和ifdef。我不想触摸源文件。是否有一些内核选项不使用foo（）函数的第二个实例？

Answer 1

您的问题未指定是否要替换函数声明或函数定义。由于Frama-C对它们的处理方式不同，我将详细介绍它们。

Duplicate definitions at the kernel level

目前，在解析级别，Frama-C中没有选项可以完全忽略为解析而给出的一个文件中存在的函数的定义。 Frama-C AST将包含它找到的所有函数的定义。强/弱符号没有确切的等价物。

如果找到相同功能的第二个定义，则会发生以下情况之一：

1. 如果两个定义都出现在同一个编译单元中，则会出错。
2. 如果每个定义都在不同的编译单元中发生，Frama-C将尝试找到一个合理的解决方案： 如果两个事件具有相同的签名，Frama-C将发出警告，例如：

   [kernel] b.c:2: Warning: 
     dropping duplicate def'n of func f at b.c:2 in favor of that at a.c:1

   在这种情况下，您只需要确保您想要的定义稍后出现在要解析的源列表中。 如果事件具有不同的签名，但实际上从未使用过其中一个函数，则可能会出现如下警告：

   [kernel:linker:drop-conflicting-unused] Warning: 
     Incompatible declaration for f:
     different number of arguments
     First declaration was at a.c:1
     Current declaration is at b.c:2
     Current declaration is unused, silently removing it

   但是，如果同时使用两种情况，则会出现错误：

   [kernel] User Error: Incompatible declaration for f:
     different type constructors: int vs. int *
     First declaration was at a.c:1
     Current declaration is at b.c:2

Duplicate declarations at the kernel level

考虑到函数声明，Frama-C将根据C标准接受尽可能多的函数声明，只要它们兼容即可。如果他们有ACSL规范，那么这些规范将被合并。

如前所述，处理多个不兼容的声明，并根据是否使用两个版本发出警告或错误（在这种情况下，Frama-C无法选择）。

Plugin-specific options

插件可能具有特定选项来覆盖AST中函数的默认行为。例如，Eva有选项-eva-use-spec <fns>，它告诉分析忽略函数<fns>的定义，而只使用它们的规范。