NAME

       cccheck - Perform static code contracts verification for CLR assemblies.

SYNOPSIS

       cccheck --assembly=<assembly> [options]

DESCRIPTION

       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.

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)