私は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"