|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000548||Frama-C||Kernel||public||2010-07-25 22:14||2014-02-12 16:55|
|Product Version||Frama-C Boron-20100401|
|Target Version||Fixed in Version||Frama-C Carbon-20101201-beta1|
|Summary||0000548: Header limit.h is nonsense|
|Description||Header limit.h contains macros that cannot be used for anything:|
$ cat t.c
unsigned int x = UINT_MAX;
$ gcc -C -E -I/Users/pascal/ppc/share/libc/ -o t.i t.c
$ cat t.i
# 2 "t.c" 2
unsigned int x = (((1 << (4*8))-1))U;
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.
|Tags||No tags attached.|
|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)?|
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.
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)
|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||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|
|2013-12-19 01:12||pascal||Source_changeset_attached||=> framac master 366cb7be|
|2014-02-12 16:55||pascal||Source_changeset_attached||=> framac stable/neon 366cb7be|