--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] can we collect referenced variables with frama-c?



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