Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Printing all global variables of a set of C files?

  • Subject: [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 2 Oct 2013 16:30:29 +0200
  • In-reply-to: <CA+yPOViM5uojsLY10UTC1RMDb5fCQVcoPMirmh1+eJ7AmMcOLQ@mail.gmail.com>
  • References: <CAC3Lx=YHQsCeWEP0q7eZbfz1S9OS2625Lrk4BR5-MVF+jXZw+g@mail.gmail.com> <1A32855E5FA08141A8C56E7CF24D442C0F007D83@SCTEX101.st-cloud.dassault-avion.fr> <CAC3Lx=bfbFo5Zciu8T_U0-3gzK2choL0qJZC7==8ixfGrhbYiw@mail.gmail.com> <CA+yPOViM5uojsLY10UTC1RMDb5fCQVcoPMirmh1+eJ7AmMcOLQ@mail.gmail.com>
Hello Virgile,

Thank you for the explanations on the behaviour of Frama-C.

2013/9/30 Virgile Prevosto <virgile.prevosto at m4x.org>:
>>   * Some definition location refer to the foo.h instead of the foo.c
>> file. I checked for some of those variables: the foo.h file correctly
>> defines the variable as "extern" (extern int v;) and the foo.c file
>> defines the variable (int v;). Why the foo.h file is referenced? I
>
> My guess is that int v; is seen as a re-declaration instead of a
> proper definition (see above remark about vdefined). Then, only the
> first declaration is kept. If you have int x = 0; instead, you should
> obtain the location of the explicit definition.

OK, this is indeed the case. This is illustrated with files q12_a.c
and q12_a.h attached.

Variable g1 is see defined in the q12_a.c file while g2, not
initialized in the C file, is seen defined in q12_a.h.
"""
Global Var: g1 : q12_a.c:3
Global Var: g2 : q12_a.h:5
"""

>> also observe the same behaviour for a global variable referenced into
>> another C file (using "extern int v" in a function f()), the location
>> printed is this later location (I would have expected the former
>> definition location).

The attached files also illustrate this behaviour: variable g3 is
defined in q12_a.c but is seen defined in q12_b.c by Frama-C.

"""
Global Var: g3 : q12_b.c:5
"""

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q12_a.c
Type: text/x-csrc
Size: 106 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131002/ce61ab5d/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q12_a.h
Type: text/x-chdr
Size: 32 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131002/ce61ab5d/attachment.h>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: q12_b.c
Type: text/x-csrc
Size: 46 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131002/ce61ab5d/attachment-0001.c>