|View Issue Details|
|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|
|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.|
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
|Just for the sake of completeness, it's not just postconditions but also assigns clauses.|
|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|