View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
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 | ||||||
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. | ||||||||
Attached Files |
|
![]() |
|
pascal (reporter) 2011-05-12 18:56 Last edited: 2011-05-12 18:56 |
You have forgotten "unsigned" before "bitfields which have a size equal to the size of int" in your commit message. Unfortunately, you have also forgotten to handle signed 32-bit bitfields in your patch. Try the following : Manzana:~ pascal$ ~/ppc/bin/toplevel.byte -val t.c ... [value] Values for function main: r ? {1} Manzana:~ pascal$ gcc t.c Manzana:~ pascal$ ./a.out 0 Manzana:~ pascal$ clang t.c t.c:7:1: warning: type specifier missing, defaults to 'int' [-Wimplicit-int] main(){ ^ 1 warning generated. Manzana:~ pascal$ ./a.out 0 Manzana:~ pascal$ cat t.c #include <stdio.h> struct S { signed f:32; } x = { 28349}; unsigned short us = 0xDC23L; main(){ int r = (x.f ^ ((short)-87)) >= us; printf("%d\n", r); return r; } |
monate (reporter) 2014-02-12 16:59 |
Fix committed to stable/neon branch. |
![]() |
|||
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 |