--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on October 2014 ---
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