c - 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 将中间结果视为数学整数，因此忽略了 unsigned char“提示”。

我还尝试了值(value)分析:

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

which language is that?

这是Why无论是在版本 2 中还是在版本 3 中(转换大约是在您使用版本时进行的)。

the following condition cannot be proved […]:

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

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

I don't understand why the results for a and b are approximated (shouldn't they be trivial to determine?)

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