12 questions
0
votes
0
answers
24
views
Exposing local pointers in trace and producing load event in case of non-volatile load in CompCert
CompCert only exposes global pointers in trace. How difficult would be to change the overall development to expose the local pointers in trace? I understand preservation of the trace would be the ...
- 89
0
votes
2
answers
332
views
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, ...
- 1,872
1
vote
1
answer
143
views
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 ...
- 101
1
vote
1
answer
299
views
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: ./...
0
votes
1
answer
103
views
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 _ _ _ _ _ (...
- 103
0
votes
2
answers
124
views
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?
- 21
1
vote
1
answer
664
views
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 ...
1
vote
1
answer
945
views
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 :=
...
0
votes
1
answer
83
views
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) <> (...
- 21
0
votes
1
answer
489
views
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 ...
- 21
0
votes
1
answer
60
views
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<i -> Int.ltu (Int.repr i) (Int.repr t) = false.
Proof.
....
I found the tactic for equality (link) but can't ...
- 21
0
votes
1
answer
179
views
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 ...
- 21