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



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>