numerous asserts within the same comment are not possible

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

---

Id	Project	Category	View	Due Date	Updated
ID0000246	Frama-C	Plug-in > jessie	public	2009-09-16	2014-02-12

Reporter	Christoph	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090901	Target Version	-	Fixed in Version	-

Description :

Hello,

I do not know whether its a bug or a feature but asserts like the following cause problems:

(excerpt from a code):

for ( ; i < length; ++i)
    if (a[i] != value)
    {
        b[j] = a[i];
        /*@
	assert \forall integer k; ! ( 0 <= k < j) ==> b[k] == \at(b[k],Pre);
            assert j+1 == spec_remove_copy{Pre,Here}(a, i, b, j, value);
        */
        ++j;
    }
return j;

} This happens with any code I have tried.

Sincerely

Christoph