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

[Frama-c-discuss] Uninitialized variables



Hello,

2012/4/11 Vijayaraghavan Murali <m.vijay at nus.edu.sg>:
> So my question is: other than modifying the input program, is it possible to
> tweak Frama-C so that it can automatically assign infinite range for
> uninitialized variables (such as the eg above)? Or is there a way to forbid
> Frama-C from making this assumption in the first place?

Beyond Pascal's response which you should take into account (e.g. by
using one of frama_c_* to initialize your variable to an unknown
value), you can use -lib-entry option to consider all global variables
to have unknown values, instead of zero value.

Best regards,
david