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.