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