--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on October 2014 ---
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 -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141023/2b1ef96d/attachment-0001.html> -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: 35F.gif Type: image/gif Taille: 540 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141023/2b1ef96d/attachment-0001.gif>