--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on November 2009 ---
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.