Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000885Frama-CKernel > ACSL implementationpublic2011-07-19 13:402014-02-12 16:59
Reporterpatrick 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000885: Typing error on expression array == pointer
DescriptionFile:
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!
TagsNo tags attached.
Attached Files

- 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
Powered by Mantis Bugtracker