Verifiable C is a program logic for the C programming language, used in the Verified Software Toolchain system.
Questions tagged [verifiable-c]
37 questions
3
votes
2 answers
Verified software toolchain: if-then-else proof
I'm learning using the Verified Software Toolchain (VST). I get stuck at proving a simple "if-then-else" block.
Here is the .c file:
int iftest(int a){
int r=0;
if(a==2){
r=0;
else{
r=0;
}
return r;
}
I write a…
lgbo
- 221
- 3
- 14
2
votes
0 answers
VST type punning
C ISO 99 standard supports so-called "type punning". Here is a small example:
char *f(const char *x) {
union {
const char *x;
char *y;
} t;
t.x = x;
return t.y;
}
As you can see, here we're using union type to get rid of const…
Yarick
- 326
- 3
- 14
2
votes
0 answers
VST built-in annotation support
I got a question, about VST support for compcert built-in annotation mechanism.
Suppose we have a C function:
int f(int *p) {
// p is not null
__builtin_annot("_p <> nullval");
int t = *p;
return t;
}
And specification for it:
Definition…
Yarick
- 326
- 3
- 14
2
votes
1 answer
VST forward_call fail on non-standard calling convention
I'm using VST 2.5 and Coq 8.11.0
Got an error while doing forward_call on function with non-standard calling convention.
Minimal code example:
struct t {
int t_1;
int t_2;
};
struct t test_aux() {
struct t ret;
ret.t_1 = 1;
ret.t_2 = 2;
…
Yarick
- 326
- 3
- 14
2
votes
0 answers
Proving that an int is equal to an array of characters
I'm using VST v1.7.
Has anyone ever proved that an int is equal as an array of characters? Something along those lines:
Definition int2uchars (i : int) : list Z :=
[
Int.unsigned (Int.and (Int.shru i (Int.repr 24)) (Int.repr 255));
…
Corto Maltese
- 21
- 2
2
votes
1 answer
How to reason about array access in VST?
I have a trouble proving a trivial array access function (file arr.c):
int get(int* arr, int key)
{
return arr[key];
}
which is translated by clightgen arr.c to (file arr.v):
...
Definition f_get := {|
fn_return := tint;
fn_callconv :=…
Necto
- 2,594
- 1
- 20
- 45
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
2 answers
What subset of C is supported by Verifiable-C?
I'm trying to figure out what subset of C is supported by Verifiable C from Verified Software Toolchain. "Program Logics For Certified Compilers" (p. 143) states that it is subset of Clight. But CompCert compiler transforms program from CompCert C…
Artem Kokorin
- 27
- 5
1
vote
0 answers
Unable to read from offset 0 of a pointer in VST
For various reasons I am verifying a program that attempts to read from a pointer with an offset of 0:
int x = (*(z + 0)).ssl_int;
When verifying this in VST, the context has as an assumption that there is a value on the heap at this…
Kiran Gopinathan
- 73
- 7
1
vote
1 answer
How do I write a proof for a switch statement with VST/ coq?
I had a question regarding the use of VST and switch statements.
I am having trouble writing a proof that steps through the switch statement when there is a matching case for the switch variable. For example:
I CAN write a proof for something like…
R2D2
- 11
- 1
1
vote
1 answer
Figuring out proper loop invariant when appending to a linked list with verifiable C
I'm working on the beta 5th software foundations module which covers verifiable C. I'm on the final portion, which has to do with operations on a hash map (which requires operations on a linked…
A Question Asker
- 3,339
- 7
- 31
- 39
1
vote
1 answer
Coq VST Internal structure copying
run into a problem with VST(Verified Software Toolchain) 2.5v library for Coq 8.10.1:
Got an error with the latest working commit of VST namely "Internal structure copying is not supported".
Minimal example:
struct foo {unsigned int a;};
struct foo…
Yarick
- 326
- 3
- 14
1
vote
1 answer
How to describe a double link using separation logic in the VST tool
As an example in the VST project, the reverse.c file has a linked list like this:
struct list {unsigned head; struct list *tail;};
unsigned sumlist (struct list *p) {
unsigned s = 0;
struct list *t = p;
unsigned h;
while (t) {
h =…
haiyong
- 21
- 2
1
vote
1 answer
Proving correctness of Xor-Swapping
Update: Now I have the following program 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;
}
My specification…
schoppenhauer
- 411
- 3
- 11
1
vote
2 answers
How to use more than 8 variables in a function specification?
WITH construction is defined only for up to 8 variables. How can I use more than 8?
Example:
Definition find_key_spec :=
DECLARE _find_key
WITH sh : share, m : ArrMapZ, start : Z, key : Z, i : nat,
vbb : val, vkeys : val, vstart :…
Necto
- 2,594
- 1
- 20
- 45