Interface precondition not translating to implementations during static analysis - by naasking

Status : 

  Fixed<br /><br />
		This item has been fixed in the current or upcoming version of this product.<br /><br />
		A more detailed explanation for the resolution of this particular item may have been provided in the comments section.


1
0
Sign in
to vote
ID 785045 Comments
Status Closed Workarounds
Type Bug Repros 0
Opened 4/18/2013 11:00:29 AM
Access Restriction Public

Description

If I define an interface with a corresponding contract class declaring some preconditions, then I create an implementation of said interface and copy over the preconditions as assertions to the implementation, many of the assertions fail when the code contracts checker is set to report all warnings.

If you remove the interface and simply copy over all the preconditions and place them before the assertions, compilation succeeds as expected.

See the code sample below.
Sign in to post a comment.
Posted by Microsoft on 3/10/2014 at 2:25 PM
The bug in Error2.cs has been fixed in the most recent release of Code Contracts.

For the bug in Error1.cs, it is a known limitation with the tools, which will be addressed in the future.
The time being, the best thing is to mask it adding this attribute at the definition of IArray<,,>.TArray:

[SuppressMessage("Microsoft.Contracts", "EnsuresInMethod-Length(left) == Length(Contract.Result<TArray>())")]
Posted by Microsoft on 4/19/2013 at 5:25 AM
Thank you for submitting feedback on Visual Studio and .NET Framework. Your issue has been routed to the appropriate VS development team for investigation. We will contact you if we require any additional information.
Posted by naasking on 4/18/2013 at 5:49 PM
I have attached another sample where the postconditions are not properly applied. That is, the postconditions from the interface are expected to be satisfied and the static checker seems to recognize this fact. However, the condition is quite obviously satisfied and the checker doesn't recognize it. I can't even get it to recognize the satisfaction by explicitly specifying the assumption.
Posted by Microsoft on 4/18/2013 at 11:56 AM
Thank you for your feedback, we are currently reviewing the issue you have submitted. If this issue is urgent, please contact support directly(http://support.microsoft.com)
Posted by naasking on 4/18/2013 at 11:02 AM
Sorry about the muddled text. I've attached a file containing the code sample.