Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000814Frama-CPlug-in > jessiepublic2011-05-09 16:422011-10-28 10:39
Assigned Tocmarche 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000814: memory blocks: pointer assignment and equality treated differently
DescriptionThe 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.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (262 bytes) 2011-05-09 16:42 [Show Content]

- Relationships

-  Notes
cmarche (developer)
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

- Issue History
Date Modified Username Field Change
2011-05-09 16:42 Jochen New Issue
2011-05-09 16:42 Jochen Status new => assigned
2011-05-09 16:42 Jochen Assigned To => cmarche
2011-05-09 16:42 Jochen File Added: ftest.c
2011-05-24 06:54 cmarche Note Added: 0001922
2011-05-24 06:54 cmarche Status assigned => resolved
2011-05-24 06:54 cmarche Resolution open => fixed
2011-10-10 14:14 signoles Status resolved => closed
2011-10-10 14:15 signoles Status closed => resolved
2011-10-28 10:39 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-28 10:39 signoles Status resolved => closed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker