--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Logic types and Ghost code



Hello B?rbara,

Le ven. 22 oct. 2010 14:32:03 CEST,
Barbara Vieira <barbaraisabelvieira at gmail.com> a ?crit :

> 
> I did as you suggested above. The problem is when I want to do some proofs with the successive changes of  logical variable (I need a variable with state) I'm not able to do it. The provers are always able to prove the assertions that I include in the code even when the things to prove are wrong.

Well, I warned you that this was not thoroughly tested ;-). However,
I'd say that the declaration of your logic variable does not completely
match what I suggested, and your issue might well lie therein:

> 
> - Declaration of the logical and ghost variables 
> //@ ghost int var_1;
> /*@ axiomatic logic_var_1{
>     logic list logic_var_1 reads var_1;
                           ^^^
                     There is an {L} missing to inform
                     the tool that you want logic_var_1 to depend
                     on the memory state where it is applied.
>     }
>   @*/

> 
> //@ ghost int var_2;
> /*@ axiomatic logic_var_2{
>     logic list logic_var_2 reads var_2;
                            ^^^
                            Same thing with logic_var_2 of course.
>     }
>   @*/

I haven't checked whether this is sufficient to make the generated PO
unprovable, but it should be a step in the good direction. Feel free to
tell me if there are still some problems.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile