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

Attachments

• generated_member_functions.cpp