Anonymous | Login | Signup for a new account | 2019-12-14 07:03 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
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. | ||||||||
Attached Files | |||||||||
![]() |
|
(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. |
![]() |
|||
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 |