frama-c - 使用 frama-c 引理检查无符号整数中的位不起作用

Question

使用 frama-c 我正在编写使用位域来表示集合的代码。说类似

typedef uint32_t  myset_t;

#define EMPTY_SET  UINT32_C(0)
#define FULL_SET   UINT32_C(0x0ffffff)

所以我只使用 32 位无符号整数的 n 最低位。然后我想实现一个谓词来检查“myset_t”中是否设置了一个位。这没有按预期工作（带有 alt-ergo 的 frama-c 能够证明有关此类集合的内容），我可以生成一个简单的引理，它已经表明了我的问题。在我的安装（frama-c 21.1 Scandium）上，它不能自动证明以下简单的引理：

    lemma test:
        \forall integer i;
        (0U <= i < 16U) ==> (0xFFFFU & (1U << (unsigned int)i)) != 0U;

有谁能向我解释我做错了什么以及问题出在哪里？还是定理证明者不能自动正确地处理这些琐碎的算术问题（我的意思是只有 16 种情况，可以列举它们）。

标签： frama-c

Answer 1

似乎自动求解器无法处理 WP 生成的属性。可能是因为他们不能，也可能是因为属性的编码。

尽管如此，正如你所说：

这只是16个案例，一个可以枚举它们

WP GUI 提供了一种策略来生成这样的证明。一旦证明失败，双击窗口底部“WP 目标”面板中的证明目标。然后选择要枚举的变量。点击战术“范围”，将下限设置为 0，上限设置为 15。最后，点击战术名称旁边的绿色箭头。WP 将生成 18 个证明目标：

• < 0和> 15：微不足道，因为条件是0 <= i <= 15
• 0, 1, 2, 3 ..., 15: 由 WP Qed 自动放电

然后您可以单击保存图标，以便轻松重播证明。

如果您想在 GUI 中重放证明，您可以使用存在证明脚本时出现在“WP 目标”面板中的箭头。tip或者您可以通过添加到证明者列表中直接要求使用命令行中的现有脚本：

frama-c -wp -wp-prover alt-ergo,tip file.c

请注意，WP 脚本保存在 WP 会话中，默认情况下在目录中./.frama-c/wp/scripts。可以使用选项配置 WP 会话目录wp-session <directory>。