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

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