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



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