--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on October 2014 ---
Hi, I am trying to prove a function A in file A.c which invokes another function B in file B.c, but this function B has the contract "assigns X" which is a static global variable in B.c. This causes a problem since function A cannot see variable X. I looked through the ACSL documentation (Neon version) and found that under the appendix "A.4.1 Accessing a C variable that is masked", which seems like the solution to my problem. However, after running Frama-C (Neon) on the example code: 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. George -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141023/24750d69/attachment.html>