goto generated by Frama-C and not supported by Jessie
ID0000332: This issue was created automatically from Mantis Issue 332. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000332 | Frama-C | Kernel | public | 2009-11-17 | 2010-04-13 |
| Reporter | dpariente | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
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.
But Jessie doesn't support this feature: File "slicef.jc", line 42, characters 7-16: unsupported goto (backward or to some inner block)
Category of this report is "kernel" as it is let up to Frama-C team to choose between an evolution of Jessie (in order to take this feature into account) or a change in the way the Kernel (CIL) transforms boolean equations.