0001360: \valid_read and assigns - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0001360

Frama-C

Plug-in > wp

public

2013-02-08 20:44

2014-02-12 16:58

Reporter

jens

Assigned To

correnson

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Oxygen-20120901

Target Version

Fixed in Version

Frama-C Fluorine-20130401

Summary

0001360: \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"?

Tags

No tags attached.

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