--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on October 2014 ---
On Thu, Oct 23, 2014 at 10:57 PM, Virgile Prevosto <virgile.prevosto at m4x.org > wrote: > > > 2014-10-23 16:03 GMT+02:00 Claude Marche <Claude.Marche at inria.fr>: > > > > > > On 10/23/2014 10:59 AM, Virgile Prevosto wrote: > >> > >> However, if we go back to your concrete example, my guess is > >> that you're just missing the -wp-init-const option on the command > >> line, that tells WP to assume that global const variables always have > >> their initial values (const specifier is so easily abused that this > >> option is not on by default). > > > > > > Just a thought, not tested, why not using a logic constant instead of a > > ghost, e.g > > > > //@ logic int *addr_x = &x; > > > > Indeed, this works perfectly well, I'm not sure why I didn't think about > it [?] > > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > > I have tried this too and it works. Now I have this burning question: why does "logic" work in this case and "ghost" fails? What is the main difference between the two? As I am new to Frama-C and am learning how to use it, any explanation here will be greatly appreciated. Thanks! George -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141024/cb935fce/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: 35F.gif Type: image/gif Size: 540 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141024/cb935fce/attachment.gif>