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.
|ID0001582||Frama-C||Kernel > ACSL implementation||public||2013-12-03||2013-12-03|
|Product Version||Frama-C GIT, precise the release id||Target Version||-||Fixed in Version||-|
~ $ cat t.c char t;
/*@ requires t <= p <= t+5; */ void f(char *p);
~ $ frama-c t.c
[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.
comparison of incompatible types: char * and char in annotation.
I am fine with t <= p being rejected, since it is possible to write &t 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.