| 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 ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
| 0002356 | Frama-C | Plug-in > clang | public | 2018-02-07 07:55 | 2018-02-09 10:18 | ||||||||
| Reporter | jens | ||||||||||||
| Assigned To | virgile | ||||||||||||
| Priority | normal | Severity | feature | Reproducibility | always | ||||||||
| Status | confirmed | Resolution | open | ||||||||||
| Platform | OS | OS Version | |||||||||||
| Product Version | Frama-C 16-Sulfur | ||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0002356: insufficient contracts for generated constructors and assignment operator(s) | ||||||||||||
| Description | The attached file contains a very simple class (struct). It is used in simple copy initialization and assignment operations. When called with with frama-c-gui -wp -wp-rte generated_member_functions.cpp then the two assertions are not verified by Fram-Clang/WP. From what I see about the contracts of the generated constructors and assignment operator(s), this is not surprising because their postconditions do not refer to the member 'n'. EVA seems to work just fine. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |  generated_member_functions.cpp [^] (194 bytes) 2018-02-07 07:55 | ||||||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0006522) virgile (developer) 2018-02-07 10:31 |
Indeed, generated constructors do not have a generated contract (other than the default \valid(this) requires). Since we're already generating the body, having some ensures in addition should be doable |
|
(0006528) jens (reporter) 2018-02-09 10:18 |
Just for the sake of completeness, it's not just postconditions but also assigns clauses. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2018-02-07 07:55 | jens | New Issue | |
| 2018-02-07 07:55 | jens | Status | new => assigned |
| 2018-02-07 07:55 | jens | Assigned To | => virgile |
| 2018-02-07 07:55 | jens | File Added: generated_member_functions.cpp | |
| 2018-02-07 10:31 | virgile | Note Added: 0006522 | |
| 2018-02-07 10:31 | virgile | Severity | minor => feature |
| 2018-02-07 10:31 | virgile | Status | assigned => confirmed |
| 2018-02-09 10:18 | jens | Note Added: 0006528 | |
|
Issue History |
| Copyright © 2000 - 2020 MantisBT Team |
|