c - 非標準の呼び出し規約で VST forward_call が失敗する

Question

VST 2.5 と Coq 8.11.0 を使用しています

forward_call非標準の呼び出し規則で関数を実行中にエラーが発生しました。最小限のコード例:

struct t {
  int t_1;
  int t_2;
};

struct t test_aux() {
  struct t ret;
  ret.t_1 = 1;
  ret.t_2 = 2;
  return ret;
}

void test_f() {
  test_aux();
}

VST 仕様:

Require Import VST.floyd.proofauto. 
Require Import example.

Definition Vprog : varspecs. mk_varspecs prog. Defined. Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Open Scope Z.

Definition aux_spec : ident * funspec :=   DECLARE _test_aux
    WITH res : val
    PRE [tptr (Tstruct _t noattr)]
      PROP ()
      PARAMS (res)
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) res)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP (data_at Tsh (Tstruct _t noattr) 
                   (Vint (Int.repr 1), Vint (Int.repr 2)) res).

Definition test_spec : ident * funspec :=   DECLARE _test_f
    WITH temp : val
    PRE []
      PROP ()
      PARAMS ()
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) temp)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP ().

Definition Gprog := ltac:(with_library prog [aux_spec; test_spec]).

Theorem test : semax_body Vprog Gprog f_test_f test_spec. Proof.   start_function.   Fail forward_call (nullval). Admitted.

エラー：

Unable to unify  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid cc_default" with  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid
    {|
    cc_vararg := false;
    cc_unproto := false;
    cc_structret := true |}".

これがバグなのか意図した動作なのかわかりませんので、いくつか質問があります。

1) これはバグですか?

2) そうでない場合、そのようなケースを証明するための回避策はありますか?

アップデート：

構造体コピーの制限を回避する次の回避策を使用した後、この問題に遭遇しましたstruct_normalize : statement -> statement。構造体の割り当てをフィールドごとの割り当てに置き換える関数を Coq で定義します。したがって、呼び出している関数に構造体のコピーがないという前提で作業しています。つまり、test_aux上記の例から を確認できます。質問は次のとおりです。

3. forward_call失敗するcc_structret := trueのはtest_auxASTだけですか?

4. 関数を正規化し、関数の本体から構造のコピーを削除した場合、それstructretに応じて値を変更して証明を進めることは安全ですか?