--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on February 2010 ---
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