Вопросы по теме 'frama-c'
Опция Frama-C -no-simplify-cfg не работает
Я использую Frama-C для вычисления фрагмента программы C. Я хочу, чтобы нарезанная программа выглядела как оригинал без преобразования кода. Однако в результирующем фрагменте у меня всегда есть операторы goto и метки. Я использую команду:...
183 просмотров
schedule
05.05.2023
Аннотации ACSL к макросам C
Можно ли аннотировать макросы C с помощью ACSL?
eg:
/*@
assigns \nothing;
behavior xmin:
assumes x < y;
ensures \result == x;
behavior ymin:
assumes y <= x;
ensures \result == y;
disjoint...
406 просмотров
schedule
02.05.2022
Проблема проверки с использованием плагина Jessie и Frama-C
Я новичок в Frama-C и хочу правильно изучить синтаксис ACSL. У меня есть этот фиктивный пример, и подключаемый модуль Jessie не может проверить строки № 9 и 12. Я что-то упустил? Проверяемая функция (равно) проверит, имеют ли два массива (a и b)...
296 просмотров
schedule
10.04.2023
Невозможно доказать оговорку о назначении - Frama-C
Я новичок в Frama-c и хотел бы понять, в чем проблема с этим простым примером:
/*@ requires \valid(array+(0..length-1))
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0;
@ assigns array[0..length-1];
*/
void fill(int...
922 просмотров
schedule
23.07.2023
Как контролировать размер основных арифметических типов во Frama-C?
Во Frama-C можно ли свободно указывать размеры основных типов?
Моя цель, TMS320F2808 DSP, имеет 16-битные байты. Типы char, short и int имеют один байт, а тип long — два.
Пока я не вижу, как, если это возможно, я могу указать Frama-C эти размеры.
338 просмотров
schedule
03.06.2023
Объявление типа с использованием вещественных чисел в ACSL/Frama-C
У меня есть некоторые проблемы со спецификацией ACSL для последней версии Frama-C. Я много раз пытался объявить пару вещественных чисел, но ни один из них не работал. Вот крошечный пример, иллюстрирующий проблему:
/*@ type real_pair = (real,...
108 просмотров
schedule
18.10.2022
frama-c [ядро] ошибка пользователя: пропуск файла selection.c, в котором есть ошибки
Я новый пользователь Frama-c. Я только что установил Neon-20140301 и почему 2.34 в моей системе Fedora 14 с компилятором Ocaml 4.01.0.
В режиме без графического интерфейса установка прошла успешно.
Однако, когда я попытался запустить некоторые...
195 просмотров
schedule
28.03.2023
Можно ли получить обратный динамический срез во Frama-C?
Я получаю обратный срез от Frama-c, но похоже, что это статический, а не динамический срез.
Есть ли в frama-c конкретная опция для получения динамического обратного среза?
258 просмотров
schedule
05.05.2022
Установка Frama-c Sodium/Fluorine в Ubuntu 14.04 из исходников
Я пытаюсь установить frama-c из исходного кода в Ubuntu 14.04, но это невозможно.
Фтор делает ошибку:
allberson@allberson-Aspire-E1-531:~/Área de Trabalho/frama-c-Fluorine-20130601$ make
Generating src/lib/dynlink_common_interface.ml...
288 просмотров
schedule
06.07.2023
Frama-c не может проанализировать приведенный вручную пример ACSL list_length, включающий конструкцию сопоставления с образцом
В следующем определении функции (list.c):
//@ type list<A> = Nil | Cons(A,list<A>);
/*@ logic integer list_length<A>(list<A> l) =
@ \match l {
@ case Nil : 0
@ case Cons(h,t) : 1 + list_length(tail)
@ };
*/...
107 просмотров
schedule
07.07.2022
Как использовать функции в модулях Value.Eval_expr, Value.Eval_op и т. д. плагина Frama-c Value
Я пытаюсь создать плагин frama-c. Этот плагин зависит от плагина Frama-c Value. Я хочу получить и распечатать набор значений всех значений lvalue в исходном коде C. Для этого я хочу использовать функции, доступные в Value.Eval_exprs, Value.Eval_op...
243 просмотров
schedule
20.05.2022
Расчет достижимости функции с помощью анализа значений frama-c
Вот мой пример:
int in;
int sum(int n){
int log_input = n;
int log_global = in;
return 0;
}
int main(){
int n = Frama_C_interval(-10, 10);
in = n;
if (n > 0){
sum(n + 4);
}
return 0;
}
Что я хотел...
143 просмотров
schedule
03.11.2022
Frama-C делает ошибку
Моя настройка среды — Ubuntu 14.04 LTS x86_64:
После того, как я "./configure" и затем "make", появляются следующие ошибки:
Ocamlc src/plugins/value/gui_eval.cmi
Ocamlc src/plugins/value/gui_eval.cmo
Ocamlc...
152 просмотров
schedule
06.02.2024
Frama-C: нет разделения оператора if
У меня возникла следующая проблема при анализе if-условий с помощью моего плагина. Когда я анализирую код, например
if ((a && b) || c)
Frama-C создает такой код:
if (a) {
if (b){
goto _LOR;
}
else{...
152 просмотров
schedule
08.06.2023
Недопустимое утверждение для проверки переполнения Frama-C
При проверке переполнения для типов данных short и char для операции добавления утверждения, вставленные Frama-C, кажутся неверными:
Для char и коротких данных максимальные положительные и отрицательные значения имеют целочисленный тип...
151 просмотров
schedule
27.09.2022
Frama-C генерирует запутанные утверждения о сравнении указателей
Я получаю утверждения, которые не имеют смысла для меня.
Код:
struct s {
int pred;
};
/*@ assigns \result \from \nothing;
ensures \valid(\result);
*/
struct s *get(void);
int main(void)
{
return !get()->pred;
}
Выход...
146 просмотров
schedule
27.11.2022
Установка Frama-c - настроить: ошибка: не удается найти ocamlfind
xhy0908deMacBook-Pro:frama-c-Phosphorus-20170501 xhy0908$ ./configure
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
checking version of make... 3.81
configure:...
361 просмотров
schedule
17.05.2024
Как использовать подключаемый модуль Frama-C WP для расчета самых слабых формул предварительных условий?
Я реализую статический анализ в качестве плагина для Frama-C, и в рамках этого анализа мне нужно сгенерировать самые слабые формулы предварительных условий. Я нашел этот связанный вопрос: Как использовать ли результаты WP в другом плагине? ,...
173 просмотров
schedule
30.07.2022
Ошибка компиляции E-ACSL FRAMA-C
Я новичок в фреймворке Frama-C и пытаюсь провести контрактное тестирование с программами на C. Я намерен использовать для этого подключаемый модуль E-ACSL, и я пробовал тестовую программу, чтобы увидеть, как она работает, но получаю некоторые ошибки...
103 просмотров
schedule
14.05.2022
Я не могу открыть какие-либо файлы .C с помощью Frama-c и получаю только сообщения о недопустимых ошибках пользовательского ввода.
Я новичок в Frama-c и совсем новичок в программировании в целом. Я установил Frama-C на свой Mac. Я использую ОСХ. Из командной строки я ввожу Frama-C-Gui, который открывается нормально, и в это время я выбираю «Новый проект» Графический интерфейс...
196 просмотров
schedule
30.07.2022
