--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on April 2010 ---
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