Как cbmc работает с заголовком c?

Question

Если у меня есть ac-файл, который содержит более одной функции, и я хочу запустить cbmc с z3 solver для предварительно обработанной версии программы (используя gcc), а в разделе заголовка есть несколько других файлов (c-файлов),Как cbmc увидит эти файлы?потому что я попытался запустить его, и он выдает некоторые ошибки о некоторых переменных, которые не были объявлены, где они фактически объявлены в одном из заголовочных файлов.

Кто-нибудь может объяснить, как это работает?

ОБНОВЛЕНИЕ:

int test(int x) {
for (int i = 2; i < sqrt(x); i++) {
    if (x%i == 0)
        return 0;
}

Прежде всего, я предварительно обработал программу, используя gcc

Затем проанализировал программу с помощью pycparser

затем инструмент (добавить оператор печати после 4 впосмотрите значение x)

Затем я запустил cbmc для инструментированной версии файла и получил эту ошибку: функция `sqrt 'не объявлена ​​

Answer 1

Вы должны включить в проект все файлы, на которые ссылаются файлы заголовков.Недостаточно включить только правильный заголовок (и), если связанный файл .c недоступен.

---

Ваш пример кода ДОЛЖЕН иметь следующие строки:

    else
    {
        return 1;
    }
}