To give you some experience with writing and attempting to prove contracts with Frama-C and the WP plug-in, try the following:
In the C header file buffers.h write a declaration for Copy_Into following the SPARK version of the procedure. Include appropriate ACSL statements (postcondition, etc).
Implement the function in buffers.c, again following the SPARK version.
See if you can get Frama-C, using the WP plugin, to prove the postcondition and thus show that your implementation has the property described by that postcondition.
Zip together the two files buffer.h and buffer.c and submit the zip archive.