2021-01-27 08:48 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001582Frama-CKernel > ACSL implementationpublic2013-12-03 18:35
Assigned Tovirgile 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001582: r24600: confusing error message when t[] is used where t* is expected
DescriptionTO REPRODUCE:

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

/*@ 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[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.
TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2013-12-03 18:35 pascal New Issue
2013-12-03 18:35 pascal Status new => assigned
2013-12-03 18:35 pascal Assigned To => virgile
+Issue History