--- layout: fc_discuss_archives title: Message 64 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



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>