Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1276

Closed
Open
Created Apr 11, 2011 by Pascal Cuoq@pascal

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)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking