Как могут быть связаны файлы C при использовании плагина E-ACSL?

Question

Я пытаюсь создать аннотированный файл с помощью плагина Frama-C E-ACSL. Я создал следующие файлы:

• Insert.c : содержит все структуры для создания связанного списка.
• AxiomTest.c : включает основную функцию, в которой указываются утверждения, которые он должен выполнять. Все функции и структуры определены в терминах Insert.c file

При компиляции / инструментировании программы в руководстве указывается следующая команда терминала:

$ e-acsl-gcc.sh -c <files> -O <output>

Для успешной компиляции Insert.c и AxiomTest.c должны быть связаны, но я не могу найти никакого флага для этого.

Любая помощь? Или есть другой способ сделать это правильно?

Answer 1

e-acsl-gcc.sh компилирует и связывает файлы с параметром -c, несмотря на то, что он выглядит только при компиляции (-c здесь не связан с параметром -c GCC, который выполняет только компиляцию, без связь).

Если вы хотите присвоить компоновщику дополнительные флаги, man e-acsl-gcc.sh (или e-acsl-gcc.sh -h) укажет опцию -l:

-l         pass additional options to the linker