Frama-C Bug Tracking System - Frama-C
View Issue Details
0000885Frama-CKernel > ACSL implementationpublic2011-07-19 13:402014-02-12 16:59
patrick 
virgile 
normalminorhave not tried
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000885: Typing error on expression array == pointer
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!
No tags attached.
Issue History
2011-07-19 13:40patrickNew Issue
2011-07-19 13:40patrickStatusnew => assigned
2011-07-19 13:40patrickAssigned To => virgile
2011-07-19 13:41virgileStatusassigned => acknowledged
2011-07-19 13:45patrickNote Added: 0002032
2011-07-22 10:15svnCheckin
2011-07-22 10:15svnStatusacknowledged => resolved
2011-07-22 10:15svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004762
2014-02-12 16:59Statusclosed => resolved

Notes
(0002032)
patrick   
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.