Frama-C/WP fails to discharge simple bit operation for small integer types
ID0001750: This issue was created automatically from Mantis Issue 1750. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001750 | Frama-C | Plug-in > wp | public | 2014-04-11 | 2015-03-17 |
| Reporter | jens | Assigned To | patrick | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | Frama-C Sodium |
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.