[bug] Invalid contract for Buffer.BlockCopy

Question

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".

 

---

Developer

Answer 1

Yes, I agree that seems wrong.

Answer 2

Hello,

  our contract faithfully reflects the documentation:

 

http://msdn.microsoft.com/en-us/library/system.buffer.blockcopy.aspx 

 

ciao

f

Answer 3

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[10];
  var dst = new double[5];

  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.

Answer 4

So what did you decide? Has Matthew Watson explanation convinced you?

---

Developer

Answer 5

There's no doubt about it that it's currently wrong, but who knows if it'll be fixed. :)

Answer 6

ok, it is fixed (internally).

Sorry for that.

f