--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] goto generated by Frama-C and not supported by Jessie



Hello,

When slicing (or simply analyzing) a function like the following one:

void f(int*p,int e,int t,int f,int r)
{
  *p = ( (e || (t && f)) && (t || f) );
}

Frama-C translates it into:

/* Generated by Frama-C */
void f(int *p , int e , int t , int f_0 , int r ) 
{
  int tmp ;
  if (e) { goto _LOR; }
  else {
    if (t) {
      if (f_0) {
        _LOR: /* internal */ ;
        if (t) { tmp = 1; }
        else { if (f_0) { tmp = 1; } else { tmp = 0; } }
      }
      else { tmp = 0; }
    }
    else { tmp = 0; }
  }
  *p = tmp;
  return;
}

with a goto to a inner block.

Unfortunately, Jessie doesn't support this feature:
File "slicef.jc", line 42, characters 7-16: unsupported goto (backward
or to some inner block)

Indeed, either there is a means to make CIL avoid transforming this
equation in that way, or it is a new feature to add to Jessie!
What can be done to get around this point in a short term?

Any idea will be welcome!
D.