--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2013 ---
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