Как 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, чтобы увидеть значение х)

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

Answer 1

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

---

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

    else
    {
        return 1;
    }
}