Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001360Frama-CPlug-in > wppublic2013-02-08 20:442014-02-12 16:58
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001360: \valid_read and assigns
Description In the following specification I have deliberately used "\valid_read" instead of of "\valid". /*@ requires \valid_read(a); ensures *a == 0; assigns *a; */ void foo(int* a) { *a = 0; } Frama-C/WP verifies this specification and implementation. However, isn't it wrong that 1.) the assigns clause of the specification refers to a memory location that is not "\valid" but only "\valid_read"? 2.) the implementation writes to a memory location that is not "\valid"?
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0003715)
correnson (manager)
2013-02-27 16:46

 There are two different issues with this program : 1. Assignment to a non-valid-write pointer 2. Checking the assigns clause The first point is currently not handled by WP. You need, say, RTE. Indeed, frama-c -wp -wp-rte SHOULD fails on this program. It DOES NOT fail as expected in the last public release. The second point about assigns can be non-intuitive. However, the assigns clauses claims that, no valid region outside { *a } have been modified. That means : \forall p, \valid(p) -> \separated(p,a) -> *p == \old(*p). Indeed, the program IS correct w.r.t its assigns contract ! Actually, if a program DO NOT assigns (*a), it stills validates the contract "assigns *a". There is bug in checking for \valid_read instead of \valid. And probably WP should check assigned code for \valid, without RTE.
(0004589)
correnson (manager)
2014-02-12 16:58

 Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-02-08 20:44 jens New Issue
2013-02-08 20:44 jens Status new => assigned
2013-02-08 20:44 jens Assigned To => correnson
2013-02-27 16:46 correnson Note Added: 0003715
2013-02-27 16:49 svn Checkin
2013-02-27 16:49 svn Status assigned => resolved
2013-02-27 16:49 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2014-02-12 16:58 correnson Note Added: 0004589
2014-02-12 16:58 correnson Status closed => resolved

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker