Mono(cccheck)Mono(cccheck)NAMEcccheck - Perform static code contracts verification for CLR assem‐
blies.
SYNOPSIScccheck --assembly=<assembly> [options]
DESCRIPTION
Perform static code contracts verification to find bugs and inconsis‐
tences 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 sup‐
ported. 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.
CONFIGURATION OPTIONS--assembly <assembly-name>
The assembly to perform static verification.
--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.
--method=<method-name-substring>
String for finding method. It filters all methods in assembly
where method name has this parameter as a substring.
--help Show help for cccheck, listing configuration options.
EXAMPLES
Suppose you have a method:
void Method() {
object x = null;
int y = 1;
if (y % 2 == 1)
x = new object();
else
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)
AUTHOR
Written by Alexander Chebaturkin
COPYRIGHT
Copyright 2011 Alexander Chebaturkin. Released under MIT license.
WEB SITE
Visit http://www.mono-project.com for details
Mono(cccheck)
