C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

I think 0 is the correct result.  The unsigned bitfield can only represent values 0 and 1, so it should get promoted to a signed int (n1570, 6.3.1.1:2) "If an int can represent all values of the original type (as restricted by the width, for a bit-field), the value is converted to an int".  This means you effectively (int)-3 >= (int)0, so there is no conversion necessary.  -3 >= 0 is false.

It looks like ICC is getting confused with the comma operator.  Changing (0,  g_791.f2.f1) to  g_791.f2.f1 causes ICC to return 0 as well.  The result of the comma operator is supposed to have the type and value of the right operand, so I don't see how this could affect the result.

Fun catch John!

-Chucky

On Tue, Jul 12, 2011 at 2:59 PM, John Regehr <regehr AT cs.utah.edu> wrote:

CompCert gives 0, MSVC gives 1.  The vote is still split.  Help! :)

John

On 07/12/2011 01:56 PM, John Regehr wrote:
> GCC and KCC give one answer, ICC and Clang give another -- all with
> optimizations disabled.  Can any of the C experts here tell me who is wrong?
>
> I'm pretty sure the test case is well-defined (but never 100% sure with
> this kind of thing).
>
> John
>
>
>
> [regehr@babel ~]$ cat small.c
> int printf (const char *, ...);
>
> struct S0
> {
>     unsigned f1:1;
> };
>
> struct S2
> {
>     struct S0 f2;
> };
>
> struct S2 g_791;
>
> int main (void)
> {
>     int l_45 = -3;
>     int t = l_45>= (0, g_791.f2.f1);
>     printf ("%d\n", t);
>     return 0;
> }
> [regehr@babel ~]$ gcc small.c
> [regehr@babel ~]$ ./a.out
> 0
> [regehr@babel ~]$ kcc small.c
> [regehr@babel ~]$ ./a.out
> 0
> [regehr@babel ~]$ clang small.c
> small.c:18:20: warning: _expression_ result unused [-Wunused-value]
>     int t = l_45>= (0, g_791.f2.f1);
>                      ^
> 1 warning generated.
> [regehr@babel ~]$ ./a.out
> 1
> [regehr@babel ~]$ icc small.c
> [regehr@babel ~]$ ./a.out
> 1
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>
_______________________________________________
c-semantics mailing list
c-semantics AT cs.illinois.edu
http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics