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



Hi Vergile,


A 2010/10/25, ?s 09:20, Virgile Prevosto escreveu:

> 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.
>>    }
>>  @*/

It worked ;-) I'm sorry, but I completely forgot the labels.

> 
> 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.

The PO are not provable now! 

Thank you very much for your help.
Best regards,
B?rbara 



> 
> Best regards,
> -- 
> E tutto per oggi, a la prossima volta.
> Virgile
> 
> 
> _______________________________________________
> 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