verifiable-c - 寻找方法来指定功能规范 Verifiable-c

Question

我刚刚开始使用可验证的 c 工作，并且正在努力为我编写的 C 代码生成功能规范。我正在使用的基本示例是（C 代码）

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

而且我很难将定义 xor_spec 部分放在一起。

谢谢。

Answer 1

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 以确保它是你想要的。

Answer 2

可以发一下C代码吗？从您上一条评论来看，您似乎有局部变量“tmp”、“bit”、“key”，但我在 C 程序中看不到它们。