frama-c

4зной

2ответ

Получить результат в строковую переменную в OCaml

У меня есть эта функция работать, которая печатает значение в качестве offsetmap: let pretty_offsetmap_original lv fmt offsetmap = begin match offsetmap with | None -> Format.fprintf fmt "<B

4зной

1ответ

Невозможно доказать, присвойте положение - FRAMA-C

Я новичок в Фрам-с, и я хотел бы понять, что проблема с этим простым примером: /*@ requires \valid(array+(0..length-1)) @ ensures \forall integer k; 0 <= k < length ==> array[k] == 0; @ assigns arra

2зной

1ответ

Условная нарезка в Frama-C

Мой последний вопрос (Understanding Frama-C slicer results) был на конкретном примере, но, как я уже сказал, моя цель - узнать, можно ли сделать условную резку (вперед и назад) с помощью Frama-C. Явля

0зной

1ответ

ошибки при установке frama-c в cygwin

Я пытаюсь установить frama-c в cygwin и получить следующие ошибки, но я не могу их интерпретировать. Можете ли вы помочь мне интерпретировать их или дать мне ссылку на то, где я получаю информацию? Pr

1зной

1ответ

Использовать возможно неверный указатель в зависимостях ACSL

Мне нужно написать спецификацию ACSL для зависимостей функции, которая принимает указатель как входной, и использует его содержимое, когда указатель не равен NULL. Я думаю, что данная спецификация явл

3зной

1ответ

Проблема с проверкой с помощью Jessie plug-in и Frama-C

Я новичок в Frama-C, и я хочу правильно изучить синтаксис ACSL. У меня есть этот фиктивный пример, и плагин Jessie не может проверить строку № 9 и 12. Я что-то пропустил? Функция, которая должна быть

3зной

1ответ

Анализ крупных проектов с Фрама-C

Я хочу, чтобы проанализировать файл из большого проекта по созданию программы граф зависимостей, используя FRAMA-C, но продолжают получать странные ошибки, такие как: /usr/include/bits/fcntl-linux.h:3