Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000187Frama-CPlug-in > jessiepublic2009-07-14 17:072010-12-09 19:20
Reporterlukaszc 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000187: Error while processing legitimate C construction
DescriptionThe system generates an error when encounters the following code:

PTT & 0x10

where PTT is of type (unsigned char*)
Additional InformationFixed in Why 2.20
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(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.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker