Frama-C/Jessie does not recognize the length of array in struct
ID0000628: This issue was created automatically from Mantis Issue 628. Further discussion may take place here.
|ID0000628||Frama-C||Plug-in > jessie||public||2010-11-13||2017-03-14|
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||-|
The assertion in the attached file cannot be proved by any atp. I suppose it's because Frama-C/Jessie does not recognize the length of an array in a struct. As this kind of code is normal for embedded applications it should be supported by Frama-C.