diff options
author | Alexander Chebaturkin <chebaturkin@gmail.com> | 2011-07-14 02:47:34 +0400 |
---|---|---|
committer | Marek Safar <marek.safar@gmail.com> | 2011-08-25 00:35:02 +0400 |
commit | e8352f0bd13a2999064eece8af4214c540fbc156 (patch) | |
tree | 97dfa05a49680012b63e247b277372056cf1720f /man/cccheck.1 | |
parent | 33d931c95b09861c416b57135f727bd879b315d1 (diff) |
The base architecture for code-contracts analysis
Diffstat (limited to 'man/cccheck.1')
-rw-r--r-- | man/cccheck.1 | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/man/cccheck.1 b/man/cccheck.1 new file mode 100644 index 00000000000..aead19a58d0 --- /dev/null +++ b/man/cccheck.1 @@ -0,0 +1,67 @@ +.\" +.\" cccheck manual page. +.\" Copyright (C) 2011 Alexander Chebaturkin +.\" Author: +.\" Alexander Chebaturkin (chebaturkin@gmail.com) +.\" +.TH Mono "cccheck" +.SH NAME +cccheck \- Perform static code contracts verification for CLR assemblies. +.SH SYNOPSIS +.PP +.B cccheck --assembly=<assembly> [options] +.SH DESCRIPTION +Perform static code contracts verification to find bugs and inconsistences +between code and specification. This includes non-null, integer analyses. +.PP +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. +.PP +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. +.SH CONFIGURATION OPTIONS +.TP +.I "--assembly <assembly-name>" +The assembly to perform static verification. +.TP +.I "--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. +.TP +.I "--method=<method-name-substring>" +String for finding method. It filters all methods in assembly where method +name has this parameter as a substring. +.TP +.I "--help" +Show help for cccheck, listing configuration options. + +.SH EXAMPLES +.TP +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) + +.SH AUTHOR +Written by Alexander Chebaturkin +.SH COPYRIGHT +Copyright 2011 Alexander Chebaturkin. +Released under MIT license. +.SH WEB SITE +Visit http://www.mono-project.com for details |