2

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 代码，您将到达无法证明的目标（在评论中提到），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 代码之外，是否有解决此问题的方法？

4

0 回答 0