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