Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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