Frama-C Bug Tracking System - Frama-C
View Issue Details
0002356Frama-CPlug-in > clangpublic2018-02-07 07:552018-02-09 10:18
Assigned Tovirgile 
PlatformOSOS Version
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 Filescpp generated_member_functions.cpp (194) 2018-02-07 07:55

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
2018-02-09 10:18   
Just for the sake of completeness, it's not just postconditions but also assigns clauses.

Issue History
2018-02-07 07:55jensNew Issue
2018-02-07 07:55jensStatusnew => assigned
2018-02-07 07:55jensAssigned To => virgile
2018-02-07 07:55jensFile Added: generated_member_functions.cpp
2018-02-07 10:31virgileNote Added: 0006522
2018-02-07 10:31virgileSeverityminor => feature
2018-02-07 10:31virgileStatusassigned => confirmed
2018-02-09 10:18jensNote Added: 0006528