Thursday, August 18, 2011 8:38 AM
I use System.Buffer.BlockCopy method and get following warning:
Warning 32 CodeContracts: requires unproven: src.Length - count >= srcOffset
The requirement seems to be wrong as count parameter is not about src array elements but "the number of bytes to copy". As well as srcOffset is "The zero-based byte offset into src".
Thursday, August 18, 2011 10:13 AMYes, I agree that seems wrong.
Thursday, August 18, 2011 8:27 PMOwner
our contract faithfully reflects the documentation:
Thursday, August 18, 2011 9:24 PM
But src.Length is in units of elements, not units of bytes, surely?
The method signature is:
void BlockCopy( Array src, int srcOffset, Array dst, int dstOffset, int count )
Note that srcOffset is a byte offset, not an element index.
Also note that count is a number of bytes, not a number of elements.
Now the precondition is this:
src.Length - count >= srcOffset
src is of type Array, therefore src.Length is the number of elements in the array, NOT the number of bytes in the array.
But the precondition is subtracting count (a number of bytes) from src.Length (a number of elements). It seems to me that this can't be right...
The online documentation itself does indeed state that it is an error if "the length of src is less than srcOffset plus count."
It therefore looks as if the documentation itself is wrong.
Consider this code (which runs correctly):
var src = new int; var dst = new double; Buffer.BlockCopy(src, 0, dst, 0, src.Length * sizeof(int));
In the call to BlockCopy(), srcOffset is 0, and count is 10 * 4 = 40 (10 elements times sizeof(int)).
src.Length is 10 (the number of integer elements that it contains).
The precondition will therefore be: "Requires(10 - 40 >= 0)", which clearly fails since -30 is not >=0.
The method call succeeds however, because although the documentation and the precondition are both incorrect, the method itself is implemented correctly.
Monday, August 22, 2011 2:55 PMSo what did you decide? Has Matthew Watson explanation convinced you?
Wednesday, September 07, 2011 10:42 AMThere's no doubt about it that it's currently wrong, but who knows if it'll be fixed. :)
Monday, May 07, 2012 6:42 PMOwner
ok, it is fixed (internally).
Sorry for that.