"Loss of precision" message after shift

ID0001423: This issue was created automatically from Mantis Issue 1423. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001423	Frama-C	Plug-in > Eva	public	2013-05-22	2013-05-23

Reporter	dhekir	Assigned To	yakobowski	Resolution	no change required
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Fluorine-20130401	Target Version	-	Fixed in Version	-

Description :

If I use Frama-C to analyze the following program:

int a[2];

int main() { int i = &(a[0]); int j = i >> 8; return 0; }

The value analysis reports the following:

[kernel] preprocessing with "gcc -C -E -I. test.c" [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization a[0..1] ? {0} test.c:5:[kernel] warning: Operation {{ &a }} >> {8} incurs a loss of precision test.c:5:[value] Assigning imprecise value to j. The imprecision originates from Arithmetic {test.c:5} [value] Recording results for main [value] done for function main

Is this expected? Shouldn't there be a message in line 4? I'm sorry if my understanding of the C standard is incorrect, but I believe the warning could be made in a more clear way, or maybe it could reference line 4 to help the user see the original source of the problem.