0

以下是 C 中的示例代码。

unsigned int  COUNTER;
unsigned int  get_counter(void) {
    COUNTER ++;
    return COUNTER;
}

我使用可验证的 c (vst) 编写了它的功能规范，但在验证结束时我遇到了错误“typecheck_error (deref_byvalue tint)”。任何人都可以告诉我如何编写上述 c 函数的正确 founc 规范吗？关键是如何编写全局变量的 SEP()。

（这里是错误的，请纠正我）

Definition get_counter_spec :=
 DECLARE _get_counter
  WITH v : Z, counter:val
  PRE []
        PROP  () 
        LOCAL (gvar _COUNTER counter)
        SEP   (data_at Ews tint (Vint (Int.repr v)) counter)
  POST [ tint ]
        PROP () 
        LOCAL(temp ret_temp (Vint (Int.repr (v+1))))
        SEP   (data_at Ews tint (Vint (Int.repr (v+1))) counter).
4

1 回答 1

1

您的错误：在 C 程序中，COUNTER 被声明为“unsigned int”，但在您的 get_counter_spec 中，您使用“tint”而不是“tuint”。有了这个改变，证明马上就通过了：启动函数；做4前进。

我们的错误：您收到的错误消息（在 VST 2.0 中）非常无用！我将添加一个问题报告来改进这种情况下的错误报告。

于 2018-02-05T13:58:23.140 回答