2021-03-02 03:38 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000187Frama-CPlug-in > jessiepublic2010-12-09 19:20
Assigned Tocmarche 
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




virgile (developer)

operators of bitwise and must have integer type according to C standard ( 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)

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)

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
+Issue History