CODEWITHSUNDEEP
ccoqformal-verificationverifiable-c
Yarick
Yarick

Reputation: 346

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 f() {
struct foo q;
return q; }

On starting proof got an error:

Error: Tactic failure: The expression (_q)%expr contains internal structure-copying, a feature of C not currently supported in Verifiable C (level 97).

This is due to the check_normalized in floyd/forward.v :

Fixpoint check_norm_expr (e: expr) : diagnose_expr :=
match e with
| Evar _ ty => diagnose_this_expr (access_mode ty) e
...

So, the questions are:

1) What suggested workarounds exists?

2) What is the reason for this limitation?

3) Where can I get a list of unsupported features?

Upvotes: 2

Views: 174

Answers (1)

Andrew Appel
Andrew Appel

Reputation: 548

1) The workaround is to change your C program to copy field by field.

2) The reason is the absurdly complicated and target-ISA-dependent implementation/semantics of C's structure-copying, especially in parameter passing and function-return.

3) The first 10 lines of Chapter 4 ("Verifiable C and clightgen") of the reference manual has a short list of unsupported features, but unfortunately struct-by-copy is not on that list. That's a bug.

Upvotes: 5

Related Questions