Вопросы по теме 'frama-c'
Экзистенциальное количественное утверждение терпит неудачу
Я пытаюсь доказать количественные утверждения для массивов и столкнулся с некоторыми проблемами. Рассмотрим следующую небольшую программу:
int a[4] = {1,2,3,4};
/*@ requires p == a;
assigns \nothing;
*/
void test(int *p)
{
p++;
//@...
142 просмотров
schedule
15.01.2024
Frama-C/WP/ACSL Правильное использование \valid на структурах
У меня есть некоторые сомнения относительно того, как правильно использовать аннотацию \valid для структур.
struct someStruct{
int size1;
int size2;
char *str1;
char *str2;
}
Правильный предикат для проверки безопасности...
790 просмотров
schedule
18.04.2022
Можем ли мы запустить анализ значений в Frama-C для файла C, у которого нет основной функции?
При запуске Frama-C на файле C без основной функции я получил ошибки. Есть ли возможность запустить анализ значений Frama-C для таких файлов C?
211 просмотров
schedule
10.03.2023
Компиляция Frama-c под mac os x 10.9
Я пытаюсь установить последнюю версию frama-c (Fluorine 3) в mac os x 10.9. Используя brew, я смог заполнить предварительные условия frama-c (Gtk, GtkSourceView, GnomeCanvas и Lablgtk2)
Результат из файла конфигурации следующий:
$ ./configure...
705 просмотров
schedule
28.06.2023
/*неопределенная последовательность*/ в нарезанном коде из Frama-C
Я пытаюсь нарезать код с помощью Frama-C.
Исходный код
static uint8_T ALARM_checkOverInfusionFlowRate(void)
{
uint8_T ov;
ov = 0U;
if (ALARM_Functional_B.In_Therapy) {
if (ALARM_Functional_B.Flow_Rate > ALARM_Functional_B.Flow_Rate_High)...
69 просмотров
schedule
10.07.2022
Frama-C: доступ к данным модулей cil/src/ext, а также несколько других вопросов
прежде всего, я объясню, что я хотел бы сделать здесь: учитывая большую программу C, я хотел бы вывести список производителей/потребителей для данных и список вызывающих/вызываемых функций функции, где это данные есть.
для этого я думаю об...
68 просмотров
schedule
21.12.2022
Доказательство SMT дает «неизвестно», несмотря на сильно доказанные утверждения
Предположим, у нас есть следующий аннотированный код C:
#define L 3
int a[L] = {0};
/*@ requires \valid(a+(0..(L - 1)));
ensures \forall int j; 0 <= j < L ==> (a[j] == j); */
int main() {
int i = 0;
/*@ loop assigns...
177 просмотров
schedule
18.02.2024
Предотвратить изменение входного кода плагином для нарезки Frama-C.
Учитывая файл C, я хочу вычислить обратный срез по некоторым критериям и сравнить срез с исходным кодом. Поскольку я не хочу создавать программу для нарезки с нуля, я уже пытался привыкнуть к Frama-C, который, кажется, помогает с этой задачей....
84 просмотров
schedule
07.08.2023
Встроенные функции Frama-C
Я только что установил его из диспетчера пакетов Opam и пытаюсь научиться использовать анализ значений из учебника на веб-сайте frama-c. В настоящее время я не могу использовать встроенный файл.c, его нет в моей общей папке, и я не могу понять, как...
100 просмотров
schedule
16.07.2022
Frama-C: получение выходных данных функции при использовании указателей
Мне нужно получить список всех выходов функции. Когда я использую From -плагин в следующем коде
void add(int *sum, int a, int b)
{
*sum = a + b;
}
int main()
{
int result;
add(&result, 1, 2);
}
он говорит мне, что result...
179 просмотров
schedule
23.05.2024
Синтаксическая ошибка в Frama-C из-за пользовательского machdep
Я использую компилятор C MPLAB XC16 для своего приложения. Если я использую machdep x86_16, Frama-C работает нормально. Например, я могу запустить Frama-C таким образом:
$ frama-c-gui machdep x86_16 -cpp-command 'C:\\"Program Files...
160 просмотров
schedule
17.10.2023
Ошибки при использовании плагина Frama-Clang
Учитывая, что плагин https://frama-c.com/frama-clang.html считается на "ранней стадии" разработки, возможно мне пока не везет. Но интересно, сталкивался ли кто-нибудь с такой проблемой:
navarre@navarre-t400:~/code/c$ frama-c max.cpp
[kernel]...
342 просмотров
schedule
10.12.2022
Как доказать почему3 сгенерированный скрипт в coq?
Я использую frama-C WP и хочу отладить свои аннотации ACSL (чтобы понять, почему доказывающие говорят, что я «не знаю»). У меня есть результат зеленого или оранжевого цвета. Открываю why3 IDE и вижу сгенерированные скрипты. Затем я выбираю теорию /...
282 просмотров
schedule
12.06.2022
Как избежать обнаружения неинициализированных переменных при использовании анализа влияния Frama-C
Я обнаружил, что если в программе есть неинициализированное левое значение (например, переменная X), Frama-C утверждает, что X было инициализировано, но тогда утверждение получает недействительный окончательный статус. Похоже, что Frama-C...
79 просмотров
schedule
30.06.2022
не могу анализировать код openmp с помощью frama-c
Я новичок в frama-c. Я попытался запустить плагин анализа значений для следующего кода c с директивами openmp:
static void kernel_2mm(int ni, int nj, int nk, int nl, float alpha,
float beta, float *tmp, float *A, float *B, float *C, float *D)...
193 просмотров
schedule
22.06.2022
Frama-c: сохранить результаты анализа плагина в c-файле
Я новичок в frama-c. Поэтому заранее извиняюсь за свой вопрос.
Я хотел бы сделать плагин, который будет изменять исходный код, клонировать некоторые функции, вставлять некоторые вызовы функций, и я хотел бы, чтобы мой плагин генерировал второй...
89 просмотров
schedule
15.11.2023
Как я могу просмотреть свои отчеты с помощью vstmt_aux во Frama-C
Я работаю над плагином для скалярной замены. У меня возникли некоторые трудности с заявлением посетителя. Я хотел бы проанализировать инструкции, которые находятся в циклах, для каждой инструкции мне нужно знать, включена ли она в цикл, включен ли...
44 просмотров
schedule
12.10.2023
Обрабатываются ли бесконечные циклы в Frama-C?
Я пытаюсь доказать, что значение переменной всегда увеличивается. Я написал следующий код:
void Commit() {
int count = 1;
//@ ghost int old_count = 0;
while (1) {
//@ ghost old_count = count;
count++;
//@...
124 просмотров
schedule
12.12.2022
Выполнение обязательств по подтверждению для memcpy? [Фрама-С]
Мы использовали Frama-C для «экспериментального» статического анализа в коммерческом проекте (интегрированном в наш CI с несколько выборочными блокирующими проверками на небольшом участке общей кодовой базы).
Одна из возникающих проблем связана с...
225 просмотров
schedule
30.06.2023
Как я могу доказать эту функцию C is_power_of_2, используя Frama-C?
В предыдущем вопросе Я просил помощи в написании predicate , чтобы определить, является ли число степенью двойки. Это было прелюдией к попытке доказать следующую функцию C:
static inline bool
is_power_of_2 (unsigned long v)
{
return v...
80 просмотров
schedule
14.12.2023
