Missing rte guard when assigning an unsigned int to an int
ID0001766: This issue was created automatically from Mantis Issue 1766. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001766 | Frama-C | Plug-in > RTE | public | 2014-04-30 | 2014-05-19 |
| Reporter | jens | Assigned To | signoles | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | Linux | OS Version | ubuntu 3.13 |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
The following function assigns the unsigned int variable "a" to the int variable "b". I do not see any generated rte assertions to guard this operation. The C standard says in 6.3.1.3.3 about this kind of operation
Otherwise, the new type is signed and the value cannot be represented in it; either the result is implementation-defined or an implementation-defined signal is raised.
On the other hand, for the operation involving "a" and "x", proper rte guards are generated.
/*@ requires \valid(x); assigns *x; / int f(unsigned int a, unsigned int x) { *x = a + a; int b = a; return b; }