| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000332 | Frama-C | Kernel | public | 2009-11-17 17:01 | 2010-04-13 15:33 | ||||
| Reporter | dpariente | ||||||||
| Assigned To | virgile | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Boron-20100401 | |||||||
| Summary | 0000332: goto generated by Frama-C and not supported by Jessie | ||||||||
| 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
virgile (developer) 2010-01-12 18:36 |
Jessie relies on ad'hoc normalization of C code, which it sets when -jessie is enabled. If it used on code pretty-printed by frama-c and re-parsed, the ad'hoc normalization phase is no longer possible (it must occur at the first parsing). A new option -jessie-adhoc-normalization will force such normalization even if the jessie analysis is not triggered (allowing for instance a slicing phase before it). Is this an acceptable work-around? |
|
dpariente (reporter) 2010-01-12 19:08 |
At a first glance, it seems OK. Thanks. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2009-11-17 17:01 | dpariente | New Issue | |
| 2010-01-12 18:36 | virgile | Note Added: 0000619 | |
| 2010-01-12 18:36 | virgile | Status | new => feedback |
| 2010-01-12 19:08 | dpariente | Note Added: 0000620 | |
| 2010-01-13 17:01 | virgile | Status | feedback => resolved |
| 2010-01-13 17:01 | virgile | Resolution | open => fixed |
| 2010-01-13 17:01 | virgile | Assigned To | => virgile |
| 2010-04-13 15:30 | signoles | Status | resolved => new |
| 2010-04-13 15:31 | signoles | Status | new => closed |
| 2010-04-13 15:33 | signoles | Fixed in Version | => Frama-C Boron |
| Issue History |