--- layout: fc_discuss_archives title: Message 10 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



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