GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages


Manual Reference Pages  -  CCCHECK (1)

NAME

cccheck - Perform static code contracts verification for CLR assemblies.

CONTENTS

Synopsis
Description
Configuration Options
Examples
Author
Copyright
Web Site

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
Search for    or go to Top of page |  Section 1 |  Main Index


MONO (cccheck) -->

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with manServer 1.07.