1

我正在尝试验证 FFS 的软件实现。FFS 的作用是返回一个数字中最低位的索引位置（从 1 开始）。我尝试了许多不同的方式，包括使用幽灵变量。Jessie 无法验证，我不知道为什么？一些指示会非常有帮助。这是代码示例，我假设是 8 位数字：

/*@

requires x >= 0;
assigns x;

behavior zero:
  assumes x == 0;
  ensures \result == 0;

behavior nonzero1:
  assumes x > 0;
  assumes (x & 1) == 1;
  ensures \result == 1;

behavior nonzero2:
  assumes x > 0;
  assumes (x & 2) == 2;
  assumes (x & 1) == 0;
  ensures \result == 2;

behavior nonzero3:
  assumes x > 0;
  assumes (x & 4) == 4;
  assumes (x & 1) == 0;
  assumes (x & 2) == 0;
  ensures \result == 3;

behavior nonzero4:
  assumes x > 0;
  assumes (x & 8) == 8;
  assumes (x & 1) == 0;
  assumes (x & 2) == 0;
  assumes (x & 4) == 0;
  ensures \result == 4;

behavior nonzero5:
  assumes x > 0;
  assumes (x & 16) == 16;
  assumes (x & 1) == 0;
  assumes (x & 2) == 0;
  assumes (x & 4) == 0;
  assumes (x & 8) == 0;
  ensures \result == 5;

behavior nonzero6:
  assumes x > 0;
  assumes (x & 32) == 32;
  assumes (x & 1) == 0;
  assumes (x & 2) == 0;
  assumes (x & 4) == 0;
  assumes (x & 8) == 0;
  assumes (x & 16) == 0;
  ensures \result == 6;

behavior nonzero7:
  assumes x > 0;
  assumes (x & 64) == 64;
  assumes (x & 1) == 0;
  assumes (x & 2) == 0;
  assumes (x & 4) == 0;
  assumes (x & 8) == 0;
  assumes (x & 16) == 0;
  assumes (x & 32) == 0;
  ensures \result == 7;

behavior nonzero8:
  assumes x > 0;
  assumes (x & 128) == 128;
  assumes (x & 1) == 0;
  assumes (x & 2) == 0;
  assumes (x & 4) == 0;
  assumes (x & 8) == 0;
  assumes (x & 16) == 0;
  assumes (x & 32) == 0;
  assumes (x & 64) == 0;
  ensures \result == 8;
*/

int my_ffs(char x) {

  int r = 1;

  if (!(x))
    return 0;

  if (!(x & 0xf)) {
    x >>= 4;
    r += 4;
  }
  if (!(x & 3)) {
    x >>= 2;
    r += 2;
  }
  if (!(x & 1)) {
    x >>= 1;
    r += 1;
  }

  return r;
}
4

0 回答 0