--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on April 2010 ---
I misunderstood the [--..--], I thought it was an empty interval. Thanks for the help. Best regards, Jo?o 2010/4/22 Pascal Cuoq <pascal.cuoq at gmail.com> > On Thu, Apr 22, 2010 at 4:27 PM, Joao Antunes <j37140 at gmail.com> wrote: > > 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] ? [--..--] > > If a is an unsigned char array, then [--..--] for the elements of a > mean the range [0..255]. > Intervals covering the full range of possible values and not > containing any addresses > are displayed this way because they happen often and seeing > -2147483648, 2147483647, > and 4294967295 gets tiresome after a while. > > > > 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? > > a and b appear to be arrays, but assuming that they are arrays of > unsigned chars, > be assured that each element is in the range [0..255]. We wouldn't have to > guess > if you provided a C program, but since you didn't, I assume that you could > have > written: > > int x; > unsigned char y; > > int main() > { > y = Frama_C_interval(0,255); > x = y; > } > > and obtained with the commanline: > > frama-c -val t.c /usr/local/Frama-C_Be/share/frama-c/builtin.c > > the result: > > x ? [0..255] > y ? [--..--] > > You could also have used the program: > > int x; > unsigned char y; > > int main() > { > y = Frama_C_interval(0,254); > x = y; > } > > and obtained: > > x ? [0..254] > y ? [0..254] > > So what is the problem? > > 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/07710dfa/attachment.htm>