Вопросы по теме 'frama-c'
Значение \ old в пост-условиях ACSL
Я новичок в Frama-C, и у меня есть несколько вопросов относительно утверждений относительно указателей.
Рассмотрим фрагмент C ниже, включающий:
две связанные структуры данных Data и Handle, s.t. Handle имеет указатель на данные;
поле...
270 просмотров
schedule
23.10.2021
Логическая ошибка набора ACSL / синтаксическая ошибка frama-c
Я использую азотную версию Frama-c на Mac и, похоже, не могу использовать логику "set", как описано в руководстве ACSL, например, я не могу объявить призрачную переменную, как в "// @ набор призраков ‹integer› someSet; ".
Программа frama-c всегда...
321 просмотров
schedule
20.09.2021
Frama-C: компиляция в Cygwin / Windows 8.1
Легкий вопрос для тех, кто компилирует C для windows!
Я хочу использовать последнюю версию статического анализатора Frama-C C и его графический интерфейс в Windows 8. Пока Насколько я могу судить, самая последняя версия, в которой есть установщик...
761 просмотров
schedule
08.09.2021
Frama-C Gui на mavericks не работает
Кто-нибудь устанавливал Frama-C на Mavericks? Потому что я не могу его установить или не знаю, как его установить (версия Gui)!
Я уже установил ocaml на свой компьютер, но для версии Gui мне нужно установить следующие библиотеки: Gtk,...
680 просмотров
schedule
28.11.2021
Модуль анализа стоимости и опции расширений
У меня есть вопросы по опциям модуля анализа стоимости и опциям расширений.
Использую команду: frama-c-gui -val -slevel 100 -plevel 300 -absolute-valid-range 0x00000000-0xffffffff -metrics -metrics-value-cover -scope-def-interproc -main MYMAIN...
116 просмотров
schedule
08.09.2021
Установите и запустите frama-C в Windows 7
Я пытался запустить Frama-C на Windows 7, но это не сработало.
Я прочитал все советы и комментарии, которые вы написали здесь, но все еще не работают.
Может кто-нибудь объяснить процесс установки понятным и простым способом, и я буду признателен?
1964 просмотров
schedule
10.09.2021
Ошибка синтаксиса Frama-c при раскрытии макроса
Я получаю следующую синтаксическую ошибку:
../stat-time.h:58:[kernel] user error: Cannot find field st_atim
Это в gnu stat-time.h Пола Эггерта. Вот фрагмент, вызывающий ошибку:
#define STAT_TIMESPEC(st, st_xtim) ((st)->st_xtim)
long...
140 просмотров
schedule
28.11.2021
Анализ значений для верхних границ цикла
Я анализирую управляющую программу со следующей структурой:
unsigned int cnt=0;
unsigned int inc=3;
...
void main(){
int i;
int lim;
for(i=0;i<100000;i++)
{
f1();
....
lim = f2();
if(cnt < lim)
cnt += inc;
....
}
}
Моя...
51 просмотров
schedule
26.10.2021
Проверка функции, которая суммирует массив int vs массив float с помощью FramaC / WP
Я пытаюсь определить и проверить эту простую функцию, которая суммирует массив. Эта спецификация для массива целых чисел принята WP:
/*@ axiomatic Sum_Int {
logic int sum_int(int *values, integer begin, integer end)
reads...
224 просмотров
schedule
06.09.2021
Выполнение удаления мертвого кода / вырезания из исходного исходного кода в Frama-C
РЕДАКТИРОВАТЬ: в исходном вопросе не было лишних деталей
У меня есть исходный файл, который я анализирую в Frama-C, часть кода выделяется как мертвый код в нормализованном окне, а не исходный исходный код.
Могу ли я получить фрагмент исходного...
112 просмотров
schedule
02.11.2021
Frama-C сообщает о недопустимом привидении в спецификации внешней связи при загрузке файлов .C
Я новичок в Frama-C, поэтому, возможно, мне не хватает чего-то очевидного. Когда я пытаюсь загрузить файлы проекта (среди которых есть файлы .C), Frama-C сообщает об ошибке в окне консоли и прекращает обработку.
[kernel]...
54 просмотров
schedule
16.10.2021
Как на примере доказать remove_copy из ACSL
Я попытался доказать алгоритм удаления копии (первой версии) из «ACSL by Example» версии 11.1.0.
Я использовал Alt-Ergo (0.99.1), CVC3 (2.4.1), Z3 (4.3.2), CVC4 (1.4) и Why3 (0.85). Ограничение по времени в why3 было 50 секунд, а для запуска...
204 просмотров
schedule
25.02.2022
Проверка кода C на недопустимый доступ к памяти с помощью Frama-C
Мне дан этот код C (детали кода, включая возможные ошибки, не очень важны):
int read_leb128(char **ptr, char *end) {
int r = 0;
int s = 0;
char b;
do {
if ((intptr_t)*ptr >= (intptr_t)end) (exit(1));
b = *(*ptr)++;
r += (b...
180 просмотров
schedule
10.05.2022
Невозможно проверить предложение assign — Frama-C
В приведенном ниже примере frama-c не может доказать мое предложение assign в функциональном контракте, и я не уверен, почему. Буду очень признателен за любую помощь.
/*@
@ requires n>0;
@ requires \valid(a+(0..n-1));
@ ensures \forall...
85 просмотров
schedule
19.05.2022
Проверка линейного поиска с помощью Frama-C
Я снова озадачен простым упражнением по проверке, на этот раз во Frama-C (Sodium) с использованием плагина WP, поскольку я не смог заставить Джесси работать на рабочих станциях uni (в процессе установки администратором/командой .) Я читал «ACSL на...
277 просмотров
schedule
27.05.2022
Указание ссылочной прозрачности в ACSL
Я хочу найти аннотацию ACSL, которую можно применить к функции или указателю функции, чтобы указать, что она обладает свойством ссылочной прозрачности. Какой-то способ сказать, что «эта функция всегда будет возвращать одно и то же значение при...
45 просмотров
schedule
01.06.2022
Проблема нетерминирующей функции (без зависимостей)
Используя Frama-C, я пытаюсь нарезать только один исходный код следующим образом:
#include <stdio.h>
#include <stdlib.h>
#include <time.h>
typedef struct
{
int event;
int status;
int* msg;
}pbBLEEvt_t;
int...
111 просмотров
schedule
27.05.2022
Что означает сообщение о недоступной точке входа?
У меня есть файл, содержащий несколько утверждений ACSL ( file.c ):
#include <stdio.h>
#include <stdlib.h>
void foo() {
int a=0;
//@ assert(a==0);
}
void print(const char* text) {
int a=0;
//@ assert(a==0);...
161 просмотров
schedule
01.07.2022
Как скомпилировать плагин Frama-C с исходным кодом C?
Я создал подключаемый модуль Frama-C, который использует исходный код .c , и я хотел бы его скомпилировать, но при добавлении
PLUGIN_EXTRA_OPT = file
в Makefile моего плагина я получаю следующую ошибку после запуска make :
Packing...
91 просмотров
schedule
16.07.2022
Подавить сообщения [значение] в журнале анализа стоимости Frama-C.
Я хочу использовать результат анализа плагина Value во Frama-C (пакетный режим) для дальнейшей оценки переменных в функциях. Однако вывод кажется большим с большим количеством тегов [value] , мне нужна только часть из [value] ====== VALUES COMPUTED...
78 просмотров
schedule
20.08.2022
