Описание тега alt-ergo
Alt-Ergo - это автоматическое средство доказательства теорем с открытым исходным кодом, предназначенное для проверки программ.
1
ответ
Как выполнить следующий код SMT-LIB, используя Alt-Ergo
Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но не работает в Alt-Ergo, пожалуйста, дайте мне знать, что происходит, большое спасибо: (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true) (declare-fun…
01 июн '13 в 15:10
1
ответ
Обеспечивает доказательство, даже если код неисправен?
Далее, как подтверждаются постусловия для поведения neg_limit, когда соответствующий код C закомментирован? Как и ожидалось, одно из арифметических переполнений Safety->check не доказуемо, но похоже, что neg_limit также должен быть недоказуемым. Кон…
30 июл '13 в 17:18
1
ответ
Есть ли теория неинтерпретируемых функций (конгруэнтный анализ)?
У меня есть набор символических переменных: int a, b, c, d, e; Набор неизвестных функций, ограниченный рядом аксиом: f1(a, b) = f2(c, b) f1(d, e) = f1(e, d) f3(b, c, e) = f1(b, e) c = f1(a, b) b = d Здесь функции f1, f2, f3 неизвестны, но исправлены…
29 авг '16 в 09:13
1
ответ
Доказательство простого свойства функции над массивом
Предположим, у нас есть следующий аннотированный C-код: int a[3] = {0}; /*@ requires \valid(a+(0..2)); assigns a[0..2]; ensures \forall int j; 0 <= j < 3 ==> (a[j] == j); */ int main() { int i = 0; /*@ loop assigns i, a[0..(i-1)]; loop inva…
16 июл '15 в 09:33
2
ответа
Невозможно доказать евклидово деление в frama-c
Я хотел бы доказать эту реализацию цикла евклидова деления в Frama-C: /*@ requires a >= 0 && 0 < b; ensures \result == a / b; */ int euclid_div(const int a, const int b) { int q = 0; int r = a; /*@ loop invariant a == b*q+r && …
21 июн '18 в 11:15
1
ответ
Как запустить следующий код SMT-LIB с помощью Alt-Ergo
Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но не работает в Alt-Ergo, пожалуйста, дайте мне знать, что происходит, большое спасибо: (set-logic QF_LIA) (set-option :interactive-mode true) (set-option :incremental true) (declare-…
29 ноя '13 в 23:24
1
ответ
SMT Prover дает "неизвестно", несмотря на сильные проверенные утверждения
Предположим, у нас есть следующий аннотированный код 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 i, a[0..(i-1)]; loop inv…
20 июл '15 в 07:32
1
ответ
Плагин frama-c wp не может проверить функцию подкачки из руководства
Как сделать frama-c -wp проверить пример из руководства wp - тривиально swap функция (swap.c): /* @ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b); @ ensures B: *b == \old(*a); @ assigns *a,*b; @*/ void swap(int * a, int * b); …
04 сен '15 в 14:14
2
ответа
alt-ergo не запускается на windows через cygwin
Я пытаюсь запустить тестовый файл на frama-c с помощью средства проверки alt-ergo. Тем не менее, я получаю следующую ошибку с alt-ergo. Все остальные проверки Frama-C в порядке. Я знаю, что проблема не в тестовом файле. -----------------------------…
17 сен '14 в 17:34
1
ответ
frama-c wp константная переменная и константный массив
Я пытаюсь доказать некоторый код C с плагином WP Frama-C и у меня проблема с примером ниже: typedef unsigned char uint8_t; const uint8_t globalStringArray[] = "demo"; const int STRING_LEN = 5; /*@ requires \valid(src) && \valid(dest) &&a…
05 окт '15 в 19:24
2
ответа
Рассчитать диапазон входных данных, который приводит к удовлетворению предиката
Допустим, у нас есть следующий C-код: int my_main(int x){ if (x > 5){ x++; if (x > 8){ x++; if (x < 15){ //@(x >= 9 && x <= 14); } } } return 0; } Я хотел бы вычислить с помощью статического анализа границы переменной x при ин…
09 фев '16 в 10:04
2
ответа
Доказательства для кода, который полагается на переполнение целых чисел без знака?
Как я должен подходить к доказательству правильности кода, как показано ниже, который, чтобы избежать некоторой неэффективности, опирается на модульную арифметику? #include <stdint.h> uint32_t my_add(uint32_t a, uint32_t b) { uint32_t r = a + …
02 авг '13 в 11:25
2
ответа
Пример Frama-C acsl max из руководства не работает
Я считаю, что мне не хватает чего-то очевидного, но я много пытался, и мне не удалось найти источник проблемы. Я слежу за руководством по acsl от Frama-C. Вот вводный пример того, как проверить правильность нахождения максимального значения в массив…
07 май '20 в 18:50
1
ответ
Есть ли способ избавиться от обязательств доказательства alt-ergo, которые создает frama-c?
В настоящее время я играю с frama-c и хочу посмотреть, как frama-c кодирует различные обязательства по доказательству для передачи доказывающему (или помощнику по доказательству). В этом случае alt-ergo. Мне было интересно, есть ли какой-либо конкре…
16 ноя '19 в 00:02
1
ответ
Ошибка пользователя: доказатель 'alt-ergo' не найден в why3.conf
Я пытаюсь протестировать функцию с помощью Frama-c: /*@ ensures \result >= x && \result >= y; ensures \result == x || \result == y; */ int max( int x, int y){ return (x>y) ? x : y; } После того, как я установил все требования: OPAM,…
29 сен '20 в 18:44
1
ответ
Тайм-аут при проверке WP с помощью Alt-ergo на Frama C
Я пытался проверить правильность приведенной ниже программы с помощью Frama-c. Я новый пользователь frama-C. ПРОБЛЕМА: Введите базовую заработную плату сотрудника и рассчитайте его валовую заработную плату в соответствии со следующим Базовая зарплат…
07 окт '20 в 07:45
1
ответ
Что мне делать, когда возникает эта ошибка? Alt-Ergo: «Неизвестная ошибка»
Когда я запускаю пример WP, возникает ошибка, и я не знаю, что это такое. /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b) ; @ ensures B: *b == \old(*a) ; @ assigns *a,*b ; @*/ void swap(int *a, int *b){ int tmp = *a; *a = *b…
13 дек '20 в 14:07
1
ответ
Почему WP не может вывести «еще» близко?
Я пытаюсь написать спецификацию для функции, которая принимает 2 указателя на int и присваивает меньшее значение первому указателю, а другое — второму. Вот код и спецификация: /*@ requires \valid(a) && \valid(b); assigns *a, *b; ensures *a &…
13 мар '22 в 11:20
0
ответов
FRAMA-C/WP Цели не подтверждаются
Я пытаюсь доказать упрощенную версию примера из руководства по WP, но постоянно получаю сообщение об ошибке для одного из условий обеспечения. Вот мой код: /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b) ; @ ensures B: *b ==…
31 авг '22 в 19:12
0
ответов
Проверка того, является ли действительное число целым числом в alt-ergo
Я хочу проверить, является ли реальное значение целым числом. Кажется, не существует функции Floor или аналогичной, поэтому я пытаюсь использовать функцию real_of_int из учебника следующим образом: function real_of_int(n:int):real = n **. 1 predicat…
15 июл '23 в 14:35