Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001582Frama-CKernel > ACSL implementationpublic2013-12-03 18:352013-12-03 18:35
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeveritytweakReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
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

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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker