Unable to verify pointer dereferencing

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

---

Id	Project	Category	View	Due Date	Updated
ID0000156	Frama-C	Plug-in > jessie	public	2009-06-09	2009-06-10

Reporter	boris	Assigned To	-	Resolution	no change required
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	-

Description :

Jessie is unable to verify pointer dereferencing in the following code:

/*@ requires \valid(a+ (left..right)); */ void foo(int a[], int left, int right) { int k;

k = a[right]; // Jessie fails here
}