0000785: 12799, doubtful choice of promotion x86_64 mode (csmith)

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

Notes
(0004805) pascal (reporter) 2014-02-12 16:59	Fix committed to stable/neon branch.

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	Checkin
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
2014-02-12 16:59	pascal	Note Added: 0004805
2014-02-12 16:59	pascal	Status	closed => resolved