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

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