--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value-analysis range values



On Thu, Apr 22, 2010 at 4:27 PM, Joao Antunes <j37140 at gmail.com> wrote:
> What i want to do is when I use some variables type char define their range
> between?[0..255], because when I use some bitwise operations with char's I
> get this result:
>
> [value] Values for function main:
>
> ?? ? ? ? ?a[0..130] ? [--..--]

If a is an unsigned char array, then [--..--] for the elements of a
mean the range [0..255].
Intervals covering the full range of possible values and not
containing any addresses
are displayed this way because they happen often and seeing
-2147483648, 2147483647,
and 4294967295 gets tiresome after a while.


> As you can see the variables "a" and "b" don't have any range defined. Is it
> possible to use?Frama_C_interval() in these cases?

a and b appear to be arrays, but assuming that they are arrays of
unsigned chars,
be assured that each element is in the range [0..255]. We wouldn't have to guess
if you provided a C program, but since you didn't, I assume that you could have
written:

int x;
unsigned char y;

int main()
{
  y = Frama_C_interval(0,255);
  x = y;
}

and obtained with the commanline:

frama-c -val t.c /usr/local/Frama-C_Be/share/frama-c/builtin.c

the result:

  x ? [0..255]
  y ? [--..--]

You could also have used the program:

int x;
unsigned char y;

int main()
{
  y = Frama_C_interval(0,254);
  x = y;
}

and obtained:

 x ? [0..254]
 y ? [0..254]

So what is the problem?

Pascal