--- layout: fc_discuss_archives title: Message 99 from Frama-C-discuss on January 2014 ---
Hi, On Mon, Jan 27, 2014 at 9:29 AM, David MENTRE <dmentre at linux-france.org> wrote: > Hello Dharmalingam, > > Le 25/01/2014 21:17, Dharmalingam Ganesan a ?crit : > >> For this below function, the value plugin says the >> >> [value] Values at end of function myFun: >> i ? [--..--] >> >> >> In my understanding [--, --] refers to all possible integers. But, the >> value of i for this function can never be below zero. Value's manual is misleading on this point. When querying the value of a l-value [--..--], means all possible integers *that fit within the type*. Here, on your 32 bits unsigned value, this amounts to [0..4294967295]. This is not a display artefact: for various (good) reasons, [--..--] is exactly what Value stores internally. > In fact, Value analysis knows about this fact, see below > "Frama_C_show_each_i([0..4294967295])". Exactly. When you call a primitive such as Frama_C_show_each, [--..--] is converted to the actual range. Another option is to use the "Evaluate term" contextual menu, in order to evaluate 'i+0'. > Maybe Value prints "[--..--]" because the whole range of variable "i" is > seen? Yes. > In below int.c program (with an "int" instead of "unsigned int"), the Value > analysis computes the correct range for i: > > --------------- > #include <limits.h> > > int i = 0; > > void myFun() > { > if (i == INT_MAX) { > i = 0; > } > i++; > Frama_C_show_each_i(i); > } > > void main(void) > { > while (Frama_C_nondet(0,1)) { > myFun(); > } > } > ---------------- > > $ frama-c -val `frama-c -print-share-path`/builtin.c -slevel 10 int.c > [...] > > [value] ====== VALUES COMPUTED ====== > [value] Values at end of function Frama_C_nondet: > Frama_C_entropy_source ? [--..--] > > [value] Values at end of function myFun: > i ? [1..2147483647] > [value] Values at end of function main: > Frama_C_entropy_source ? [--..--] > i ? [0..2147483647] Indeed. As [0..2147483647] does not cover the entire range for i (the negative values are missing), we do not display [--..--]. To complicate matters further, notice that your guard > if (i == INT_MAX) { > i = 0; > } is not needed to obtain those results. Since signed integer overflow is an undefined behavior, the alarm emitted by Value on the line i++ is sufficient to guarantee that i will never become negative. Without the 'if', the exact same values are inferred for i. HTH, -- Boris