| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000785 | Frama-C | Kernel | public | 2011-04-11 16:17 | 2014-02-12 16:59 | ||||
| Reporter | pascal | ||||||||
| Assigned To | pascal | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000785: 12799, doubtful choice of promotion x86_64 mode (csmith) | ||||||||
| Description | int x; long x2; unsigned long x9[6][2]; #if 0 #define d(n, v) Frama_C_show_each##n(v); #else #define d(n, v) #endif main(){ x2 = 2793414595; for (int i = 0; i < 6; i++) { for (int j = 0; j < 2; j++) x9[i][j] = 1U; } d(102, (0x090E7AF82577C8A6LL | x9[1][0]) ) d(103, (~(x2 || x9[1][0])) ) d(95, ((0x090E7AF82577C8A6LL | x9[0][1]) <= (~(x2 || x9[0][1])))) x = ((0x090E7AF82577C8A6LL | x9[0][1]) <= (~(x2 || x9[0][1]))); return x; } ~/ppc/bin/toplevel.opt -val -machdep x86_64 r.c -slevel 5000 ... [value] Values for function main: x ? {0; } BUT: gcc -std=c99 r.c ; ./a.out ; echo $? 1 NOTE THAT: ~/ppc/bin/toplevel.opt -print -machdep x86_64 r.c [kernel] preprocessing with "gcc -C -E -I. r.c" ... x = (0x090E7AF82577C8A6LL | (long long )x9[0][1]) <= (long long )(~ tmp); } return (x); } gcc is the computation server's, supposed to match x86_64. x9[0][1] is an unsigned long. The promotion of the arguments of | seems to be wrong in Frama-C's front-end according to 6.3.1.8 (p 45), where the very last case of ยง1 seems to apply. | ||||||||
| Additional Information | In addition to the computation server's GCC (version 4.4.3 (Ubuntu 4.4.3-4ubuntu5)), this one also predicts the result 1 for x when compiling with -m64: gcc -m64 -v Using built-in specs. Target: powerpc-apple-darwin9 Configured with: /var/tmp/gcc/gcc-5493~1/src/configure --disable-checking -enable-werror --prefix=/usr --mandir=/share/man --enable-languages=c,objc,c++,obj-c++ --program-transform-name=/^[cg][^.-]*$/s/$/-4.0/ --with-gxx-include-dir=/include/c++/4.0.0 --with-slibdir=/usr/lib --build=i686-apple-darwin9 --program-prefix= --host=powerpc-apple-darwin9 --target=powerpc-apple-darwin9 Thread model: posix gcc version 4.0.1 (Apple Inc. build 5493) | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-04-11 16:17 | pascal | New Issue | |
| 2011-04-11 16:33 | pascal | Additional Information Updated | |
| 2011-04-15 18:40 | pascal | Status | new => assigned |
| 2011-04-15 18:40 | pascal | Assigned To | => pascal |
| 2011-04-15 18:48 | svn | ||
| 2011-04-15 18:48 | svn | Status | assigned => resolved |
| 2011-04-15 18:48 | svn | Resolution | open => fixed |
| 2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
| 2011-10-10 14:14 | signoles | Status | resolved => closed |
| 2013-12-19 01:12 | pascal | Source_changeset_attached | => framac master 13c2b436 |
| 2014-02-12 16:54 | pascal | Source_changeset_attached | => framac stable/neon 13c2b436 |
| 2014-02-12 16:59 | pascal | Note Added: 0004805 | |
| 2014-02-12 16:59 | pascal | Status | closed => resolved |
| Issue History |