2021-02-24 18:56 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000548Frama-CKernelpublic2014-02-12 16:55
Assigned Topascal 
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 <limits.h>

  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

  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




virgile (developer)

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)

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)

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