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

[Frama-c-discuss] Uninitialized variables



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