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



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>