Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000443Frama-CPlug-in > jessiepublic2010-04-06 16:552010-04-19 16:14
ReporterJochen 
Assigned Tocmarche 
PriorityurgentSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFrama-C Boron-20100401Fixed in VersionFrama-C Boron-20100401 
Summary0000443: assigns clause unchecked on arrays
DescriptionWhile a write-access to a simple variable (int a) is recognized to violate an assigns-clause, a similar access to an array variable (int a[1]) is not.

No proof obligation is generated in the latter case.

See attached file; uncomment / comment-out the #define to demonstrate the different behaviors.

I tried jessie only without the option "-jessie-no-regions".
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (209 bytes) 2010-04-06 16:55 [Show Content]

- Relationships

-  Notes
(0000756)
cmarche (developer)
2010-04-08 16:53

Fixed in current SVN of Why.

The fix exposes another bug when adress of a local variable is taken (see ref.c dillon1.c, dillon3.c), where an incorrect Why program is now generated.

The fix is preferable than nothing, because the original bug was a major one.


(0000774)
signoles (manager)
2010-04-19 16:14

Fix in Why 2.24 (require Frama-C Boron-20100401).

- Issue History
Date Modified Username Field Change
2010-04-06 16:55 Jochen New Issue
2010-04-06 16:55 Jochen Status new => assigned
2010-04-06 16:55 Jochen Assigned To => cmarche
2010-04-06 16:55 Jochen File Added: ftest.c
2010-04-08 13:01 cmarche Priority normal => urgent
2010-04-08 14:28 cmarche Assigned To cmarche =>
2010-04-08 14:30 cmarche Assigned To => cmarche
2010-04-08 14:30 cmarche Target Version => Frama-C Boron
2010-04-08 16:53 cmarche Note Added: 0000756
2010-04-08 16:53 cmarche Status assigned => resolved
2010-04-08 16:53 cmarche Resolution open => fixed
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000774


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker