Frama-C：Jessie 插件无法证明按位或安全（w.r.t. 溢出）

Question

我正在使用 Frama-C Nitrogen 来分析以下代码

#include "/usr/share/frama-c/builtin.h"

int test()
{
    const unsigned char a = Frama_C_interval(0, 255);
    const unsigned char b = Frama_C_interval(0, 255);
    const unsigned int c = ((unsigned int)a) | ((unsigned int)b);

    return 0;
}

与

frama-c -jessie test.c

很遗憾，Jessie 无法证明不存在整数溢出。 特别是，无法证明以下条件（确保我正确解释了输出，那是哪种语言？我在哪里可以找到手册？）：

 0 <= bw_or(integer_of_uint32(result7), integer_of_uint32(result8))

通过查看前面的几行，我们还得到：

H23: 0 <= integer_of_uint8(b) and integer_of_uint8(b) <= 429496725
H24: integer_of_uint32(result8) = integer_of_uint8(b)

Jessie 不应该能够在 H23 中推断出更强的属性吗？ 喜欢

H23: 0 <= integer_of_uint8(b) and integer_of_uint8(b) <= 255

在我看来，Jessie 将中间结果视为数学整数，因此忽略了无符号字符“提示”。

我也尝试过价值分析：

frama-c -main test -val test.c

产生输出：

[kernel] preprocessing with "gcc -C -E -I.  test.c"
[value] Analyzing a complete application starting at test
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        Frama_C_entropy_source ∈ [--..--]
[value] computing for function Frama_C_interval <- test.
    Called from new_test.c:5.
/usr/share/frama-c/builtin.h:46:[value] Function Frama_C_interval: precondition got status valid.
/usr/share/frama-c/builtin.h:47:[value] Function Frama_C_interval: postcondition got status unknown.
[value] Done for function Frama_C_interval
[value] computing for function Frama_C_interval <- test.
        Called from new_test.c:6.
[value] Done for function Frama_C_interval
new_test.c:7:[value] assigning non deterministic value for the first time
[value] Recording results for test
[value] done for function test
[value] ====== VALUES COMPUTED ======
[value] Values for function test:
          Frama_C_entropy_source ∈ [--..--]
          a ∈ [--..--]
          b ∈ [--..--]
          c ∈ [0..255]
          __retres ∈ {0}

值分析正确计算了 c 的界限，但我不明白为什么 a 和 b 的结果是近似的（确定它们不应该是微不足道的吗？）

任何见解都将不胜感激。

Answer 1

那是什么语言？

这是 Why 的版本 2 或版本 3（转换大约在您使用的版本时）。

以下条件无法证明[…]：

0

决定如何公理化 C 的位运算符总是很困难的。这完全取决于被验证的程序如何使用这些运算符。 Jessie/Why 验证链不会做出决定，并将这些运算符的公理化留给您。这在之前已经讨论过了。这个message 承诺了一些改进（同样，大约可以追溯到 Nitrogen 版本的时间，所以要么早一点，要么晚一点）。

我不明白为什么 a 和 b 的结果是近似的（确定它们不应该是微不足道的吗？）

在值分析（选项-val）的结果中，整数类型变量的[--..--] 表示该类型的所有值。变量 a 和 b 可以取 unsigned char 类型的任何值，因此这些变量的值显示为 [--..--]。这些结果不是近似的，在这个特定的例子中它们是最优的。