| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000187 | Frama-C | Plug-in > jessie | public | 2009-07-14 17:07 | 2010-12-09 19:20 | ||||
| Reporter | lukaszc | ||||||||
| Assigned To | cmarche | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Beryllium-20090601-beta1 | ||||||||
| Target Version | Fixed in Version | Frama-C Beryllium-20090902 | |||||||
| Summary | 0000187: Error while processing legitimate C construction | ||||||||
| Description | The system generates an error when encounters the following code: PTT & 0x10 where PTT is of type (unsigned char*) | ||||||||
| Additional Information | Fixed in Why 2.20 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
virgile (developer) 2009-07-17 14:15 |
operators of bitwise and must have integer type according to C standard (6.5.10.2). You must cast PTT in order to have a correct C construction. Could you provide a complete example exhibiting the error (i.e. on which gcc -c -Wall -std=c99 does not report anything while Frama-C sees an error). |
|
lukaszc (reporter) 2009-07-17 15:23 |
This code: -------------------------------------------------------------------------------- unsigned char * PTT; #define BUTTON_SEL ((int)PTT & 0x10) int main() { if(BUTTON_SEL) ; return 0; } ------------------------------------------------------------------------------- compiles well using gcc -c -Wall -std=c99 (gcc 4.3.3 (Ubuntu 4.3.3-5ubuntu4)). When analysed using frama-c, however, the following error is displayed: ------------------------------------------------------------------------------- test3.c:6: Error: Casting from type struct unsigned_char_P * to type int not allowed Dropping definition of function main ------------------------------------------------------------------------------- Sorry for not being precise (and correct) sufficiently the previous time. |
|
virgile (developer) 2009-07-17 16:12 |
OK. Then this is "normal": arbitrary casts from pointers to integers are not supported by the jessie plugin as for now, its memory model is too abstract for that. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2009-07-14 17:07 | lukaszc | New Issue | |
| 2009-07-17 14:15 | virgile | Note Added: 0000274 | |
| 2009-07-17 14:15 | virgile | Status | new => feedback |
| 2009-07-17 15:23 | lukaszc | Note Added: 0000275 | |
| 2009-07-17 16:12 | virgile | Note Added: 0000276 | |
| 2009-07-17 16:12 | virgile | Status | feedback => confirmed |
| 2009-08-26 11:45 | signoles | Status | confirmed => acknowledged |
| 2009-09-23 16:48 | monate | Status | acknowledged => assigned |
| 2009-09-23 16:48 | monate | Assigned To | => cmarche |
| 2009-09-23 16:51 | signoles | Status | assigned => acknowledged |
| 2009-10-15 10:29 | cmarche | Status | acknowledged => resolved |
| 2009-10-15 10:29 | cmarche | Additional Information Updated | |
| 2009-10-15 12:25 | signoles | Status | resolved => closed |
| 2009-10-15 12:25 | signoles | Fixed in Version | => Frama-C Beryllium 2 |
| 2010-12-09 19:20 | signoles | Resolution | open => fixed |
| 2010-12-09 19:20 | signoles | Additional Information Updated | |
| Issue History |