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

Then it would be taken for sure that the value of addr_c is &x in

//@ assigns *addr_x;
int f(int x) {
     // ...
     return g();
}

- Claude