frama-c

2зной

1ответ

Как использовать эту функцию Db.Slicing.Select.select_stmt с FRAMA-C

Функция, которая в названии имеет следующую подпись: val select_stmt : (set -> spare:bool -> Cil_types.stmt -> Cil_types.kernel_function -> set) Pervasives.ref Я хотел бы использовать эту функ

1зной

1ответ

Плагин анализа влияния удара frama-C

Плагин анализа влияния имеет срез метода, который разрезает данный оператор в соответствии с анализом воздействия. Разве это как плагин для разрезания, где мы создаем проект, тогда мы выбираем зону ре

2зной

1ответ

Frama-с синтаксической ошибкой на макроподстановках

Я получаю следующую ошибку синтаксиса: ../stat-time.h:58:[kernel] user error: Cannot find field st_atim Это в ГНУ стате-time.h Пол Эггерт. Вот фрагмент кода вызывает ошибку: #define STAT_TIMESPEC(st

3зной

1ответ

Как доказать remove_copy из ACSL на примере

Я попытался доказать, что алгоритм удаляет копию (первая версия) из «ACSL по примеру» версии 11.1.0. Я использовал Alt-Ergo (0.99.1), CVC3 (2.4.1), Z3 (4.3.2), CVC4 (1.4) и Why3 (0.85). Ограничение вр

1зной

1ответ

Как отслеживать различия между исходным кодом C и предварительно обработанным кодом Frama-C?

В frama-C, когда я загружаю исходный файл, он выполняет предварительную обработку и выполняет автоматическую коррекцию ошибок, такую как «автоматический тип», как показано ниже (int is typecasted to

0зной

1ответ

Чтобы получить узел, соответствующий объявлению локальной переменной с Db.Pdg.find_decl_var_node

* Я написал этот скрипт, чтобы получить узел, соответствующий объявлению локальной переменной, в моем случае «val», который находится в небольшом количестве программа C, но я получаю ошибку Неожиданна

1зной

1ответ

Как вы объявляете предложение «присваивает» многомерным массивам в frama-c?

У меня есть следующие переменные: int** send_count; message_struct*** send_queue; И у меня есть функция я хочу объявить контракт на message_record_struct postSend(int destination, double* buf); К