--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on October 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unable to prove the example code in ACSL documentation



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>