--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on October 2014 ---
On Thu, Oct 23, 2014 at 4:59 PM, Virgile Prevosto <virgile.prevosto at m4x.org> wrote: > Hello, > > > 2014-10-23 10:12 GMT+02:00 gg lee <georgeleeliangwei at gmail.com>: > > > > > int x; > > > > //@ ghost int* const ghost_ptr_x = &x; > > > > //@ assigns x; > > int g() > > { > > return x; > > } > > > > //@ assigns *ghost_ptr_x; > > int f(int x) { > > // ... > > return g(); > > } > > > > > > surprisingly I am not able to prove the code completely. Please help me > on > > this as I have been stuck on this for a few days. Thanks. > > > > Lo?c's answer explains how ACSL should be extended to deal with your > issue. 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). > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > > Thank you for the suggestion. I tried using -wp-init-const but I think there is no such option..at least for Neon version. Which version of Frama-C provides such option? Perhaps I can switch to that version to give it a try. George -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141023/2cf02217/attachment.html>