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: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Mon, 30 Sep 2013 17:35:44 +0200
  • In-reply-to: <CAC3Lx=bfbFo5Zciu8T_U0-3gzK2choL0qJZC7==8ixfGrhbYiw@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>
Hello David,

2013/9/30 David MENTRE <dmentre at linux-france.org>:

>   * If I try to keep only the definition points, where "vi.vdefined =
> true" as shown on Anne's page
> (https://anne.pacalet.fr/Notes/outils/frama-c/scripts/#index3h2), but
> some variables are missing;

If I'm not mistaken, vdefined will be true only for variables that
have an explicit initializer.
Implicitely 0-initialized objects will show up with vdefined equal to false.

>
>   * I don't need to use "Rmtmps.keepUnused := true" trick, as I am
> already seeing all my variables;

Again if I'm not mistaken, global variables are always kept. Only
unused function prototypes and types are removed.

>
>   * 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.

> 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).
>
>   * I have a variable "v" erroneously defined in two C files (a.c and
> b.c): what is the expected behaviour of a C compiler and Frama-C in
> such a case?
As often with the C standard, nothing is completely clear. (references
below are made against C99):
Following 6.2.2?5, and ?2, as long as v is not explicitely declared
static in one of the files, it should refer to the same object after
link. In addition, it should not be initialized explicitely in both
files (as per 6.9?5).
That said, 6.9.2?2 seems to indicate that if you only have int v; in a
file (without an explicit extern declaration), it should be treated as
int v = 0;, so that you would end up with a variable defined in both
a.c and b.c.
A quick check suggests that neither gcc nor clang does the latter: as
long as v is explicitely initialized in at most one file, they will
link the program and use this initializer, as does Frama-C.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile