Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002356Frama-CPlug-in > clangpublic2018-02-07 07:552018-02-09 10:18
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusconfirmedResolutionopen 
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 file icon generated_member_functions.cpp [^] (194 bytes) 2018-02-07 07:55

- 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.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker