0002356: insufficient contracts for generated constructors and assignment operator(s) - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Reporter

jens

Assigned To

virgile

Priority

normal

Severity

feature

Reproducibility

always

Status

confirmed

Resolution

open

Platform

OS

OS Version

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.

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 - 2019 MantisBT Team