Anonymous | Login | Signup for a new account | 2019-02-18 16:36 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
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 | ||||||
Platform | OS | OS Version | |||||||
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 | |||||||||
![]() |
|
(0000274) 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). |
(0000275) 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. |
(0000276) 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. |
![]() |
|||
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 |
Copyright © 2000 - 2019 MantisBT Team |