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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 27 May 2013 17:45:05 +0200
  • In-reply-to: <CAC3Lx=brLLEht0LqH7TMdTvexPKExjpS+btJcWc60mCup_rtFA@mail.gmail.com>
  • References: <CAC3Lx=Zzm7DFwU_XEtn+u_p=18kgn-qFRQMp5VOpBqRs8PDZAw@mail.gmail.com> <E50756B2-BF80-4A38-AE62-AD3F4A70A264@cea.fr> <CAC3Lx=ZT5n1iZ-oJZHGr2emVsNRd2HgoSaC+Tghn69Cj=UR0eA@mail.gmail.com> <CAC3Lx=brLLEht0LqH7TMdTvexPKExjpS+btJcWc60mCup_rtFA@mail.gmail.com>

Hello, David.


On Mon, May 27, 2013 at 4:39 PM, David MENTRE <dmentre at linux-france.org>wrote:

> > I'll ask back at the original code's developer about his exotic
> > developing environment and check the real needs.
>
> I checked. In his development environment, some global variables are
> indeed uninitialized at program start. So I need to mark them
> "UNITIALIZED" (uninitialized) and not "[--..--]" (initialized to an
> unknown value, done with -lib-entry).
>

If it is only ?some? global variables that need to uninitialized,
then you could mark them as such in your own main() before
launching the real main():

~ $ cat un.c
int a, b, c;

int main(int argc, char **argv){
  Frama_C_dump_each();
}

int uninitialize_and_main(int argc, char **argv){
  // mark variable(s) as uninitialized
  char uninitialized[640] ; // ought to be enough for anyone
#define UNINIT(t, v) v = * (t *) uninitialized;
  UNINIT(int, c);
  return main(argc, argv);
}
~ $ frama-c -val un.c -main uninitialize_and_main
[kernel] preprocessing with "gcc -C -E -I.  un.c"
[value] Analyzing a complete application starting at uninitialize_and_main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
  a ? {0}
  b ? {0}
  c ? {0}
[value] computing for function main <- uninitialize_and_main.
        Called from un.c:12.
[value] DUMPING STATE of file un.c line 4
        a ? {0}
        b ? {0}
        argc ? [--..--]
        argv ? {‌{ NULL ; &S_argv }‌}
        argc ? [--..--]
        argv ? {‌{ NULL ; &S_argv }‌}
        S_argv[0] ? {‌{ NULL ; &S_0_S_argv }‌}
              [1] ? {‌{ NULL ; &S_1_S_argv }‌}
        S_0_S_argv[0..1] ? [--..--]
        S_1_S_argv[0..1] ? [--..--]=END OF DUMP==
[value] Recording results for main
[value] Done for function main
[value] Recording results for uninitialize_and_main
[value] done for function uninitialize_and_main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  __retres ? {0}
[value] Values at end of function uninitialize_and_main:
  c ? UNINITIALIZED

Do not worry about c not appearing in the dump, this only means that it is
properly uninitialized.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130527/636245f0/attachment-0001.html>