|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001907||Frama-C||Plug-in > Eva||public||2014-08-08 14:17||2015-03-17 22:18|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|Target Version||Fixed in Version||Frama-C Sodium|
|Summary||0001907: Value abort because of Zero-sized location|
|Description||Value 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.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|
|Tags||No tags attached.|
|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.|
|I have many of those in the application I am analyzing, and it is usually working pretty well... except this external variable problem.|
|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.|
|Fix committed to master branch.|
|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|