Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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