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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000628 | Frama-C | Plug-in > jessie | public | 2010-11-13 | 2017-03-14 |
| Reporter | jens | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
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.