lose of location displayed by Cil.warning
ID0000645: This issue was created automatically from Mantis Issue 645. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000645 | Frama-C | Kernel | public | 2010-12-20 | 2014-02-12 |
Reporter | sduprat | Assigned To | monate | Resolution | fixed |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Carbon-20101202-beta2 | Target Version | - | Fixed in Version | Frama-C Carbon-20110201 |
Description :
In previous releases, location displayed by Cil.warning was correct.
In Carbon beta 2, location is sometimes 0.
Additional Information :
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