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

[Frama-c-discuss] Uninitialized variables



> 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