--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on February 2010 ---
Hello, I have a question about the Jessie plugin concerning implicit casts between an enumerated type and integer one in Acsl. 1/ First of all, I've found some problems with the translation of this code by Jessie (test3.c) : typedef enum{ VRAI=1, FALSE=0 }T_BOOLEEN; /*@logic T_BOOLEEN test (integer b)= @ (b==1)? @ (T_BOOLEEN)VRAI @ : (T_BOOLEEN) FALSE; @*/ /*@ensures \result == test(boo); @*/ T_BOOLEEN test(int boo) { T_BOOLEEN b; if (boo==1) b = VRAI; else b= FALSE; return b; } What is wrong in this form ? 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"). Is there another way to express it or is it a problem on the Jessie plugin? Thank you in advance. Best regards, Victoria -- -------------- next part -------------- A non-text attachment was scrubbed... Name: test2.c Type: text/x-csrc Size: 290 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100222/8582b1ea/attachment.c -------------- next part -------------- A non-text attachment was scrubbed... Name: test3.c Type: text/x-csrc Size: 300 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100222/8582b1ea/attachment-0001.c