--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on February 2011 ---
It works well for simple program when it only has one .c file, how to use it when we have a lot of .c files and .h files in a complex project? Can frama-c merge the input/output information of all the .c files? Thanks Xu Deng 8621-7069 -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Deng, Xu Sent: Wednesday, February 16, 2011 1:26 PM To: Frama-C public discussion Subject: Re: [Frama-c-discuss] can we collect referenced variables with frama-c? Great thanks for the quick response, let me have a try. Thanks Xu Deng 8621-7069 -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal Cuoq Sent: Wednesday, February 16, 2011 1:16 PM To: Frama-C public discussion Subject: Re: [Frama-c-discuss] can we collect referenced variables with frama-c? 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; } _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss