Описание тега verifiable-c
Verifiable C - это программная логика для языка программирования C, используемого в системе Verified Software Toolchain.
1
ответ
Как использовать retval-postcondition для переменной, содержащей возвращаемое значение?
Моя простая программа vars.c: int pure0 () { return 0; } int get0(int* arr) { int z = pure0(); return z; } Я начал доказательство (файл verif_vars.c): Require Import floyd.proofauto. Require Import vars. Local Open Scope logic. Local Open Scope Z. D…
18 янв '15 в 18:48
3
ответа
Как обрабатывать цели "Forall (closed_wrt_vars (eq _z')) P " в VST?
На этот раз я проверяю функцию вызова другого. vars.c: int pure0 () { return 0; } int get0(int* arr) { int z = pure0(); return 0; } Мое доказательство начала - verif_vars.v: Require Import floyd.proofauto. Require Import vars. Local Open Scope logic…
18 янв '15 в 13:00
1
ответ
Тактическая ошибка: используйте forward_call W. подпись метода
Я пытаюсь проверить мою программу с VST. У меня странное сообщение об ошибке: Coq < Check ( (sh, n, guess-1, vn, Vint (Int.sub (Int.repr guess) (Int.repr 1)))). > (sh, n, guess - 1, vn, Vint (Int.sub (Int.repr guess) (Int.repr 1))) > : shar…
13 дек '14 в 19:29
1
ответ
Странная цель VST при проверке хранилища массивов
Сейчас я пытаюсь доказать тривиальную процедуру доступа к массиву (файл arr.c): void set(int* arr, int key, int val) { arr[key] = val; } Файл arr.c переводится на arr.v: ... Definition f_set := {| fn_return := tvoid; fn_callconv := cc_default; fn_pa…
13 янв '15 в 13:35
2
ответа
Поиск способов указать функциональную спецификацию Verifiable-c
Я только начинаю работу с поддающимся проверке c и пытаюсь сгенерировать функциональные спецификации для написанного мною кода. Мой основной пример, с которым я работаю, это (код C) просто int xor(int v1, int v2) { return v1 ^ v2; } и я испытываю за…
18 сен '16 в 23:00
2
ответа
Спецификации с адресуемыми локальными переменными
Я пытаюсь понять, как VST обрабатывает (адресуемые) локальные переменные, поэтому я написал эту функцию: int main() { int x = 5, y = 7; int *a = &x; int *b = &y; *a = 8; *b = 9; return x; } Затем я попытался проверить это с помощью следующей…
24 сен '18 в 15:45
0
ответов
Доказательство того, что int равен массиву символов
Я использую VST v1.7. Кто-нибудь когда-нибудь доказывал, что int равен массиву символов? Что-то в этом роде: Definition int2uchars (i : int) : list Z := [ Int.unsigned (Int.and (Int.shru i (Int.repr 24)) (Int.repr 255)); Int.unsigned (Int.and (Int.s…
25 янв '17 в 20:34
0
ответов
Изменение массива на месте с последующим использованием Verifiable C
VST 1.7, Coq 8.5pl2. У меня есть глобальный массив processingQVars, для которого я вызвал функцию для изменения на месте, изменив условие SEP с data_at Ews (tarray tint 8) (map Vint [Int.repr 15; Int.repr 5463; Int.repr 12; Int.repr 75; Int.repr 231…
03 дек '16 в 20:11
1
ответ
semax_func_cons - нет применимой тактики
Я пытаюсь собрать доказательства для моих двух функций в доказательство для всей программы: ... Definition Vprog : varspecs := nil. Definition Gprog : funspecs := get_spec :: set_spec :: nil. Lemma body_get: semax_body Vprog Gprog f_get get_spec. Pr…
14 янв '15 в 22:22
2
ответа
Проверенный программный инструментарий: доказательство "если потом"
Я учусь с помощью проверенного программного пакета (VST). Я застрял в доказательстве простого блока "если-то-еще". Вот файл.c: int iftest(int a){ int r=0; if(a==2){ r=0; else{ r=0; } return r; } Я пишу спецификацию о iftest() следующим образом: Defi…
20 авг '13 в 07:30
1
ответ
Как рассуждать о доступе к массиву в VST?
У меня проблема с проверкой тривиальной функции доступа к массиву (файл arr.c): int get(int* arr, int key) { return arr[key]; } который переводится clightgen arr.c к (файл arr.v): ... Definition f_get := {| fn_return := tint; fn_callconv := cc_defau…
11 янв '15 в 17:25
3
ответа
Ошибка компилятора Coq: невозможно объединить "4" с "8". с VST сделать
У меня есть два вопроса: Во-первых, если я напишу программу на C со встроенной сборкой, могу ли я проверить всю программу на C в VST? Или это только программы на чистом C, которые можно проверить? Во-вторых, я попытался установить последние версии V…
12 янв '15 в 16:01
1
ответ
forward_call с локальными переменными
VST версия 1.7. У меня проблема, когда coq не распознает объявленные локально переменные, когда я пытаюсь использовать их в вызове функции. У меня есть код: void deSignArray(int bits[], int invKey, int size) { int i = 0; while (i < size) { int bi…
12 ноя '16 в 16:39
2
ответа
Как использовать более 8 переменных в спецификации функции?
WITH Конструкция определяется только для 8 переменных. Как я могу использовать более 8? Пример: Definition find_key_spec := DECLARE _find_key WITH sh : share, m : ArrMapZ, start : Z, key : Z, i : nat, vbb : val, vkeys : val, vstart : val, vkey : val…
24 янв '15 в 11:54
1
ответ
Диапазон массива в предварительном условии
В настоящее время я пытаюсь узнать, как использовать VST. Я использую VST 1.5. У меня есть эта маленькая программа C (backref.c): char* rbr (char* out, int length, int dist) { while (length-- > 0) { out[0] = out[-dist]; out++; } return out; } Мой…
04 авг '15 в 15:46
1
ответ
Как описать двойную связь, используя логику разделения в инструменте VST
Например, в проекте VST файл reverse.c имеет связанный список, например: struct list {unsigned head; struct list *tail;}; unsigned sumlist (struct list *p) { unsigned s = 0; struct list *t = p; unsigned h; while (t) { h = t->head; t = t->tail;…
01 мар '18 в 03:55
1
ответ
Как написать спецификацию разделения глобальной переменной, используя проверяемый c
Ниже приведен пример кода на языке C. unsigned int COUNTER; unsigned int get_counter(void) { COUNTER ++; return COUNTER; } Я написал основную спецификацию с использованием поддающегося проверке c (vst), но в конце проверки я сталкиваюсь с ошибкой "t…
05 фев '18 в 09:30
1
ответ
Доказательство правильности Xor-Swapping
Обновление: теперь у меня есть следующая программа swap.c: void swap (int* a, int* b) { int ta = *a; int tb = *b; ta = ta ^ tb; tb = ta ^ tb; ta = ta ^ tb; *a = ta; *b = tb; } Моя спецификация Require Import floyd.proofauto. Require Import floyd.ent…
09 авг '15 в 18:21
1
ответ
Книга PLCC. страница 23. Является ли это опечаткой, и следует ли заменить сигму на простую сигму?
В книге "Логика программирования для сертифицированных компиляторов" на странице 23 в выражении: (v ≠ 0 ∧ ∃σ' ∃h∃t. σ = h · σ' ∧ v.head->h ∗ v.next->t ∗ listrep σ (t, 0)) Мне кажется, что, поскольку σ представляет весь список v, а σ'представля…
12 янв '15 в 11:12
1
ответ
Почему циклы while, основанные на проверке типов (w/ tc_expr), являются условным выражением?
Кажется, что tc_expr ограничен знанием контекста типизации и ничем иным, поэтому невозможно безопасно "проверить тип" выражения, которое требует знания состояния кучи, например разыменование указателя в качестве условия цикла while. Почему это так и…
12 окт '18 в 18:02