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

我有一个 16 位 MPU，其大小与 x86_16 不同size_t, ptrdiff_t等等。任何人都可以给我有关如何在 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 -打印共享路径)

PLUGIN_NAME=Custom_machdep
PLUGIN_CMO=my_machdep

include $(FRAMAC_SHARE)/Makefile.dynamic

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

UPDATE如果您使用 Frama-C 标准库中的一些标头，您还必须更新$(frama-c -print-share-path)/libc/__fc_machdep.h为了定义适当的宏（与limits.h and stdint.h大多）。