Incorrect overflow and cast assertions for bitfields
ID0002314: This issue was created automatically from Mantis Issue 2314. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002314 | Frama-C | Plug-in > RTE | public | 2017-06-26 | 2017-12-29 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
The following snippet: struct STR { int num : 7; };
void foo(int a, long b) { struct STR s = { .num = 0 }; s.num = b; s.num += a; }
generates the following assertions /*@ assert rte: signed_downcast: b ≤ 2147483647; / /@ assert rte: signed_downcast: -2147483648 ≤ b; / s.num = (int)b; /@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; / /@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */ s.num = (int)((int)s.num + a);
The limits for s.num are incorrect, since s.num is a bitfield of 7 bits its limits should be [-64, 63]
Steps To Reproduce :
frama-c -machdep x86_64 file.c -rte -warn-signed-overflow -warn-signed-downcast -print