--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on April 2012 ---
Dear Pascal, Sorry if it came across as otherwise, but I didn't mean to criticize Frama-C. I was just trying to find a way around the issue. The assumption is indeed a valid one, it's just that for some of my benchmarks it doesn't always hold. Anyway I really appreciate the help. Thank you! Vijay On 4/11/2012 5:02 PM, Pascal Cuoq wrote: >> main() { >> int a,x; >> if(a> 0) x=a+1; >> else x=a+2; >> >> return x; >> } > > The above program invokes undefined behavior as per C99's J.2 clause: > >> The value of an object with automatic storage duration is used while it is >> indeterminate (6.2.4, 6.7.8, 6.8). > > To be very clear at the risk of boring people who already know this > stuff, ?undefined behavior? means that you cannot expect variable a to > have some value. Both branches in your program could be executed, or > the program could reformat your harddrive. Plus, if you get into the > habit of using uninitialized variables as a shortcut for ?anything? in > your analyses, you are at risk of someone eventually poking (gentle) > fun at you in a blog post: > > http://blog.frama-c.com/index.php?post/2011/11/25/Static-analysis-tools-comparisons > > But if you want to take that risk, go ahead and treat uninitialized > variables as unknown values. I never tire of writing these blog posts. > >> Now it's able to compute values for a and x as [--..--] (I guess it >> represents infinite range). > > You don't need to guess. This is documented on page 26 of: > http://frama-c.com/download/frama-c-value-analysis.pdf > >> is it possible to tweak Frama-C so that it can >> automatically assign infinite range for uninitialized variables (such as the >> eg above)? > > With the attached patch, that should apply without too much difficulty > to the Nitrogen release, the program above gives the result: > > [value] Values at end of function main: > x ? [--..--] > > Pascal > > Index: src/value/eval_funs.ml > =================================================================== > --- src/value/eval_funs.ml (revision 17768) > +++ src/value/eval_funs.ml (working copy) > @@ -376,9 +376,12 @@ > let with_locals = > List.fold_left > (fun acc local -> > - Cvalue.Model.add_binding_not_initialized > + Cvalue.Model.add_binding > + ~with_alarms:CilE.warn_none_mode > + ~exact:true > acc > - (Locations.loc_of_varinfo local)) > + (Locations.loc_of_varinfo local) > + Cvalue.V.top_int) > with_formals > f.slocals > in