man/cccheck.1

   1 .\"
   2 .\" cccheck manual page.
   3 .\" Copyright (C) 2011 Alexander Chebaturkin
   4 .\" Author:
   5 .\"   Alexander Chebaturkin (chebaturkin@gmail.com)
   6 .\"
   7 .TH Mono "cccheck"
   8 .SH NAME
   9 cccheck \- Perform static code contracts verification for CLR assemblies.
  10 .SH SYNOPSIS
  11 .PP
  12 .B cccheck --assembly=<assembly> [options]
  13 .SH DESCRIPTION
  14 Perform static code contracts verification to find bugs and inconsistencies
  15 between code and specification. This includes non-null, integer analyses.
  16 .PP
  17 The assembly must have been built with the symbol CONTRACTS_FULL defined,
  18 otherwise the calls to the contract methods will have been removed
  19 by the compiler.
  20 .PP
  21 Currently only Contract.Assume() and Contract.Assert() methods are
  22 supported. Only non-null analysis is supported, the consecutive analyses are
  23 in development. An error message will be shown if cccheck is unable to process
  24 all or some of the methods of specified assembly.
  25 .SH CONFIGURATION OPTIONS
  26 .TP
  27 .I "--assembly <assembly-name>"
  28 The assembly to perform static verification.
  29 .TP
  30 .I "--debug"
  31 Shows debug information about process of proving the assertions. It shows
  32 four layers of abstraction, raw layer, stack layer, heap layer,
  33 and substituted expression level.
  34 .TP
  35 .I "--method=<method-name-substring>"
  36 String for finding method. It filters all methods in assembly where method
  37 name has this parameter as a substring.
  38 .TP
  39 .I "--help"
  40 Show help for cccheck, listing configuration options.
  41
  42 .SH EXAMPLES
  43 .TP
  44 Suppose you have a method:
  45   void Method() {
  46     object x = null;
  47     int y = 1;
  48     if (y % 2 == 1)
  49       x = new object();
  50     else
  51       x = new string();
  52
  53    Contract.Assert(x != null);
  54 }
  55
  56 After the verification the tool will have results in following format:
  57 "Assertion at : [Subroutine: <id> Block <blockId> PC <id>] :
  58  is (true|false|unproven|unreachable)".
  59 (PC is a program counter)
  60
  61 .SH AUTHOR
  62 Written by Alexander Chebaturkin
  63 .SH COPYRIGHT
  64 Copyright 2011 Alexander Chebaturkin.
  65 Released under MIT license.
  66 .SH WEB SITE
  67 Visit http://www.mono-project.com for details