Find file
Fetching contributors…
Cannot retrieve contributors at this time
68 lines (63 sloc) 1.98 KB
.\" cccheck manual page.
.\" Copyright (C) 2011 Alexander Chebaturkin
.\" Author:
.\" Alexander Chebaturkin (
.TH Mono "cccheck"
cccheck \- Perform static code contracts verification for CLR assemblies.
.B cccheck --assembly=<assembly> [options]
Perform static code contracts verification to find bugs and inconsistences
between code and specification. This includes non-null, integer analyses.
The assembly must have been built with the symbol CONTRACTS_FULL defined,
otherwise the calls to the contract methods will have been removed
by the compiler.
Currently only Contract.Assume() and Contract.Assert() methods are
supported. Only non-null analysis is supported, the consecutive analyses are
in development. An error message will be shown if cccheck is unable to process
all or some of the methods of specified assembly.
.I "--assembly <assembly-name>"
The assembly to perform static verification.
.I "--debug"
Shows debug information about process of proving the assertions. It shows
four layers of abstraction, raw layer, stack layer, heap layer,
and substituted expression level.
.I "--method=<method-name-substring>"
String for finding method. It filters all methods in assembly where method
name has this parameter as a substring.
.I "--help"
Show help for cccheck, listing configuration options.
Suppose you have a method:
void Method() {
object x = null;
int y = 1;
if (y % 2 == 1)
x = new object();
x = new string();
Contract.Assert(x != null);
After the verification the tool will have results in following format:
"Assertion at : [Subroutine: <id> Block <blockId> PC <id>] :
is (true|false|unproven|unreachable)".
(PC is a program counter)
Written by Alexander Chebaturkin
Copyright 2011 Alexander Chebaturkin.
Released under MIT license.
Visit for details