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

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] ? [--..--]

          b[0..15] ? [--..--]

          i ? {32; }

          __retres ? {0; }


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?


Best regards,

Jo?o


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

> Hello,
>
> On Thu, Apr 22, 2010 at 2:06 AM, Joao Antunes <j37140 at gmail.com> wrote:
> > Hi everyone, I have a small doubt regardind the value-analysis plugin of
> > Frama-C. Is it possible to define bitwise operations in this plugin? If
> so,
> > how can I send to the plugin the information of the range of that
> > operations? I have this doubt because when I do bitwise operations the
> > plugin doesn't define any kind of range or interval of values to the
> > variables that i create.
>
> Could you give more details about what you did, what result you
> obtained and what you would have liked to see instead?
>
> Example: when I type the following program:
>
> int x,y;
>
> int main()
> {
>  x = Frama_C_interval(11,17);
>  y = Frama_C_interval(3,21);
>  return x&y;
> }
>
> and use the commandline:
>
> frama-c -val t.c /usr/local/Frama-C_Be/share/frama-c/builtin.c
>
> I get:
>
>   __retres ? [0..17]
>
> which is the optimal answer, so I do not wish to see any other result.
>
> Regards,
>
> 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/cdb4c7c7/attachment.htm>