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

Question

我刚刚开始使用 verifiable-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"值，即32位来自 CompCert 的 Int 模块的整数。通常我喜欢在数学整数上指定我的函数；规范的风格就像：

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

你能post C 代码吗？从你最后的评论来看，你似乎有局部变量 "tmp"、"bit"、"key"，但我在 C 程序中看不到它们。

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

Finding ways to specify Functional Specification Verifiable-c

verifiable-c