0000999: Missing or misleading warnings when merging two functions

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000999

Frama-C

Kernel

public

2011-10-24 13:16

2014-02-12 16:59

Reporter

yakobowski

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Nitrogen-20111001

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0000999: Missing or misleading warnings when merging two functions

Description

frama-c does not complain in the right way when parsing the following code:
- there is no warning for the types, even though the return types are not compatible
- the warning "found two default behaviors, merging them" is not really intuitive for the user, as he has not written "behavior" anywhere.

//@ assigns \nothing;
int foo(int* p);

//@ ensures 0 <= \result < 25;
unsigned short foo()
{
return 0;
}

Tags

No tags attached.

Attached Files

Relationships

Notes
(0004718) 2014-02-12 16:59	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2011-10-24 13:16	yakobowski	New Issue
2011-10-24 13:46	yakobowski	Status	new => assigned
2011-10-24 13:46	yakobowski	Assigned To	=> virgile
2011-10-27 20:35	svn	Checkin
2011-10-27 20:35	svn	Status	assigned => resolved
2011-10-27 20:35	svn	Resolution	open => fixed
2012-09-19 17:15	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2012-09-19 17:16	signoles	Status	resolved => closed
2014-02-12 16:59		Note Added: 0004718
2014-02-12 16:59		Status	closed => resolved