insufficient contracts for generated constructors and assignment operator(s)
ID0002356: This issue was created automatically from Mantis Issue 2356. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002356 | Frama-C | Plug-in > clang | public | 2018-02-07 | 2018-02-09 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | - |
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.cppthen 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.