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

I misunderstood the [--..--], I thought it was an empty interval. Thanks for
the help.

Best regards,
Jo?o

2010/4/22 Pascal Cuoq <pascal.cuoq at gmail.com>

> 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
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100422/07710dfa/attachment.htm>