1Mono(cccheck)                                                    Mono(cccheck)
2
3
4

NAME

6       cccheck  -  Perform  static  code contracts verification for CLR assem‐
7       blies.
8

SYNOPSIS

10       cccheck --assembly=<assembly> [options]
11

DESCRIPTION

13       Perform static code contracts verification to find bugs  and  inconsis‐
14       tencies between code and specification. This includes non-null, integer
15       analyses.
16
17       The assembly must  have  been  built  with  the  symbol  CONTRACTS_FULL
18       defined,  otherwise  the  calls  to the contract methods will have been
19       removed by the compiler.
20
21       Currently only Contract.Assume() and Contract.Assert() methods are sup‐
22       ported.  Only  non-null analysis is supported, the consecutive analyses
23       are in development. An error message will be shown if cccheck is unable
24       to process all or some of the methods of specified assembly.
25

CONFIGURATION OPTIONS

27       --assembly <assembly-name>
28              The assembly to perform static verification.
29
30       --debug
31              Shows debug information about process of proving the assertions.
32              It shows four layers of abstraction,  raw  layer,  stack  layer,
33              heap layer, and substituted expression level.
34
35       --method=<method-name-substring>
36              String  for  finding  method. It filters all methods in assembly
37              where method name has this parameter as a substring.
38
39       --help Show help for cccheck, listing configuration options.
40
41

EXAMPLES

43       Suppose you have a method:
44                void Method() {
45                  object x = null;
46                  int y = 1;
47                  if (y % 2 == 1)
48                    x = new object();
49                  else
50                    x = new string();
51
52                 Contract.Assert(x != null); }
53
54              After the verification the tool will have results  in  following
55              format:  "Assertion  at  :  [Subroutine: <id> Block <blockId> PC
56              <id>] :
57               is  (true|false|unproven|unreachable)".   (PC  is   a   program
58              counter)
59
60

AUTHOR

62       Written by Alexander Chebaturkin
63

65       Copyright 2011 Alexander Chebaturkin.  Released under MIT license.
66

WEB SITE

68       Visit http://www.mono-project.com for details
69
70
71
72                                                                 Mono(cccheck)
Impressum