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

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