--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Uninitialized variables



Hi,

I noticed that in Frama-C many plugins assume that all variables are 
initialized to some value in the input program. For eg,

main() {
   int a,x;
   if(a > 0) x=a+1;
   else x=a+2;

   return x;
}

For the above program, the value plugin returns "NON TERMINATING 
FUNCTION". But if I initialize a and x to:

main() {
   int a=nondet(), x=nondet();
   if(a > 0) x=a+1;
   else x=a+2;

   return x;
}

Now it's able to compute values for a and x as [--..--] (I guess it 
represents infinite range). This also affects all plugins dependent on 
value analysis.

I use certain abstractions in program verification, so this assumption 
is not valid for some of my programs. So my question is: other than 
modifying the input program, is it possible to tweak Frama-C so that it 
can automatically assign infinite range for uninitialized variables 
(such as the eg above)? Or is there a way to forbid Frama-C from making 
this assumption in the first place?

Thanks,

---

Vijayaraghavan Murali
http://www.comp.nus.edu.sg/~mvijayar