2

我有一个问题，关于 VST 对 compcert 内置注释机制的支持。假设我们有一个C函数：

int f(int *p) {
  // p is not null
  __builtin_annot("_p <> nullval");
  int t = *p;
  return t;
}

及其规格：

Definition f_spec : ident * funspec :=
  DECLARE _f
    WITH p_b : block, p_ofs : ptrofs, a : Z
    PRE [(tptr tint)]
      PROP ()
      PARAMS (Vptr p_b p_ofs)
      GLOBALS ()
      SEP (data_at Tsh (tptr tint) (Vint (Int.repr a)) (Vptr p_b p_ofs))
    POST [tint]
      PROP ()
      LOCAL (temp ret_temp (Vint (Int.repr a)))
      SEP (data_at Tsh (tptr tint) (Vint (Int.repr a)) (Vptr p_b p_ofs)).

当我试图证明这一点时，我到达了我有这个声明的状态(builtin EF_annot 1 "_p <> nullval" []([]);

证明下一个，我不能从这里继续前进。

hint策略没有帮助，forward它的变体（如果，循环等）也不起作用。

所以问题是，我如何（如果可以的话）从这里继续前进？

4

0 回答 0