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

我有一个16位的MPU,它与x86_16的大小不同size_t,ptrdiff_t等等.有人能给我详细说明如何为我的MPU定制Frama-C中的机器依赖性吗？

目前没有办法直接从命令行执行此操作:您必须编写一个小的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应my_machdep在已知machdep列表中输出来验证这一点.

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