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