0000885: Typing error on expression array == pointer - 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

0000885

Frama-C

Kernel > ACSL implementation

public

2011-07-19 13:40

2014-02-12 16:59

Reporter

patrick

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Carbon-20110201

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000885: Typing error on expression array == pointer

Description

File:
extern int t1[10];
//@ requires t1 == \null;
void main(void) { ; }

is interpreted as:

extern int t1[10];
//@ requires (int *)t1 == (int []) \null;
void main(void) { ; }

Both operands of the equality have not the same type!

Tags

No tags attached.

Relationships

Notes
(0002032) patrick (developer) 2011-07-19 13:45	I think that t1 expression cannot be implicitly casted into a pointer (from ACSL reference manual). I don't remember if implicit cast from pointer to array are allowed. If it is not the case, the equality t1 == \null should be rejected by Frama-C.

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

Issue History
Date Modified	Username	Field	Change
2011-07-19 13:40	patrick	New Issue
2011-07-19 13:40	patrick	Status	new => assigned
2011-07-19 13:40	patrick	Assigned To	=> virgile
2011-07-19 13:41	virgile	Status	assigned => acknowledged
2011-07-19 13:45	patrick	Note Added: 0002032
2011-07-22 10:15	svn	Checkin
2011-07-22 10:15	svn	Status	acknowledged => resolved
2011-07-22 10:15	svn	Resolution	open => fixed
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed
2014-02-12 16:59		Note Added: 0004762
2014-02-12 16:59		Status	closed => resolved

Copyright © 2000 - 2017 MantisBT Team