CODEWITHSUNDEEP
frama-c
nleitao
nleitao

Reputation: 13

Cannot load a plugin to frama-c with call to ocamlyices functions

I am trying to develop a plugin to frama-c. I did build the application, which has several files, and then created the makefile referencing all the files i needed.

I am able to use make and then make install and execute the plugin. My problem appears when i call functions from the ocamlyices library in a function...

I am still able to do the make and make install and when i try to execute i get the following error:

[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.

So it says it is incompatible when I add the call to ocamlyices functions. Is there any option/configuration I am missing somewhere?

Thank you for your help.

The final solution looked like this:

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

The variable $(YICES) is defined as 

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

Upvotes: 1

Views: 222

Answers (1)

Virgile
Virgile

Reputation: 10148

As mentioned by Anne, if your plug-in uses an external library that is not already included by Frama-C itself, you need a few more steps than for a basic plug-in, especially setting PLUGIN_EXTRA_BYTE and PLUGIN_EXTRA_OPT to the external libraries that you want to be linked to your plug-in. It might also be necessary to adapt the flags passed to the linker with PLUGIN_LINK_BFLAGS and PLUGIN_LINK_OFLAGS, but this is heavily dependent on ocamlyices itself. More information on the variables that can be used to customize the compilation of your plug-in can be found in section 5.3.3 of Frama-C's development guide.

Upvotes: 1

Related Questions