Frama-C Bug Tracking System - Frama-C
View Issue Details
0000814Frama-CPlug-in > jessiepublic2011-05-09 16:422011-10-28 10:39
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000814: memory blocks: pointer assignment and equality treated differently
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.
No tags attached.
c ftest.c (262) 2011-05-09 16:42
Issue History
2011-05-09 16:42JochenNew Issue
2011-05-09 16:42JochenStatusnew => assigned
2011-05-09 16:42JochenAssigned To => cmarche
2011-05-09 16:42JochenFile Added: ftest.c
2011-05-24 06:54cmarcheNote Added: 0001922
2011-05-24 06:54cmarcheStatusassigned => resolved
2011-05-24 06:54cmarcheResolutionopen => fixed
2011-10-10 14:14signolesStatusresolved => closed
2011-10-10 14:15signolesStatusclosed => resolved
2011-10-28 10:39signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-28 10:39signolesStatusresolved => closed

2011-05-24 06:54   

The bug was in the handling of pointer comparison in annotations, with the region unification of separation analysis

The fix will appear in release 2.30 of Why