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

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