2021-01-15 16:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001907Frama-CPlug-in > Evapublic2015-03-17 22:18
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
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.

* 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 +




yakobowski (manager)

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.


Anne (reporter)

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


yakobowski (manager)

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.


yakobowski (manager)

Fix committed to master branch.

-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