--- layout: fc_discuss_archives title: Message 22 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 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>