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

2013/5/27 Pascal Cuoq <pascal.cuoq at gmail.com>:
> 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

Thanks a lot for the trick! This is exactly what I wanted. Doing such
kind of modification on my real program, I could catch an
uninitialized value! \o/

I have a bunch of globals (about 150) but I should be able to manage
that with some sed scripting.

Best regards,
david