寻找在 frama-c 期间覆盖函数的想法
Looking for idea on overwrite a function during frama-c
我正在寻找有关如何在不修改源代码的情况下覆盖函数的想法。就像我在原始源中有 foo() 一样，我想通过将它添加到 C 文件中，用我自己的具有相同函数名称的版本覆盖它，该文件可能还包含其他覆盖函数。有点像 strong/weak 编译。目前我必须使用 __FRAMAC__ 进入源文件和 ifdef。我不想触摸源文件。是否有一些内核选项不使用 foo() 函数的第二个实例？
你的问题没有具体说明你是想替换函数声明还是函数定义。由于 Frama-C 对它们的处理方式不同，我将详细介绍两者。
在内核级别重复定义
目前，在解析级别，Frama-C 中没有选项可以完全忽略存在于给定解析文件之一中的函数定义。 Frama-C AST 将合并它找到的所有函数的定义。
strong/weak 符号没有确切的等价物。
如果找到同一函数的第二个定义，将发生以下情况之一：
如果两个定义都出现在同一个编译单元中，就会出错。
如果每个定义发生在不同的编译单元中，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
在内核级别重复声明
考虑到函数 声明，Frama-C 将根据 C 标准接受尽可能多的声明，前提是它们是兼容的。如果他们有 ACSL 规范，这些规范将被合并。
多个不兼容的声明像以前一样处理，警告或错误取决于是否使用两个版本（在这种情况下 Frama-C 无法选择）。
插件特定选项
插件可能有特定的选项来覆盖 AST 中函数的默认行为。例如，Eva 有选项 -eva-use-spec <fns>，它告诉分析忽略函数的定义 <fns>，只使用它们的规范。
我正在寻找有关如何在不修改源代码的情况下覆盖函数的想法。就像我在原始源中有 foo() 一样，我想通过将它添加到 C 文件中，用我自己的具有相同函数名称的版本覆盖它，该文件可能还包含其他覆盖函数。有点像 strong/weak 编译。目前我必须使用 __FRAMAC__ 进入源文件和 ifdef。我不想触摸源文件。是否有一些内核选项不使用 foo() 函数的第二个实例？
你的问题没有具体说明你是想替换函数声明还是函数定义。由于 Frama-C 对它们的处理方式不同，我将详细介绍两者。
在内核级别重复定义
目前，在解析级别，Frama-C 中没有选项可以完全忽略存在于给定解析文件之一中的函数定义。 Frama-C AST 将合并它找到的所有函数的定义。 strong/weak 符号没有确切的等价物。
如果找到同一函数的第二个定义，将发生以下情况之一：
如果两个定义都出现在同一个编译单元中，就会出错。
如果每个定义发生在不同的编译单元中，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
在内核级别重复声明
考虑到函数 声明，Frama-C 将根据 C 标准接受尽可能多的声明，前提是它们是兼容的。如果他们有 ACSL 规范，这些规范将被合并。
多个不兼容的声明像以前一样处理，警告或错误取决于是否使用两个版本（在这种情况下 Frama-C 无法选择）。
插件特定选项
插件可能有特定的选项来覆盖 AST 中函数的默认行为。例如，Eva 有选项 -eva-use-spec <fns>，它告诉分析忽略函数的定义 <fns>，只使用它们的规范。