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

> 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