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
- Follow-Ups:
- [Frama-c-discuss] Printing all global variables of a set of C files?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Printing all global variables of a set of C files?
- References:
- [Frama-c-discuss] Printing all global variables of a set of C files?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Printing all global variables of a set of C files?
- From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
- [Frama-c-discuss] Printing all global variables of a set of C files?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Printing all global variables of a set of C files?
- Prev by Date: [Frama-c-discuss] Printing all global variables of a set of C files?
- Next by Date: [Frama-c-discuss] Printing all global variables of a set of C files?
- Previous by thread: [Frama-c-discuss] Printing all global variables of a set of C files?
- Next by thread: [Frama-c-discuss] Printing all global variables of a set of C files?
- Index(es):