Frama-C Bug Tracking System - Frama-C
View Issue Details
0001582Frama-CKernel > ACSL implementationpublic2013-12-03 18:352013-12-03 18:35
pascal 
virgile 
normaltweakalways
assignedopen 
Frama-C GIT, precise the release id 
 
0001582: r24600: confusing error message when t[] is used where t* is expected
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.
No tags attached.
Issue History
2013-12-03 18:35pascalNew Issue
2013-12-03 18:35pascalStatusnew => assigned
2013-12-03 18:35pascalAssigned To => virgile

There are no notes attached to this issue.