Verify .NET Code Contracts with cccheck

When a test suite passes but you still do not trust an assumption buried in the code, cccheck is the tool that checks it statically. You run it against a compiled CLR assembly, narrow a check to matching methods, and learn to tell a proved assertion from one the analyser simply could not prove.

Allow about fifteen minutes if the assembly is already built. The examples use Mono package version 6.8.0.105+dfsg-3.6ubuntu2, installed here as mono-devel.

It helps to know what this tool is not: a test runner. It reads an assembly and reasons about supported contracts without executing the application. It currently supports Contract.Assume() and Contract.Assert(), with non-null analysis as the only analysis the installed manual page describes.

1. Check the installed interface

Confirm which executable will actually run and read its local help. This matters because the manual page and the executable's help use slightly different notation for the debug option:

$ command -v cccheck
/usr/bin/cccheck
$ cccheck --help
cccheck

Options:
      --help                 Show this help.
      --assembly=VALUE       Assembly to check.
      --method=VALUE         Method name (if you want to check only it).
      --debug=VALUE          Show debug information

The required input is an assembly path. There is no project-file discovery step here, so pass the output of your build explicitly. Run it as your normal user when the file is readable; nothing in the normal verification workflow needs root.

2. Build with the contracts symbol enabled

The assembly must have been built with CONTRACTS_FULL defined. Skip that symbol and the compiler is free to strip out calls to contract methods, leaving cccheck with nothing to inspect. This is a build prerequisite, not something you can patch up at verification time.

• Define the symbol at build time. How you do it depends on your build system; in a compiler command that accepts C# preprocessor symbols, set the equivalent of CONTRACTS_FULL.
• Keep the output somewhere disposable. A reviewable build directory works well.
• Pass the real path to the verifier, not a source path or a project file:

$ cccheck --assembly=/path/to/ContractsEnabled/bin/Release/Example.dll

The tool loads the assembly's metadata, so a missing or unreadable path fails before any proof result exists. On this installation a missing file produces a Mono FileNotFoundException from the assembly reader. Check the path first, without touching permissions:

$ ls -l /path/to/ContractsEnabled/bin/Release/Example.dll
$ test -r /path/to/ContractsEnabled/bin/Release/Example.dll && echo "assembly is readable"

Nothing here needs undoing afterwards. Verification only reads the assembly; it never rewrites it.

3. Read the proof result

For each assertion the verifier reports a location, a subroutine, basic block and program counter, followed by a result: true, false, unproven or unreachable. That location is an analyser coordinate, not a source line number:

Assertion at : [Subroutine: <id> Block <blockId> PC <id>] : is (true|false|unproven|unreachable)

• true is the result you actually wanted: the assertion is proved.
• false means the assertion does not hold along a path the analyser found.
• unproven means the analysis could not establish it, which is not the same as evidence it is safe.
• unreachable means the analyser's model treats that location as unreachable, which still deserves a look if the code can actually be reached at runtime.

The tool can also print an error when it cannot fully process a method. Keep that diagnostic with the verification output and investigate it separately: a clean exit code is not a substitute for reading the individual results.

4. Narrow a long verification run

Use --method to filter by a name substring when a run is dragging. It is not a regular expression and it will not necessarily pick out one exact method, so choose a distinctive substring, especially where overloads or similarly named helpers exist:

$ cccheck --assembly=/path/to/ContractsEnabled/bin/Release/Example.dll --method=ParseOrder

Use this after a broad run, to dig into one area of a large assembly. If the substring catches more methods than expected, lengthen it and rerun. If it catches nothing, check the spelling and remember the filter searches method names, not source-file names.

5. Use debug output only when the result needs tracing

The manual describes --debug as showing four proof layers: raw, stack, heap and substituted-expression levels. The installed executable's help shows it as --debug=VALUE, so check that help on the actual machine before adding a value. Do not copy a debug invocation from another Mono release without checking its syntax first.

Debug output can run far longer than the assertion summary. Save it to a new file instead of overwriting an existing report:

$ cccheck --assembly=/path/to/ContractsEnabled/bin/Release/Example.dll > cccheck-example.txt

This redirection replaces cccheck-example.txt if it already exists, so pick a new filename when the old report still matters. If the command fails, the shell can still leave a partial report behind; inspect it before deleting it. No service is stopped and no system configuration changes.

6. Diagnose the limits before changing code

The installed verifier is deliberately narrower than the full Code Contracts model. The manual documents non-null analysis and the two supported contract methods, and says consecutive analyses are still in development. An assembly loading successfully is not proof that an assertion involving arithmetic, a custom contract method or an unsupported construct has actually been checked.

1. Confirm the build symbol was really present.
2. Run the smallest method filter that reproduces the result.
3. Compare the assembly's timestamp or checksum with the build artefact you meant to analyse.

These three checks catch stale DLLs and contract calls quietly removed during compilation, without touching the source or the host.

Do not "fix" an unproven result by weakening or deleting the assertion. Review the control-flow assumptions, simplify the method if that is reasonable, or accept the result as a limitation needing another tool. Keep the input assembly and its report together so a later reviewer can reproduce exactly the same run.