2021-01-15 16:10 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001907Frama-CPlug-in > Evapublic2014-08-08 14:172015-03-17 22:18
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001907: Value abort because of Zero-sized location
DescriptionValue usually support structure types holding an array field with an undefined size, but in the attached case, it aborts with:

    user error: Zero-sized location S_buf[0].chunk (type 'int []').
                Probably empty struct.
                Aborting

* Notice that the size of `buf` is defined since it is only a pointer.
* If `buf` is defined instead of just declared `extern`, the problem disappear.
Steps To Reproduce$ frama-c -val struct.c
TagsNo tags attached.
Attached Files
  • c file icon struct.c (155 bytes) 2014-08-08 14:17 - 
    typedef struct {
   unsigned int chunkCount;
   int chunk[];
} ChunkedBuffer;

extern ChunkedBuffer * buf;

int main (void) {
  return buf->chunkCount;
}
    c file icon struct.c (155 bytes) 2014-08-08 14:17 +

-Relationships
+Relationships

-Notes

~0005401

yakobowski (manager)

2014-08-08 14:25

 Thank. I was probably a bit over-zealous in fixing 1874, and will look into this. No guarantee, as this is a flexible member array, that are more or less unsupported by Value at the moment.

~0005402

Anne (reporter)

2014-08-08 14:32

 I have many of those in the application I am analyzing, and it is usually working pretty well... except this external variable problem.

~0005403

yakobowski (manager)

2014-08-08 14:35

 Because this is one is external, it is treated as if -lib-entry was enabled. In this mode, we fail when trying to feel the unknown size array.

~0005405

yakobowski (manager)

2014-08-10 21:27

 Fix committed to master branch.
+Notes

-Issue History
Date Modified Username Field Change
2014-08-08 14:17 Anne New Issue
2014-08-08 14:17 Anne Status new => assigned
2014-08-08 14:17 Anne Assigned To => yakobowski
2014-08-08 14:17 Anne File Added: struct.c
2014-08-08 14:25 yakobowski Note Added: 0005401
2014-08-08 14:32 Anne Note Added: 0005402
2014-08-08 14:35 yakobowski Note Added: 0005403
2014-08-10 21:27 yakobowski Source_changeset_attached => framac master c8dfa50c
2014-08-10 21:27 yakobowski Note Added: 0005405
2014-08-10 21:27 yakobowski Status assigned => resolved
2014-08-10 21:27 yakobowski Resolution open => fixed
2015-01-28 18:08 Lau Tag Attached: struct
2015-01-28 18:08 Lau Tag Detached: struct
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History