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: Benjamin.MONATE at cea.fr (MONATE Benjamin 205998)
  • Date: Tue, 14 May 2013 20:33:23 +0000
  • In-reply-to: <CAC3Lx=Zzm7DFwU_XEtn+u_p=18kgn-qFRQMp5VOpBqRs8PDZAw@mail.gmail.com>
  • References: <CAC3Lx=Zzm7DFwU_XEtn+u_p=18kgn-qFRQMp5VOpBqRs8PDZAw@mail.gmail.com>
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