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