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



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>