Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000548Frama-CKernelpublic2010-07-25 22:142014-02-12 16:55
Assigned Topascal 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000548: Header limit.h is nonsense
DescriptionHeader limit.h contains macros that cannot be used for anything: $ cat t.c #include main(){ unsigned int x = UINT_MAX; return 0; } $ gcc -C -E -I/Users/pascal/ppc/share/libc/ -o t.i t.c $ cat t.i .. # 2 "t.c" 2 main(){ unsigned int x = (((1 << (4*8))-1))U; return 0; } The above is not syntactically an expression: $ gcc -c t.i t.c: In function ‘main’: t.c:4: warning: left shift count >= width of type t.c:4: error: expected ‘,’ or ‘;’ before ‘U’ $ ~/ppc/bin/toplevel.opt t.i t.c:4:[kernel] user error: syntax error [kernel] user error: skipping file "t.i" that has errors. [kernel] Frama-C aborted because of invalid user input. Gcc's other warning regarding width of type is also a valid point. A low-tech solution would be to define these values as constants within #ifdef MACHDEP_X86, … and to let the user use "gcc -C -E -DMACHDEP_X86" for preprocessing.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
virgile (developer)
2010-08-23 10:15

What about expanding this macro in something like __builtin_uintmax, which could then be treated by the front-end appropriately (keeping the builtin or replacing by its literal value, which will be known at this point through access to Machdep module)?
pascal (reporter)
2010-08-23 14:59

Thinking about it, the __builtin_uintmax proposition seems a little extreme. Surely there must be a way to write an expression that evaluates to the intended value and uses only sizeof(unsigned int) and constants (and does not make up its own syntax) ? In fact, for all types but the largests, it would even be simple: compute in the larger type and cast at the end of the computation. For the maximums of unsigned types, casting -1 works, too. That leaves signed long long and other signed types of the same size, for which the 1<<...-1 trick overflows. For these, we can compute in unsigned long long and cast to signed long long after the subtraction.
virgile (developer)
2010-08-23 18:01

You're right, it would be better not to rely on a Frama-C built-in here, especially as the macros can be used in an #if directive, thus the preprocessor must be able to evaluate them. There are still issues, though: - We're not guaranteed that sizeof(long) < sizeof(long long), are we? An overflow can occur also for long - Being able to handle #if directive imposes to avoid sizeof and casts (Section 6.10 of the standard)

- Issue History
Date Modified Username Field Change
2010-07-25 22:14 pascal New Issue
2010-08-23 10:15 virgile Note Added: 0001078
2010-08-23 14:59 pascal Note Added: 0001082
2010-08-23 18:01 virgile Note Added: 0001083
2010-12-13 06:00 svn Checkin
2010-12-13 06:00 svn Status new => resolved
2010-12-13 06:00 svn Resolution open => fixed
2010-12-13 10:39 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-13 11:48 signoles Assigned To => pascal
2010-12-17 19:35 signoles Status resolved => closed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker