2021-01-22 20:38 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002356Frama-CPlug-in > clangpublic2018-02-09 10:18
Assigned Tovirgile 
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002356: insufficient contracts for generated constructors and assignment operator(s)
DescriptionThe 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.
TagsNo tags attached.
Attached Files




virgile (developer)

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


jens (reporter)

Just for the sake of completeness, it's not just postconditions but also assigns clauses.

-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