formal-verification - Frama-C を使用した FFS (Find First Set) の検証

Question

FFS のソフトウェア実装を検証しようとしています。FFS の機能は、数値の最下位ビットのインデックス位置 (1 から始まる) を返すことです。ゴースト変数を使用するなど、さまざまな方法で試しました。ジェシーはそれを確認できず、理由がわかりませんか? いくつかの指針は本当に役に立ちます。これがコードのサンプルです。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;
}