Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
Attached Filestar file icon line.tar [^] (286,720 bytes) 2010-12-20 15:00

- Relationships

-  Notes
(0001336)
monate (reporter)
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 (reporter)
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 Modified Username Field Change
2010-12-20 15:00 sduprat New Issue
2010-12-20 15:00 sduprat File Added: line.tar
2010-12-20 16:54 monate Assigned To => monate
2010-12-20 16:54 monate Status new => acknowledged
2010-12-20 16:57 monate Note Added: 0001336
2010-12-20 19:41 monate Note Added: 0001337
2010-12-20 19:43 svn Checkin
2010-12-20 19:43 svn Status acknowledged => resolved
2010-12-20 19:43 svn Resolution open => fixed
2011-02-09 14:36 signoles Status resolved => closed
2011-02-09 14:37 signoles Fixed in Version => Frama-C Carbon-20110201


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker