--- layout: fc_discuss_archives title: Message 25 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 Fri, Oct 24, 2014 at 5:13 PM, Khairul Azhar Kasmiran <kazarmy at gmail.com>
wrote:

>
>
>> I have tried this too and it works.
>>
>>
> Would you mind sharing the working code?
>
>
>
> --
> Khairul
>
>
Here is the code:

int x;

//@ logic int *l_x = &x;
//@ assigns x;
int g();

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

Note that this entire piece of code is in the same source file.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141030/fd9b2228/attachment.html>