Skip to content

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

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information