2021-03-01 05:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000885Frama-CKernel > ACSL implementationpublic2014-02-12 16:59
Reporterpatrick 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0002032

patrick (developer)

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

Fix committed to stable/neon branch.
+Notes

-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
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
2013-12-19 01:12 Source_changeset_attached => framac master b4bd1c37
2014-02-12 16:54 Source_changeset_attached => framac stable/neon b4bd1c37
2014-02-12 16:59 Note Added: 0004762
2014-02-12 16:59 Status closed => resolved
+Issue History