Как скомпилировать плагин Frama-C с исходным кодом C?

Я создал подключаемый модуль Frama-C, который использует исходный код .c, и я хотел бы его скомпилировать, но при добавлении

PLUGIN_EXTRA_OPT = file

в Makefile моего плагина я получаю следующую ошибку после запуска make:

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

Добавление VERBOSEMAKE=yes дает некоторую дополнительную информацию о причине ошибки:

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

Кажется, что по какой-то причине вызывается GCC, а не ocamlc.

Как я могу заставить make правильно скомпилировать исходники .c?


frama-c
person anol    schedule 17.06.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В этом случае правильный синтаксис для переменной PLUGIN_EXTRA_OPT должен включать расширение .o:

PLUGIN_EXTRA_OPT = file.o

Таким образом, Make применяет правильное правило и создает file.o с использованием ocamlc, а затем включает его в качестве дополнительного аргумента в команду ocamlopt, которая создает файл .cmx подключаемого модуля.

Предыдущая ошибка была вызвана тем, что Make применила неявное правило к несуществующей цели file, что продемонстрировано запуском 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'.
...
person anol    schedule 17.06.2015