0000472: Comparing a function pointer will NULL might raise incorrect warning - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000472

Frama-C

Plug-in > Eva

public

2010-05-07 12:35

2014-02-12 16:55

Reporter

yakobowski

Assigned To

pascal

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Boron-20100401

Target Version

Fixed in Version

Frama-C Carbon-20101201-beta1

Summary

0000472: Comparing a function pointer will NULL might raise incorrect warning

Description

In the code below, the value analysis flags the comparison of fun with the NULL pointer as requiring a comparability assertion, while a comparison with the NULL pointer is always legal. void f(void); void g(void); extern int j; int main (void) { void (*fun)(void); int* p; if(j) fun = f; else fun = g; if (fun == 0) return 0; else return 1; } (The problem does not appear if 'fun' is a pointer to only one function, or when comparing non-functional pointers.)

Tags

No tags attached.

Relationships

Notes
(0000823) pascal (reporter) 2010-05-10 23:49	"imprecise", not "incorrect".

(0000910) signoles (manager) 2010-06-04 22:24	Fixed by PC yesterday.

Issue History
Date Modified	Username	Field	Change
2010-05-07 12:35	yakobowski	New Issue
2010-05-07 12:35	yakobowski	Status	new => assigned
2010-05-07 12:35	yakobowski	Assigned To	=> pascal
2010-05-10 23:49	pascal	Note Added: 0000823
2010-06-03 19:39	svn	Checkin
2010-06-04 22:24	signoles	Note Added: 0000910
2010-06-04 22:24	signoles	Status	assigned => resolved
2010-06-04 22:24	signoles	Fixed in Version	=> Frama-C Carbon
2010-06-04 22:24	signoles	Resolution	open => fixed
2010-12-17 19:36	signoles	Status	resolved => closed
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2020 MantisBT Team