c - VSTタイプのパニング

Question

C ISO 99 標準は、いわゆる「型パニング」をサポートしています。以下に小さな例を示します。

char *f(const char *x) {
  union {
    const char *x;
    char *y;
  } t;

  t.x = x;

  return t.y;
}

ご覧のとおり、ここではユニオン型を使用constして、同じ型でconst.

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 f_spec : ident * funspec :=
  DECLARE _f
    WITH x : val
    PRE [tptr tschar]
      PROP ()
      PARAMS (x)
      GLOBALS ()
      SEP (data_at_ Tsh (tptr tschar) x)
    POST [tptr tschar]
      PROP ()
      LOCAL ()
      SEP ().

Definition Gprog := ltac:(with_library prog [f_spec]).

Theorem test : semax_body Vprog Gprog f_f f_spec.
Proof.
  start_function.
  forward.
  forward.
  (* if you run entailer! here, you'll get False, which is unprovable *)
  entailer!.
Admitted.

この coq コードを実行すると、union から初期化されたフィールドを取得しようとしているかどうかを VST がチェックする証明不能なゴール (コメントに記載) に到達します。次のようになります。

  ENTAIL Delta,
  PROP ( )
  LOCAL (lvar _t (Tunion __136 noattr) v_t; temp _x x)
  SEP (data_at Tsh (Tunion __136 noattr) (inl x) v_t; data_at_ Tsh (tptr tschar) x)
  |-- local (liftx (tc_val (tptr tschar) Vundef))

戦術Falseによって変身します。entailer!

したがって、質問は次のとおりです。1) VST が和集合を互いに素な合計として表すのはなぜですか?

2) この機能 (型パニング) は VST でサポートされていませんか?

3) C コードの編集以外で、この問題を回避する方法はありますか?