--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on February 2011 ---
On 2/16/11, Deng, Xu <xu.deng at intel.com> wrote: > Can we use frama-c to collect the referenced (used/modified) global > variables of a function, including the global variables referenced by the > functions called in this function? http://frama-c.com/features.html says: "the list of global variables that a function is supposed to read or write to is a formal specification. Frama-C can compute this information automatically from the source code of the function" > For example: > The func() actually has modified S.a, S.p and S.a, can frama-c support > collecting this information? Your program does not compile, but if it did, "frama-c -out -input t.c -main func" would tell you that func actually reads s1.p and writes s1; s0.a; and p. Pascal __ For what it's worth, here is the program I actually analyzed with the command above: struct S0{ int a; int b; }; struct S{ int a; struct S0 *p; }; struct S s1; struct S0 s0; void func() { s1.a=1; s1.p=&s0; struct S0 *p = s1.p; func2(p); } void func2(struct S0 *p) { p->a = 0; }