Coq VST Внутреннее копирование структуры

Question

проблема с библиотекой VST (Verified Software Toolchain) 2.5v для Coq 8.10.1:

Произошла ошибка с последней рабочей фиксацией VST, а именно: " Внутреннее копирование структуры не поддерживается ». Минимальный пример:

struct foo {unsigned int a;};
struct foo f() {
struct foo q;
return q; }

При запуске доказательства получена ошибка:

Ошибка: Tacti c Ошибка: выражение (_q)% expr содержит внутреннее копирование структуры, a функция C в настоящее время не поддерживается в Verifiable C (уровень 97).

Это связано с check_normalized в floyd / forward.v :

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

Итак, вопросы:

1) Какие предлагаемые обходные пути существуют?

2) В чем причина этого ограничения?

3) Где я могу получить список неподдерживаемых функций?

Answer 1

1) Обходной путь состоит в том, чтобы изменить вашу C программу, чтобы копировать поле за полем.

2) Причина - нелепо сложная и зависимая от ISA реализация / семантика C. копирование структуры, особенно при передаче параметров и возврате функций.

3) Первые 10 строк главы 4 («Проверяемые C и clightgen») справочного руководства содержат краткий список неподдерживаемых функций, но, к сожалению, структурно-копируются нет в этом списке. Это ошибка.