Frama-C Bug Tracking System - Frama-C | ||||||||||
View Issue Details | ||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | |||||
0001750 | Frama-C | Plug-in > wp | public | 2014-04-11 18:50 | 2015-03-17 22:17 | |||||
Reporter | jens | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
Assigned To | patrick | |||||||||
Priority | normal | Severity | minor | Reproducibility | always | |||||
Status | closed | Resolution | fixed | |||||||
Platform | OS | OS Version | ||||||||
Product Version | Frama-C Neon-20140301 | |||||||||
Target Version | Fixed in Version | Frama-C Sodium | ||||||||
Summary | 0001750: Frama-C/WP fails to discharge simple bit operation for small integer types | |||||||||
Description | In the attached file there are for simple functions that computes b = a & 1; //@ assert b == 0 || b == 1; where a and b are of type unsigned char, unsigned short, unsigned int and unsigned long. Only for the types unsigned int and unsigned long cab WP (in fact QED) discharge the assertion. Both alt-ergo and CVC4 fail on unsigned char and unsigned short. I would be very nice if Frama-C/WP could handle the other cases automatically as well. | |||||||||
Tags | No tags attached. | |||||||||
Relationships |
| |||||||||
Attached Files | ![]() https://bts.frama-c.com/file_download.php?file_id=732&type=bug |
Notes | |||||
|
|||||
|
|
||||
|
|||||
|
|
Issue History | |||||
Date Modified | Username | Field | Change | ||
---|---|---|---|---|---|
2014-04-11 18:50 | jens | New Issue | |||
2014-04-11 18:50 | jens | Status | new => assigned | ||
2014-04-11 18:50 | jens | Assigned To | => correnson | ||
2014-04-11 18:50 | jens | File Added: bit_and.c | |||
2014-06-02 16:15 | correnson | Relationship added | related to 0001751 | ||
2014-06-02 16:15 | correnson | Assigned To | correnson => patrick | ||
2014-06-10 12:48 | patrick | Note Added: 0005218 | |||
2014-06-11 11:19 | patrick | Source_changeset_attached | => framac master 959cc69e | ||
2014-06-11 11:19 | patrick | Note Added: 0005221 | |||
2014-06-11 11:19 | patrick | Status | assigned => resolved | ||
2014-06-11 11:19 | patrick | Resolution | open => fixed | ||
2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium | ||
2015-03-17 22:17 | signoles | Status | resolved => closed |