1

我正在尝试为 frama-c 开发一个插件。我确实构建了包含多个文件的应用程序，然后创建了makefile引用我需要的所有文件。

我可以使用make然后make install执行插件。当我在函数中调用ocamlyices库中的函数时出现我的问题...

我仍然可以进行 make 和 make install ，当我尝试执行时，出现以下错误：

[kernel] warning: cannot load plug-in 'name' (incompatible with Fluorine-20130601).

[kernel] user error: option `<name>' is unknown.
use `frama-c -help' for more information.

[kernel] Frama-C aborted: invalid user input.

所以它说当我添加对ocamlyices函数的调用时它是不兼容的。我在某处缺少任何选项/配置吗？

谢谢您的帮助。

最终解决方案如下所示：

FRAMAC_SHARE := $(shell frama-c.byte -print-path)
FRAMAC_LIBDIR := $(shell frama-c.byte -print-libpath)
PLUGIN_NAME = Fact

# All needed files
PLUGIN_CMO = ../base/basic_types concolic_search run_fact ../lib/lib 

PLUGIN_DOCFLAGS = -I ../base -I ../lib -I $(YICES) -I /usr/lib/ocaml/batteries -I ../instrumentation
PLUGIN_BFLAGS = -I ../base -I ../lib -I $(YICES) -I ../instrumentation 
PLUGIN_OFLAGS = -I ../base -I ../lib -I $(YICES) -I ../instrumentation 

PLUGIN_EXTRA_BYTE = $(YICES)/ocamlyices.cma 
PLUGIN_EXTRA_OPT = $(YICES)/ocamlyices.cmxa

include $(FRAMAC_SHARE)/Makefile.dynamic

变量 $(YICES) 定义为

export YICES="/usr/local/lib/ocaml/3.12.1/ocamlyices"
4

1 回答 1

1

正如 Anne 所提到的，如果您的插件使用了 Frama-C 本身尚未包含的外部库，那么您需要比基本插件更多的步骤，尤其是设置PLUGIN_EXTRA_BYTE您PLUGIN_EXTRA_OPT想要的外部库链接到您的插件。可能还需要使用 and 调整传递给链接器的标志PLUGIN_LINK_BFLAGS，PLUGIN_LINK_OFLAGS但这在很大程度上取决于它ocamlyices本身。有关可用于自定义插件编译的变量的更多信息，请参见Frama-C 开发指南的第 5.3.3 节。

于 2014-04-03T14:13:50.410 回答