--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Set global variables uninitialized at Value analysis start



Hi David,
You may explore the various results computed by InOut: if one of your global does not appears in the list of operational inputs, this means its initial value is never used.
As for changing the initial state of Value, this is possible but only programmatically. 
Hope this helps,
Benjamin Monate
TrustMySoft founder

Le 14 mai 2013 ? 22:04, "David MENTRE" <dmentre at linux-france.org> a ?crit :

> Hello,
> 
> I am analysing some embedded C code (complete application) with
> Frama-C Fluorine / Value analysis.
> 
> I would like to tell Frama-C that all global variables are
> uninitialized at program start (and not given a zero value, as assumed
> by default by Frama-C), so Frama-C would catch a read without first
> write to such a global variable.
> 
> I know option "-lib-entry" to tell Frama-C that the value of global
> variables are unknown.
> 
> But is there a way (command line option or trick) to mark global
> variables uninitialized?
> 
> Or would anybody have a suggestion to reach my goal, i.e. catch all
> read-before-write on global variables?
> 
> Thanks in advance for any help,
> Best regards,
> david
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss