Frama-C Bug Tracking System - Frama-C | ||||||||||
| View Issue Details | ||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | |||||
| 0000890 | Frama-C | Plug-in > Eva | public | 2011-07-25 18:02 | 2014-02-12 16:59 | |||||
| Reporter | monate | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| Assigned To | pascal | |||||||||
| Priority | normal | Severity | major | 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 | 0000890: Results differ between value analysis and GCC on bitfields | |||||||||
| Description | On the program ==bug.i============== union U0 { unsigned short f0 ; int f1 ; int f2 : 5 ; unsigned char const f3 ; }; unsigned short G0 ; int G1 ; int G2; unsigned char G3 ; union U0 G={(unsigned short)65532U}; int main() { G0=G.f0; G1=G.f1; G2=G.f2; G3=G.f3; printf("%d %d %d %d : %d\n",G0,G1,G2,G3,G2==-4); return (G2==-4); } ========================= frama-c -val bug.i returns: === [value] Values for function main: G0 ? {65532} G1[bits 0 to 15] ? {65532} [bits 16 to 31] ? {0} G2 ? {28} G3# ? {65532} misaligned 0%16 __retres ? {0} === but gcc bug.i && ./a.out ; echo $? displays : === 65532 65532 -4 252 : 1 1 === They do not agree on the result nor on the value of G2. | |||||||||
| Tags | No tags attached. | |||||||||
| Relationships |
| |||||||||
| Attached Files | ||||||||||
| Notes | |||||
|
|
|||||
|
|
||||
| Issue History | |||||
| Date Modified | Username | Field | Change | ||
|---|---|---|---|---|---|
| 2011-07-25 18:02 | monate | New Issue | |||
| 2011-07-25 18:02 | monate | Status | new => assigned | ||
| 2011-07-25 18:02 | monate | Assigned To | => pascal | ||
| 2011-07-25 18:03 | monate | Relationship added | parent of 0000871 | ||
| 2011-07-25 23:40 | svn | ||||
| 2011-07-25 23:40 | svn | Status | assigned => resolved | ||
| 2011-07-25 23:40 | 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 | ||
| 2013-12-19 01:12 | pascal | Source_changeset_attached | => framac master 8ead7999 | ||
| 2014-02-12 16:54 | pascal | Source_changeset_attached | => framac stable/neon 8ead7999 | ||
| 2014-02-12 16:59 | pascal | Note Added: 0004761 | |||
| 2014-02-12 16:59 | pascal | Status | closed => resolved | ||
| 2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva | ||