Описание тега compcert
CompCert - это формально проверенный компилятор C для большого подмножества языка программирования C.
1
ответ
Нужно найти правильную тактику над Int.lt
У меня есть следующая лемма, но я не смог доказать это: Lemma my_comp2: forall i t:Z, t<i -> Int.ltu (Int.repr i) (Int.repr t) = false. Proof. .... Я нашел тактику равенства (ссылка), но не могу найти тактику для lt/ltu или gt/gtu: Theorem eq_…
23 авг '16 в 01:33
1
ответ
Типы отливок в coq
У меня есть определение my_def1: Require Import compcert.common.Memory. Require Import compcert.common.Values. Require Import compcert.lib.Integers. Definition my_def1 (vl: list memval) : val := match proj_bytes vl with | Some bl => Vint(Int.sign…
14 окт '16 в 00:28
2
ответа
Как доказать 10%Z <Int.max_unsigned в Coq и тип Int из Compcert
Я хочу доказать значение Z-типа меньше, чем Int.max_unsigned. Тест леммы: 10%Z
07 фев '18 в 09:56
1
ответ
Что такое EvalOp в Coq CompCert
Определение EvalOp находится в compcert.backend.SplitLongproof: Ltac EvalOp := eauto; match goal with | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp | [ |- eval_expr _ …
26 мар '18 в 21:45
1
ответ
Сравнивая два неравных значения в coq
Я доказываю эту лемму: Require Import compcert.lib.Coqlib. Require Import compcert.lib.Integers. Require Import compcert.common.Values. Lemma test: forall (val1 val2: int), ((Vint val1) <> (Vint val2)) -> (Some (Val.cmp Ceq (Vint val1) (Vin…
01 окт '16 в 22:57
1
ответ
Ошибка: невозможно привести к доступной ссылке в coq
Я пытаюсь развернуть Mem.load и получаю ошибку: Ошибка: не удается принудительно Mem.load к оцениваемой ссылке. Я написал то же самое Definition из Mem.load как load1 и разворачивается. Require Import compcert.common.AST. Require Import compcert.com…
14 окт '16 в 19:49
1
ответ
Как получить предложение для сравнения двух типов int в Coq?
У меня есть следующее определение в моем spec-файле в Coq. Мне нужно иметь предложение, сравнивающее два значения типа "int". Это два типа 't' и 'Int.repr (i. (Period1))'.(I.period1) и (i.period2) имеют тип "Z". Это мой фрагмент кода: Definition tra…
26 июл '16 в 09:27
1
ответ
Решая равенство / неравенство в цели, код Coq
Как я могу доказать, что эти два утверждения равны: Val.shru (Val.and a (Vint b)) (Vint c) = Vint? 3434 / \? 3434 <> d Val.shru (Val.and a (Vint b)) (Vint c) <> d Концепция довольно проста, но застряла в поиске правильной тактики для ее решения. Это…
14 сен '16 в 03:02
1
ответ
Проблемы с установкой компилятора CompCert C в Ubuntu
Я устанавливаю компилятор CompCert C, как указано здесь: https://compcert.org/man/manual002.html . Однако я застрял на этапе, когда я «Запускаю сценарий настройки с соответствующими параметрами: ./configure [option…] target» Вывод консоли: ~/compcer…
18 мар '21 в 15:13
0
ответов
compcert - определенное поведение доступа к объединению
В руководстве CompCert указано в §6.5.2. Если доступ к члену объекта объединения осуществляется после того, как значение было сохранено в другом члене объекта, поведение будет таким, как описано в последнем абзаце выше: операция хорошо определена, п…
30 янв '22 в 03:54
0
ответов
Использование VST с GCC
В руководстве Verified-C говорится Какое бы наблюдаемое свойство программы на языке C вы ни доказали, используя логику проверяемой программы на языке C, это свойство фактически сохранится в программе на языке ассемблера, созданной компилятором C. а …
28 сен '22 в 08:54
2
ответа
Как формально проверить компилятор (интерфейс и/или серверную часть)?
В проекте, который я собираюсь начать, я изучал формальную проверку компилятора. Я наткнулся на компилятор C CompCert , который является официально проверенным компилятором C, удостоенным награды ACM. Когда я прочитал дальше, он упомянул, что исполь…
22 мар '23 в 10:59