frama-c - 如何在 Frama-C 中自定义机器依赖？

我有一个 16 位 MPU，它在 size_t 、 ptrdiff_t 等的大小上与 x86_16 不同。 谁能给我详细信息和明确说明如何在 Frama-C 中为我的 MPU 自定义机器依赖项？

最佳答案

目前无法直接从命令行执行此操作:您必须编写一个小的 OCaml 脚本，该脚本实质上将定义一个新的 Cil_types.mach(包含有关您的架构的必要信息的记录)并通过 File.new_machdep 注册它。假设你有一个看起来像这样的文件 my_machdep.ml:

let my_machdep = {
  Cil_types.sizeof_short = 2;
  sizeof_int = 2;
  sizeof_long = 4;
  (* ... See `cil_types.mli` for the complete list of fields to define *)
}

let () = File.new_machdep "my_machdep" my_machdep

然后，您将能够以这种方式启动 Frama-C 以使用新的 machdep:

frama-c -load-script my_machdep.ml -machdep my_machdep [normal options]

如果您想让新的 machdep 永久可用，您可以将其设为 Frama-C 插件。为此，您需要以下形式的 Makefile:

FRAMAC_SHARE:=$(shell frama-c -print-share-path)

PLUGIN_NAME=Custom_machdep
PLUGIN_CMO=my_machdep

include $(FRAMAC_SHARE)/Makefile.dynamic

my_machdep 必须是 .ml 文件的名称。请务必为 PLUGIN_NAME 选择不同的名称。然后，创建一个空的 Custom_machdep.mli 文件( touch Custom_machdep.mli 应该可以解决问题)。之后，make && make install 应编译并安装插件，以便 Frama-C 自动加载。您可以通过启动 frama-c -machdep help 来验证这一点，该代码应该在已知 machdeps 列表中输出 my_machdep。

更新
如果您使用的是 Frama-C 标准库中的一些头文件，您还必须更新 $(frama-c -print-share-path)/libc/__fc_machdep.h 以定义适当的宏(主要与 limits.h 和 stdint.h 相关)。

关于frama-c - 如何在 Frama-C 中自定义机器依赖？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/41823707/