GitLab

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; }