Frama-C Bug Tracking System

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 - 2018 MantisBT Team
Powered by Mantis Bugtracker