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
Reporterpascal 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 <limits.h>

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
(0001078)
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)?
(0001082)
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.
(0001083)
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 - 2017 MantisBT Team
Powered by Mantis Bugtracker