Frama-C: Jessie plugin can't prove bitwise-or safety (w.r.t. overflow)

Question

I'm using Frama-C Nitrogen to analyze the following code

#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;
}

with

frama-c -jessie test.c

Unfortunately, Jessie isn't able to prove the absence of integer overflows. In particular, the following condition cannot be proved (assured that I'm interpreting the output correctly, which language is that? Where can I find a manual?):

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

By looking at a few previous lines we also get:

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

Shouldn't Jessie be able to infer a stronger property in H23? Like

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

It seems to me that Jessie is treating intermediate results as mathematical integers, therefore ignoring the unsigned char "hint".

I also tried the value analysis with:

frama-c -main test -val test.c

which yields the output:

[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}

The value analysis correctly computes the bounds for c, but I don't understand why the results for a and b are approximated (shouldn't they be trivial to determine?)

Any insights would be greatly appreciated.

Answer 1

which language is that?

This is Why either in its version 2 or in its version 3 (the transition was about at the time of the version you use).

the following condition cannot be proved […]:

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

It is always difficult to decide how to axiomatize C's bitwise operators. It completely depends on how the program being verified uses these operators. The Jessie/Why verification chain does not make a decision and leaves the axiomatization of these operators to you. This has been discussed before. This message promises some improvements (again, dating from about the time of the Nitrogen version, so either a bit before or a bit after).

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

In the results of the value analysis (option -val), [--..--] for a variable of an integer type means all the values of this type. Variables a and b can take any value of the type unsigned char, so the value of these variables is displayed as [--..--]. These results are not approximated, in this particular example they are optimal.