Frama-C Bug Tracking System - Frama-C | |||||
View Issue Details | |||||
ID | Project | Category | View Status | Date Submitted | Last Update |
0000823 | Frama-C | Kernel | public | 2011-05-12 14:29 | 2014-02-12 16:59 |
Reporter | pascal | ||||
---|---|---|---|---|---|
Assigned To | monate | ||||
Priority | normal | Severity | minor | Reproducibility | always |
Status | closed | Resolution | fixed | ||
Platform | OS | OS Version | |||
Product Version | Frama-C GIT, precise the release id | ||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||
Summary | 0000823: r13417 unsigned bit-fields of width 32 should be promoted to unsigned int (csmith) | ||||
Description | #include <stdio.h> struct S { unsigned f:32; } x = { 28349}; unsigned short us = 0xDC23L; main(){ int r = (x.f ^ ((short)-87)) >= us; printf("%d\n", r); return r; } gcc w.c && ./a.out 1 But: ~/ppc/bin/toplevel.opt -print w.c | grep -v preprocessing > w2.c && gcc w2.c && ./a.out 0 The front-end is correct in typing unsigned bit-fields as int most of the time, but there should be an exception for unsigned bit-fields of size 32. See http://stackoverflow.com/q/5977456/139746 | ||||
Tags | No tags attached. | ||||
Relationships | |||||
Attached Files |
Notes | |||||
|
|||||
|
|
||||
|
|||||
|
|
Issue History | |||||
Date Modified | Username | Field | Change | ||
---|---|---|---|---|---|
2011-05-12 14:29 | pascal | New Issue | |||
2011-05-12 14:30 | pascal | Status | new => assigned | ||
2011-05-12 14:30 | pascal | Assigned To | => monate | ||
2011-05-12 15:31 | svn | ||||
2011-05-12 15:31 | svn | Status | assigned => resolved | ||
2011-05-12 15:31 | svn | Resolution | open => fixed | ||
2011-05-12 18:56 | pascal | Note Added: 0001877 | |||
2011-05-12 18:56 | pascal | Status | resolved => feedback | ||
2011-05-12 18:56 | pascal | Resolution | fixed => reopened | ||
2011-05-12 18:56 | pascal | Note Edited: 0001877 | |||
2011-05-12 18:57 | pascal | Status | feedback => confirmed | ||
2011-05-13 15:23 | svn | ||||
2011-05-13 16:14 | monate | Status | confirmed => resolved | ||
2011-05-13 16:14 | monate | Resolution | reopened => 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 | svn | Source_changeset_attached | => framac master 5ac9203a | ||
2013-12-19 01:12 | svn | Source_changeset_attached | => framac master 8b0d56b2 | ||
2014-02-12 16:54 | monate | Source_changeset_attached | => framac stable/neon 5ac9203a | ||
2014-02-12 16:54 | monate | Source_changeset_attached | => framac stable/neon 8b0d56b2 | ||
2014-02-12 16:59 | monate | Note Added: 0004791 | |||
2014-02-12 16:59 | monate | Status | closed => resolved |