NAME

SYNOPSIS

DESCRIPTION

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.

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

COPYRIGHT

WEB SITE