CODEWITHSUNDEEP
c#.netcode-contracts
Xander
Xander

Reputation: 9171

Code contracts static checking not working correctly?

I made a class with a code contract in the constructor CodeTypes has a list of string properties.

Contract.Requires(type == CodeTypes.AdmitDx1 || type == CodeTypes.AdmitDx2
|| type == CodeTypes.AdmitDx3 || type == CodeTypes.DX 
|| type == CodeTypes.CPT || type == CodeTypes.HCPCS
|| type == CodeTypes.PX);

After that warnings appeared where I was using this class because different values were put in. So far so good.

Then I went to a piece of the code where there was a complaint and added the opposite of the if statement and threw an exception.

The warning remained.

I then added a return statement on the opposite of the if statement.

The warning remained.

I then put a big if/else where the class was only called if the condition in the contract was meant.

The warning remained.

I then surrounded the contract with an if statement with that condition.

The warning disappeared.

What is going on here? I expected the 1st 3 options to work and I really wanted to use option 1. What is the best way to go about this?

Edit the calling Code the contract exists in the constructor of CreateCodeFromType:

//Type is an XElement that is passed into the method as a parameter
    if (type == null || (type.Value != CodeTypes.AdmitDx1 && type.Value != CodeTypes.AdmitDx2
    && type.Value != CodeTypes.AdmitDx3 && type.Value != CodeTypes.DX
    && type.Value != CodeTypes.CPT && type.Value != CodeTypes.HCPCS
    && type.Value != CodeTypes.PX))
    {
    throw new ValidationException("Type is invalid.");
    }
    else
    {
    var newCode = (new CreateCodeFromType(type.Value).CreateCode(term.Value));
    }

Upvotes: 0

Views: 710

Answers (2)

JBSnorro
JBSnorro

Reputation: 6746

If this "other piece of code" you mentioned is in another method, not the constructor, then you must have saved the arguments to fields on the constructed type. In that case the static checker can't check anything based on throwing or returning when a condition is not met, because after the conditions were met, another thread might change the fields in such a way that it would fail the conditions. To prevent the warnings in this case, use a ContractInvariantMethodAttribute.

If this piece of code is still in the constructor I can't think of any reason why the static checker couldn't omit the warnings(but then again, why use if-statements if you already have the Contract.Requires precondition?). In that case I'd blame the imperfection of the static checker, like Stephen does too.

EDIT: given the example I can see what's wrong.

I stated that the static checker can't guarantee anything of fields, since other threads might be messing with those fields. The type.Value is a field, so it is logical the static checker warns you of the possible breaking of the contract. I would even expect the warning in the case you claim it disappears(or I'm misinterpreting you). To solve this, create a local variable and then you've got a something the static checker can reason about. So try the following:

if (type == null) throw new ArgumentNullException();
var xElementValue = type.Value;
if(xElementValue != CodeTypes.AdmitDx1 && xElementValue != CodeTypes.AdmitDx2
&& xElementValue != CodeTypes.AdmitDx3 && xElementValuee != CodeTypes.DX
&& xElementValue != CodeTypes.CPT && xElementValue != CodeTypes.HCPCS
&& xElementValue != CodeTypes.PX) throw new ValidationException("Type is invalid.");
//And now you should be able to give xElementValue as argument without receiving warnings.

Or if you want to use contracts, use

Contract.Requires(type != null);
var xElementValue = type.Value;
Contract.Requires(xElementValue == CodeTypes.AdmitDx1 || xElementValue== CodeTypes.AdmitDx2
|| xElementValue== CodeTypes.AdmitDx3 || xElementValue== CodeTypes.DX 
|| xElementValue== CodeTypes.CPT || xElementValue== CodeTypes.HCPCS
|| xElementValue == CodeTypes.PX);

I hope the warnings don't show theirselves with either of these solutions.

Upvotes: 1

Stephen Cleary
Stephen Cleary

Reputation: 457217

The static checker is not perfect. It's still in development, and even when it's complete, it won't be able to know everything.

For now, you can give the static checker a hint using Contract.Assume and passing the condition.

Also, keep up-to-date on CC releases. They are currently at 1.4.31130.0 and planning another release soon. At this point in the development, the static checker is seeing incremental improvements with each release.

Upvotes: 0

Related Questions