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