Assertion failure when unrolling types of struct members
ID0002191: This issue was created automatically from Mantis Issue 2191. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002191 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2017-01-18 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Magnesium | Target Version | - | Fixed in Version | Frama-C 14-Silicon |
Description :
/* The following program leads to a failure of an assertion in translate.ml. The failure seems to be due to E-ACSL inability to determine the type of the term _G[0].str. */
struct ST { char *str; int num; };
struct ST _G[] = { { .str = "Struct_G[0]", .num = 99 }, { .str = "Struct_G[1]", .num = 147 } };
int main(int argc, char **argv) { /*@ assert \valid_read(_G[0].str); */ return 0; }