verifiable-c - 検証可能な c を使用してグローバル変数の分離仕様を記述する方法

Question

以下は、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).