memory blocks: pointer assignment and equality treated differently
ID0000814: This issue was created automatically from Mantis Issue 814. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000814 | Frama-C | Plug-in > jessie | public | 2011-05-09 | 2011-10-28 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
The attached program establishes one pointer equality (viz. src==asg) by assignment and another one (viz. src==eql) by equality-requirement. I'd expect that both equalities imply corresponding properties. However, the first one is translated using the same memory block (viz. "int_P_int_M_asg_1") for both pointers, while the second one uses different blocks (viz. "int_P_int_M_asg_1" and "int_P_int_M_eql_3"). Consequently, validity can be proven in line 8, but not in line 9, and contents equality can be proven in line 10, but not in line 11. This issue is relevant only for SeparationPolicy regions.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information