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