Code Inspection: Problem in contract annotation definition
This inspection verifies the syntax of contract annotations.
Syntax of contract annotations
Use the following syntax to specify input-output dependencies for contract annotations:
[ContractAnnotation("[paramName:][input] => output [; [paramName:][input] => output]", [forceFullStates:true])]
The input
can be:
The output
can be
-
null
/notnull
/canbenull
for the return value of reference type -
true
/false
for the return value of boolean type -
halt
|stop
|void
|nothing
(which are interchangeable) to indicate that the function does not return normally. I.e., it throws an exception or halts program execution.
The optional boolean forceFullStates
parameter, which is false by default, allows you force the pessimistic mode for the nullability analysis. I.e. if the method return value is not defined by the contract condition, Rider will assume that it might be null.
Remarks:
- You can omit
paramName
if there is only one parameter (see the example above) - You can omit both
paramName
andinput
if there are no parameters:or if the function has the same output independently on the input:[ContractAnnotation("=> halt")] public void TerminationMethod()
[ContractAnnotation("=> halt")] public void TerminationMethod(object data, bool flag)
- You can add several conditions for the same parameter:
[ContractAnnotation("input:null => null; input:notnull=>notnull")] public object Transform(object input, bool flag)
- You can reverse conditions, i.e.
input => output
is equal tooutput <= input
:[ContractAnnotation("halt <= condition:false")] public void Assert(bool condition, string text)
- You can also specify expected values for 'out' parameters. If you want to specify both a return value and an 'out' parameter for the same input condition, use the comma:
[ContractAnnotation("s:null => false,result:null")] public bool TryParse(string s, out object result)
Last modified: 11 October 2017