Stack Overflow
Stack Overflow

Questions tagged [compcert]

CompCert is a formally verified C compiler for a large subset of the C programming language.

The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, Risc-V, and x86 processors.

The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code.

Resources

11 questions
1
vote
1 answer

Using VST with GCC

The Verifiable-C manual says Whatever observable property about a C program you prove using the Verifiable C program logic, that property will actually hold on the assembly-language program that comes out of the C compiler. and then The program…
rsaill
  • 91
  • 1
  • 7
1
vote
1 answer

Trouble Installing CompCert C compiler on Ubuntu

I'm installing CompCert C compiler as instructed here: https://compcert.org/man/manual002.html. However I'm stuck at the stage where I "Run the configure script with appropriate options: ./configure [option …] target " The console output…
Keyboard_Crasher
  • 55
  • 8
1
vote
1 answer

Error: Cannot coerce to an evaluable reference in coq

I'm trying to unfold Mem.load and I get the error: Error: Cannot coerce Mem.load to an evaluable reference. I wrote the exact same Definition of Mem.load as load1 and is unfoldable. Require Import compcert.common.AST. Require Import…
Mina mohamadi
  • 33
  • 2
1
vote
1 answer

Casting types in coq

I have the definition 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 =>…
Mina mohamadi
  • 33
  • 2
0
votes
2 answers

How to formally verify a compiler (frontend and/or backend)?

For a project I am about to begin, I was exploring formal verification of a compiler. I came across the CompCert C Compiler which is an ACM awarded, formally verified C compiler. When I read further, it mentioned that it has used Coq Proof Assistant…
anurag
  • 1,715
  • 1
  • 8
  • 28
0
votes
1 answer

What is the EvalOp in Coq CompCert

The definition of EvalOp is in compcert.backend.SplitLongproof: Ltac EvalOp := eauto; match goal with | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp | [ |-…
Jian Wang
  • 103
  • 5
0
votes
2 answers

how ot proof 10%Z < Int.max_unsigned in Coq and the Int type from Compcert

I want to proof a Z type value less than Int.max_unsigned. Lemma test: 10%Z < Int.max_unsigned. Proof. ?? How to prove the above test lemma?
haiyong
  • 21
  • 2
0
votes
1 answer

comparing two unequal values in coq

I'm proving this lemma: 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) (Vint…
saeed M
  • 21
  • 7
0
votes
1 answer

Solving equality / inequality in goal, coq code

How can I prove that these two statements are equal: Val.shru (Val.and a (Vint b)) (Vint c) = Vint ?3434 /\ ?3434 <> d Val.shru (Val.and a (Vint b)) (Vint c) <> d The concept is pretty simple but stuck in finding the right tactic to solve it. This…
saeed M
  • 21
  • 7
0
votes
1 answer

Need finding the right tactic over Int.lt

I have the following Lemma but couldn't prove it: Lemma my_comp2: forall i t:Z, t Int.ltu (Int.repr i) (Int.repr t) = false. Proof. .... I found the tactic for equality (link) but can't find the one for lt/ltu or gt/gtu: Theorem eq_false:…
saeed M
  • 21
  • 7
0
votes
1 answer

How to have a proposition of comparing two 'int' types in Coq?

I have the following Definition in my spec file in Coq. I need to have a proposition comparing two "int" type values. These two are 't' and 'Int.repr (i.(period1))'.(i.period1) and (i.period2) have type 'Z'. This is my code snippet: Definition…
saeed M
  • 21
  • 7