Hex/octal signed constants can be represented in an unsigned extended integer type (csmith)
ID0000775: This issue was created automatically from Mantis Issue 775. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000775 | Frama-C | Kernel | public | 2011-03-31 | 2014-02-12 |
| Reporter | pascal | Assigned To | monate | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
main(){ int r = 0xE2DB80EBBD4856CDLL >= 1; return r; }
This program, when compiled with GCC, returns 1. This is in accordance to page 56 of the C99 standard, where octal/hexadecimal LL constants can be represented as unsigned long long int when they do not fit inside a long long int.
However the front-end types the program wrongly, leading the value analysis to believe the return value is 0:
~/ppc/bin/toplevel.opt -val u.c -print
[value] Values for function main: r ? {0; } /* Generated by Frama-C */ int main(void) { int r ; r = 0xE2DB80EBBD4856CDLL >= (long long )1; return (r); }