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

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

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

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

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

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

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


frama-c acsl
person Raul Coroban    schedule 26.04.2018    source источник
comment
Вы пробовали e-acsl-gcc.sh -c Insert.c AxiomTest.c -O my_executable? Обычно скрипт должен принимать множество исходных файлов в качестве аргумента (отсюда <files>, а не <file> в руководстве).   -  person Virgile    schedule 26.04.2018
comment
Выполнение e-acsl-gcc.sh -c Insert.c AxiomTest.c -O my_executable связывает оба файла, но я все равно получаю сообщение об ошибке: unbound function foo. Эта функция foo определена в файле Intert.c и вызывается в AxiomTest.c внутри предложения @ requires из аннотаций EACSL. Может быть, EACSL не принимает функцию в аннотации и выдает ошибку?   -  person Raul Coroban    schedule 28.04.2018
comment
вы не можете вызывать функции C (хотя вы можете обращаться к ним как к указателю на функцию, например, my_fct_ptr == f1 || my_fct_ptr == f2) внутри аннотации ACSL действительно: там разрешены только логические функции и предикаты. И, конечно же, если ошибки произойдут до этапа компоновки, исполняемый файл не будет создан. Если у вас есть конкретные проблемы с ошибками, о которых сообщает Frama-C/E-ACSL, создайте новый вопрос и обязательно включите MCVE показывая нам точную проблему, с которой вы столкнулись.   -  person Virgile    schedule 28.04.2018

Ответы (1)


arrow_upward
0
arrow_downward

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
person anol    schedule 27.04.2018
comment
Мой -l говорит, что это для передачи флагов компоновщику. Он все еще не связывает файлы ... - person Raul Coroban; 28.04.2018