|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000814||Frama-C||Plug-in > jessie||public||2011-05-09 16:42||2011-10-28 10:39|
|Assigned To||cmarche|| |
|Product Version||Frama-C Carbon-20110201|| |
|Target Version||Fixed in Version||Frama-C Nitrogen-20111001|| |
|Summary||0000814: memory blocks: pointer assignment and equality treated differently|
|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.
|Tags||No tags attached.|
|Attached Files|| ftest.c [^] (262 bytes) 2011-05-09 16:42 [Show Content]