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

Question

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

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

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

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

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

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

Answer 1

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

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

-l         pass additional options to the linker