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