1

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?

Nika
  • 7
  • 3
Yarick
  • 326
  • 3
  • 14

1 Answers1

4

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.

Andrew Appel
  • 453
  • 3
  • 4
  • Thanks for the response. What if we have a substantial amount of C code changing which could be impractical. This is a very basic feature of C used in much of the existing code. If there is any other workaround? Maybe structure copying could be admitted or and then proven with some limitations (e.g. only structures with primitive types)? – krokodil Mar 31 '20 at 17:15