Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000645Frama-CKernelpublic2010-12-20 15:002014-02-12 16:55
Reportersduprat 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Carbon-20110201 
Summary0000645: lose of location displayed by Cil.warning
DescriptionIn previous releases, location displayed by Cil.warning was correct.

In Carbon beta 2, location is sometimes 0.


Additional Informationwith the plugin in attached file and test1.c source file :

> frama-c -test1 -no-collapse-call-cast ../test1.c

[kernel] preprocessing with "gcc -C -E -I. ../test1.c"
:0:[kernel] warning: exp = 0
:0:[kernel] warning: exp = 1
:0:[kernel] warning: exp = 2
../test1.c:5:[kernel] warning: exp = 1
:0:[kernel] warning: exp = __retres
../test1.c:12:[kernel] warning: exp = f0
../test1.c:12:[kernel] warning: exp = *p
../test1.c:12:[kernel] warning: exp = p
:0:[kernel] warning: exp = (enum __anonenum_pole_1 )tmp
:0:[kernel] warning: exp = tmp
../test1.c:13:[kernel] warning: exp = f0
../test1.c:13:[kernel] warning: exp = *p
../test1.c:13:[kernel] warning: exp = p
../test1.c:13:[kernel] warning: exp = t
../test1.c:13:[kernel] warning: exp = t
:0:[kernel] warning: exp = (enum __anonenum_pole_1 )tmp_0
:0:[kernel] warning: exp = tmp_0
../test1.c:13:[kernel] warning: exp = t

TagsNo tags attached.
Relationships
Attached Filestar line.tar (286,720) 2010-12-20 15:00
https://bts.frama-c.com/file_download.php?file_id=139&type=bug

Notes
(0001336)
monate   
2010-12-20 16:57   
You are right: this is a regression. Since Carbon, expressions have an explicit location field (eloc). Sadly, this field is not yet filled.
This will be fixed in the final Carbon.
(0001337)
monate   
2010-12-20 19:41   
This is not related to the bug but you may prefer this way of pretty printing your messages. They become related to your plugin.
      method vexpr expr =
    Self.warning ~current:true "exp = %a" Cil.d_exp expr;
        Cil.DoChildren

instead of using the very generic "Cil.warning" function.

Issue History
Date ModifiedUsernameFieldChange
2010-12-20 15:00sdupratNew Issue
2010-12-20 15:00sdupratFile Added: line.tar
2010-12-20 16:54monateAssigned To => monate
2010-12-20 16:54monateStatusnew => acknowledged
2010-12-20 16:57monateNote Added: 0001336
2010-12-20 19:41monateNote Added: 0001337
2010-12-20 19:43svn
2010-12-20 19:43svnStatusacknowledged => resolved
2010-12-20 19:43svnResolutionopen => fixed
2011-02-09 14:36signolesStatusresolved => closed
2011-02-09 14:37signolesFixed in Version => Frama-C Carbon-20110201
2013-12-19 01:12svnSource_changeset_attached => framac master 9eeeb0b1
2014-02-12 16:55monateSource_changeset_attached => framac stable/neon 9eeeb0b1