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



>
> Here is the code:
>
>
Thanks! I was wondering about g().

:)

--
Khairul

On Thu, Oct 30, 2014 at 2:01 PM, George Lee <georgeleeliangwei at gmail.com>
wrote:

>
>
> 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.
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141030/d4122ce5/attachment.html>