Frama-C Bug Tracking System - Frama-C
View Issue Details
0000645Frama-CKernelpublic2010-12-20 15:002014-02-12 16:55
sduprat 
monate 
normalminoralways
closedfixed 
Frama-C Carbon-20101202-beta2 
Frama-C Carbon-20110201 
0000645: lose of location displayed by Cil.warning
In previous releases, location displayed by Cil.warning was correct. In Carbon beta 2, location is sometimes 0.
with 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
No tags attached.
tar line.tar (286,720) 2010-12-20 15:00
https://bts.frama-c.com/file_download.php?file_id=139&type=bug
Issue History
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:43svnCheckin
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

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.