Frama-C and XML parser

3
votes

I'm developing a plugin in Frama-C. I want to parse an xml file. I installed the package libxml-light-ocaml-dev but I get an error "Unbound module Xml" in compiling. I don't know how to proceed to make the package visible to Frama-C. Or should I use another package?

1
ocamlframa-c
The OCaml compiler option -I serves to make directories that contain libraries visible to the OCaml compiler when compiling a module that uses these libraries. - Pascal Cuoq
I'm not compiling with ocamlc directly but I'm using a frama-c makefile. So I compile with make. And my Makefile contains this : FRAMAC_SHARE := $(shell frama-c -print-path) FRAMAC_LIBDIR := $(shell frama-c -print-libpath) PLUGIN_NAME = Ctt PLUGIN_CMO = ctt_utils ctt_core ctt_trace ctt include $(FRAMAC_SHARE)/Makefile.dynamic - Amiramet

1 Answers

4
votes

Assuming you're using Makefile.dynamic as indicated in Frama-C's developer manual, there are a few variables that you have to tweak in order to compile and link your plug-in against external libraries:

  • PLUGIN_BFLAGS allows to pass extra options to OCaml's bytecode compiler, such as -I /my/path/to/xml/library, -I `ocamlfind xml-light`, or -I $(XMLLIGHTPATH) where XMLLIGHTPATH is set up by your configure script (see also developer manual for that).
  • PLUGIN_OFLAGS is the equivalent for native compilation
  • PLUGIN_EXTRA_BYTE gives a list of files that your plug-in has to be linked against when compiled in bytecode, such as xmllight.cma
  • PLUGIN_EXTRA_OPT is the native code equivalent, such as xmllight.cmxa