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] Set global variables uninitialized at Value analysis start

  • Subject: [Frama-c-discuss] Set global variables uninitialized at Value analysis start
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 14 May 2013 16:57:01 +0200
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