| Anonymous | Login | Signup for a new account | This BTS is being migrated to Gitlab, consider using those issues instead |  |
| 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 | |||||||||
 Relationships |
|
 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. |
|
Notes |
|
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 |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|