GitLab

ID0000358: This issue was created automatically from Mantis Issue 358. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000358	Frama-C	Kernel > ACSL implementation	public	2009-12-08	2010-04-13

Reporter	cmarche	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090902	Target Version	-	Fixed in Version	Frama-C Boron-20100401

Description :

In C, the code

typedef int t; t t();

fails with error: ‘t’ redeclared as different kind of symbol

The logic parser should produce a similar error as in

/*@ axiomatic A {

logic type t; logic t t(integer n);

} */

which do not produce any error, but if you do later

//* lemma \forall integer n; t(n) == t(n);

you get user error: syntax error while parsing annotation

which is very difficult to understand !