How to compile a Frama-C plug-in having a C source?

Question

I created a Frama-C plug-in which uses a .c source and I'd like to compile it, but when adding

PLUGIN_EXTRA_OPT = file

to my plug-in's Makefile, I obtain the following error after running make:

Packing      Myplugin.cmx
file.c:1:24: fatal error: caml/alloc.h: No such file or directory
 #include <caml/alloc.h>
                        ^
compilation terminated.

Adding VERBOSEMAKE=yes gives some additional information about the error cause:

...
gcc     file.c   -o file
file.c:1:24: fatal error: caml/alloc.h: No such file or directory
...

It seems that GCC is being called for some reason, instead of ocamlc.

How can I tell make to correctly compile my .c sources?

Answer 1

In this case, the right syntax for the PLUGIN_EXTRA_OPT variable is to include the .o extension:

PLUGIN_EXTRA_OPT = file.o

By doing so, Make applies the right rule and builds file.o using ocamlc, and then includes it as an additional argument to the ocamlopt command which builds the plug-in's .cmx file.

The previous error was caused by the fact that Make applied an implicit rule to the non-existing file target, as demonstrated by running make -d:

...
Considering target file `file'.
 File `file' does not exist.
 Looking for an implicit rule for `file'.
 Trying pattern rule with stem `file'.
 Trying implicit prerequisite `file.c'.
 Found an implicit rule for `file'.
...