r24600: confusing error message when t[] is used where t* is expected

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

---

Id	Project	Category	View	Due Date	Updated
ID0001582	Frama-C	Kernel > ACSL implementation	public	2013-12-03	2013-12-03

Reporter	pascal	Assigned To	virgile	Resolution	open
Priority	normal	Severity	tweak	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

TO REPRODUCE:

~ $ cat t.c
char t[5];

/*@ requires t <= p <= t+5; */
void f(char *p);

~ $ frama-c t.c

OBTAINED BEHAVIOR:

[kernel] warning: cannot load plug-in `Kitgen' (incompatible with Fluorine-20130601+dev). [kernel] preprocessing with "gcc -C -E -I. t.c" t.c:3:[kernel] user error: comparison of incompatible types: char * and char * in annotation. [kernel] user error: skipping file "t.c" that has errors. [kernel] Frama-C aborted: invalid user input.

EXPECTED BEHAVIOR:

comparison of incompatible types: char * and char[] in annotation.

DESCRIPTION:

I am fine with t <= p being rejected, since it is possible to write &t[0] which is a pointer to char in a stricter sense, or t+0 which is even shorter. However, the error message “ incompatible types: char * and char * ” is misleading.