Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Uninitialized variables

  • Subject: [Frama-c-discuss] Uninitialized variables
  • From: m.vijay at nus.edu.sg (Vijayaraghavan Murali)
  • Date: Wed, 11 Apr 2012 15:57:24 +0800
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