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); }