2021-02-27 11:25 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001141Frama-CKernelpublic2012-09-19 17:16
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityhave not tried
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001141: incorrect UINT8_MAX (and others)
Description[warning: it is a Library problem, but in put in in Kernel Category since there is no Library Category]

#include <stdint.h>

UINT8_MAX expend to ((8)(-1)) which lead to:
[kernel] failure: Unexpected type of the called function 8: int

it comes from:

libc/__fc_machdep.h:#define __umax(typ) ((typ)(-1))
libc/stdint.h:#define UINT8_MAX __umax(8)
TagsNo tags attached.
Attached Files




monate (reporter)

Nice catch: someone at some point "fixed" the three macros, but did not propagate his change to the callers of the macros...
It will be fixed in the next version.


Anne (reporter)


-Issue History
Date Modified Username Field Change
2012-04-04 11:10 Anne New Issue
2012-04-04 16:17 monate Note Added: 0002826
2012-04-04 16:17 monate Assigned To => monate
2012-04-04 16:17 monate Status new => acknowledged
2012-04-04 16:18 Anne Note Added: 0002827
2012-04-06 03:45 monate Status acknowledged => resolved
2012-04-06 03:45 monate Fixed in Version => Frama-C Oxygen-2012xx01
2012-04-06 03:45 monate Resolution open => fixed
2012-09-19 17:16 signoles Status resolved => closed
+Issue History