verifiable-c - 機能仕様 Verifiable-c を指定する方法を見つける

Question

私は検証可能な c の作業を始めたばかりで、自分が書いた C コードの機能仕様の生成に苦労しています。私が扱っている私の基本的な例は、単純に（Cコード）です

int xor(int v1, int v2) {
  return v1 ^ v2;
}

定義 xor_spec セクションをまとめるのに苦労しています。

ありがとう。

Answer 1

Cコードを投稿できますか？最後のコメントから、ローカル変数「tmp」、「bit」、「key」があるように見えますが、C プログラムには表示されません。

Answer 2

Definition xor_spec :=
 DECLARE _xor
 WITH v1 : int, v2: int
 PRE [ _v1 OF tint, _v2 OF tint]
    PROP () 
    LOCAL (temp _v1 (Vint v1); temp _v2 (Vint v2))
    SEP ()
 POST [ tint ]
    PROP() 
    LOCAL (temp ret_temp (Vint (Int.xor v1 v2))) 
    SEP().

そのバージョンは「int」値、つまり CompCert の Int モジュールの 32 ビット整数を使用します。通常、数学的な整数で関数を指定するのが好きです。その仕様のスタイルは次のようになります:

Definition xor_spec2 :=
 DECLARE _xor
 WITH v1 : Z, v2: Z
 PRE [ _v1 OF tint, _v2 OF tint]
    PROP (0 <= v1 <= Int.max_unsigned; 0 <= v2 <= Int.max_unsigned) 
    LOCAL (temp _v1 (Vint (Int.repr v1)); temp _v2 (Vint (Int.repr v2)))
    SEP ()
 POST [ tint ]
    PROP() 
    LOCAL (temp ret_temp (Vint (Int.repr (Z.lxor v1 v2)))) 
    SEP().

警告: これらのいずれも Coq で実行していないため、小さなタイプミスがある可能性があります。そして、私は Z.lxor を十分に研究しておらず、それがあなたが望むものであることを確認していません。