Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000261Frama-CKernelpublic2009-10-01 02:502009-10-01 14:58
ReporterJonathan-Christofer Demay 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in Version 
Summary0000261: Frama-C fails to parse a file
DescriptionIt compiles fine with "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -c -o dbutil.o"

But when given to Frama-C (CPP is set accordinly), I get the following error:
libtommath/tommath.h:77:[kernel] user error: GCC width mode TI applied to unexpected type, or unexpected mode

In tommath.h line 77 we have a mysterious GCC incantation (>_<):
typedef unsigned long mp_word __attribute__ ((mode(TI)));
Additional InformationUploaded a preprocessed file: "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -C -E -o dbutil.i"
TagsNo tags attached.
Attached Files? file icon dbutil.i [^] (795,104 bytes) 2009-10-01 02:50

- Relationships

-  Notes
(0000427)
virgile (developer)
2009-10-01 10:06

those gcc attributes are very scarsely documented. The best pointer I've found so far is here:
http://gcc.gnu.org/onlinedocs/gccint/Machine-Modes.html#Machine-Modes [^]
(0000428)
Jonathan-Christofer Demay (reporter)
2009-10-01 14:58

I did end up at the same web page, I guess the idea was to define a 128-bits unsigned integer. I tried to replace it with __uint128_t but since it's a gcc internal and it is not defined in any .h file, Frama-C didn't like it either.

However, both 'mode(TI)' and '__uint128_t' are only accessible through a 64-bits gcc, so I guess I'm back to 32-bits for now.

- Issue History
Date Modified Username Field Change
2009-10-01 02:50 Jonathan-Christofer Demay New Issue
2009-10-01 02:50 Jonathan-Christofer Demay File Added: dbutil.i
2009-10-01 09:34 signoles Status new => assigned
2009-10-01 09:34 signoles Assigned To => virgile
2009-10-01 10:06 virgile Note Added: 0000427
2009-10-01 10:06 virgile Status assigned => acknowledged
2009-10-01 14:58 Jonathan-Christofer Demay Note Added: 0000428


Copyright © 2000 - 2016 MantisBT Team
Powered by Mantis Bugtracker