我尝试编写 ACSL 谓词以查看整数是否为 2 的幂,如下所示:
/*@
predicate positive_power_of_2 (integer i) =
i > 0 &&
(i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1)));
*/
但是,当我将一些断言行添加到随机函数中时,会出现一些超时(即失败)。我不明白为什么?
//@ assert positive_power_of_2 (1); // Timeout
//@ assert positive_power_of_2 (2); // Valid
//@ assert positive_power_of_2 (4); // Valid
//@ assert !positive_power_of_2 (7); // Timeout