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

[Frama-c-discuss] Acsl implicit cast Enumeration - integer



Hello Victoria,

Le lun. 22 f?vr. 2010 10:50:03 CET,
Victoria MOYA LAMIEL <victoria.moyalamiel at atosorigin.com> a ?crit :

> 1/ First of all, I've found some problems with the translation of this 
> /*@logic T_BOOLEEN test (integer b)=
>   @ (b==1)?
>   @   (T_BOOLEEN)VRAI
>   @   : (T_BOOLEEN) FALSE;
>   @*/
> What is wrong in this form ?

Thanks for the report, this is indeed a bug in the type-checker for
the logic. It is corrected in the development version.

> 
> 2/ The only way we found to translate it with Jessie was :
> 
> /*@logic T_BOOLEEN test (integer b)=
>   @ (T_BOOLEEN)((b==1)?
>   @   VRAI
>   @   : FALSE);
>   @*/
> 
> Nevertheless, this solution doesn't work with the integer model 
> ("-jessie-int-model exact").

This looks like a bug in the jessie plugin itself, but I'll let Jessie
experts comment on that particular topic.

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