12799, doubtful choice of promotion x86_64 mode (csmith)
ID0000785: This issue was created automatically from Mantis Issue 785. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000785 | Frama-C | Kernel | public | 2011-04-11 | 2014-02-12 |
| Reporter | pascal | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
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)