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