--- layout: fc_discuss_archives title: Message 146 from Frama-C-discuss on September 2013 ---
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