frama-c - 如何使用 Frama-C 证明这个 C is_power_of_2 函数？

Question

在上一个问题中，我寻求帮助编写 apredicate以查找数字是否为 2 的幂。这是尝试证明以下 C 函数的前奏：

static inline bool
is_power_of_2 (unsigned long v)
{
  return v && ((v & (v - 1)) == 0);
}

（这个“技巧”来自这里）。使用我尝试过的前一个谓词：

/*@
  ensures positive_power_of_2 (v) <==> \result == \true;
 */

但我使用的各种 SMT 求解器（alt-ergo、z3、gappa、cvc4）似乎都无法证明这一点。

标签： frama-cacsl