Описание тега acsl

Вопросы с тегом
ACSL (ANSI/ISO C Specification Language) is a specification language for C programs, used by tools such as Frama-C.
1 ответ

ACSL - не может доказать функцию

Я пытаюсь доказать эту функцию, но тщетно. Я тоже использую другую функцию, но я это доказал. Кто-нибудь может мне помочь? I'm using Frama-C Sodium version with Alt-ergo 3 as prover. Given a not-empty string x. An integer number p such that 0 < p…
25 янв '16 в 15:32
3 ответа

sh.exe препятствует работе команды windows cmd move

Я запускаю старое приложение под названием ACSLX, Он пытается вызвать команду перемещения DOS, но потому что sh.exe на моем пути, я получаю ошибку. sh.exe это часть Git а также RTools, оба из которых я установил. Как видите, он просто пытается перем…
21 авг '18 в 03:15
1 ответ

Указание ссылочной прозрачности в ACSL

Я хочу найти некоторую аннотацию ACSL, которую можно применить к функции или указателю на функцию, чтобы указать, что она обладает свойством ссылочной прозрачности. Некоторый способ сказать, что "эта функция всегда будет возвращать одно и то же знач…
12 ноя '18 в 07:51
1 ответ

ACSL "назначает" аннотацию для внутренних структур и полей кода C

Предположим, у нас есть такая структура данных: #typedef struct { int C_Field; }C; #typedef struct { C B_Array[MAX_SIZE]; }B; #typedef struct { B A_Array[MAX_SIZE]; }A; Кажется, что Frama-C не назначает местоположение для поля структуры типа C в сле…
27 апр '17 в 04:36
1 ответ

Спецификация ACSL функции, которая добавляет строку в динамический массив символов

Я работаю над написанием спецификации ACSL для функции, которая добавляет данную строку в конец динамического массива символов. Вот что у меня так далеко: #include <stddef.h> #include <stdint.h> #include <stdlib.h> #include <str…
12 ноя '15 в 22:50
1 ответ

Предупреждение Frama-C: отсутствует пункт assigns (вместо него назначается "все")

Я тестирую эту маленькую программу с frama-c и продолжаю получать ту же ошибку. Я не уверен, что это значит. Я особенно запутался в том, что назначает все, что значит. Вот этот код с аннотациями ACSL: // assuming n is nonnegative and even, f returns…
12 апр '18 в 18:30
2 ответа

Как заставить область памяти быть действительной в ACSL?

Я определяю доступ к устройству следующим образом volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS; Я смоделировал доступ с помощью @ volatile dev->somereg reads somereg_read writes somereg_write; Теперь проблема в том,…
20 июл '17 в 18:33
1 ответ

Как мне отладить ACSL в frama-c?

Я пытаюсь выучить ACSL, но пытаюсь написать полную спецификацию. Мой код #include <stdint.h> #include <stddef.h> #define NUM_ELEMS (8) /*@ requires expected != test; @ requires \let n = NUM_ELEMS; @ \valid_read(expected + (0.. n-1)) &amp…
19 июл '17 в 23:20
1 ответ

Может ли ACSL обозначать, что назначение должно быть скрыто?

Эта функция проверяет функцию, которая возвращает непрерывно растущее значение, пока не произойдет переполнение. Это как millis() функция в Arduino. Чтобы доказать реализацию, мне нужно увеличить (таким образом, назначить) статические переменные, чт…
19 ноя '18 в 10:13
0 ответов

Должны ли мы писать "assert" после каждого вызова функции, когда вызывается последовательность функций?

Позвольте мне начать мой вопрос с этого примера: void A (void) { B(); C(); D(); E(); ... // function calls go on. return; } Теперь давайте добавим аннотации ACSL к коду: /*@ ensures PostConditionOfB(); ensures PostConditionOfC(); ensures PostConditi…
08 май '17 в 02:16
1 ответ

Ошибка компиляции E-ACSL FRAMA-C

Я новичок в фреймворке Frama-C и пытаюсь провести некоторое контрактное тестирование с помощью C-программ. Я намерен использовать плагин E-ACSL для этого, и я попробовал тестовую программу, чтобы увидеть, как она работает, но я получаю некоторые оши…
03 апр '18 в 17:31
1 ответ

Frama-c: вызовы функций и статические переменные

В настоящее время я открываю для себя возможности frama-c, особенно инструменты анализа WP & Value. Моя конечная цель - использовать frama-c в больших кодах, включающих несколько уровней: много вызовов функций использование сложных структур данных с…
17 май '18 в 07:56
1 ответ

Спецификация ACSL для возможно бесконечной функции C

Я пытаюсь уточнить поведение внешних функций, точнее, их прекращение. В документации ACSL сказано, что \terminates p; свойство указывает, что если предикат p удерживается, то функция гарантированно завершается, но ничего не указывает, когда p не дер…
21 фев '13 в 09:42
2 ответа

Сортировка предложения с использованием массивов и строк

Извините, ребята, предупреждаю, что я отстой в кодировании, но у меня большой проект и мне нужна помощь! Вход: полное предложение. Вывод: отсортированный порядок (ASCii Chart Order) предложения (игнорировать регистр.) Выведите гистограмму для следую…
22 апр '16 в 14:10
2 ответа

ACSL Битовые строки Flickking

Мне нужна помощь с проблемой ACSL. Конкурс проводился в 2014-2015 годах. Это просто практика, и я хочу посмотреть, правильно ли я решил проблему. Строка Бит-Строка: Решите для х (5 бит) в следующем уравнении. Сколько существует уникальных решений? (…
02 фев '16 в 18:42
1 ответ

Как могут быть связаны файлы C при использовании плагина E-ACSL?

Я пытаюсь создать аннотированный файл с помощью плагина Frama-C E-ACSL. Я создал следующие файлы: Insert.c : содержит все структуры для создания связанного списка. AxiomTest.c : включает основную функцию, в которой указываются утверждения, которые о…
26 апр '18 в 13:15
0 ответов

Ошибка вызова логической функции E-ACSL - несвязанная функция

Я хочу определить простые контракты функций (определенные в руководстве ACSL, раздел 2.3.2) из ​​программы insert.c, указанной ниже. Эти контракты будут определены в соответствии с функциями наблюдателя (например, если isempty(s)==trueпосле вставки …
04 май '18 в 16:37
1 ответ

Нужна помощь по прошлой программе ACSL с 2013 года

Мой учитель заставляет нас делать старую программу ACSL для практики, и он сказал, что мы можем использовать любые ресурсы, которые захотим. Программа с 2013 года. Ссылка здесь: https://s3.amazonaws.com/iedu-attachments-question/5a989d787772b7fd88c0…
06 фев '16 в 23:42
1 ответ

Неограниченная функция в плагине EACSL Frama-C

Я пытаюсь сгенерировать контракты в C с помощью плагина E-ACSL из FRAMA-C для следующей программы: struct lnode { int value; struct lnode *next; }; struct set { int capacity; int size; struct lnode *elems; }; struct set* new(int capacity) { struct s…
30 апр '18 в 11:21
1 ответ

ACSL-подтверждение функции, которая проверяет, отсортирован ли массив в порядке возрастания или убывания

Я пытаюсь доказать правильность функции, которая проверяет, отсортирован ли массив в порядке возрастания / убывания или нет. Поведение состоит в том, чтобы вернуть -1, если отсортировано в порядке убывания, 1, если отсортировано в порядке возрастани…
06 дек '19 в 13:23