Mono(cccheck)

✨ Mono(cccheck) — cccheck, bestie edition ✨

okay so welcome to the Mono(cccheck) manual page, grab a snack, we're doing static analysis 💅

🎀 NAME 🎀

cccheck — perform static code contracts verification for CLR assemblies. it's giving "your code says one thing and does another and we're gonna catch it" 🔍

🦋 SYNOPSIS 🦋

cccheck --assembly=<assembly> [options]

💖 DESCRIPTION 💖

So what does cccheck actually do? It performs static code contracts verification to find bugs and inconsistencies between code and specification. that includes non-null analyses and integer analyses, no cap 🔥

⚠️ Big important thing, bestie: the assembly must have been built with the symbol CONTRACTS_FULL defined. if it wasn't, then the calls to the contract methods will have been removed by the compiler and there's literally nothing left for the tool to look at 😭

Currently only Contract.Assume() and Contract.Assert() methods are supported. Only non-null analysis is supported, and the consecutive analyses are in development (they're cooking 👩‍🍳). An error message will be shown if cccheck is unable to process all or some of the methods of specified assembly — so if it can't handle everything, it will tell you, it's not gonna be quiet about it.

🌈 CONFIGURATION OPTIONS 🌈

• --assembly <assembly-name> — the assembly to perform static verification on. this is the one, the main character, the whole reason we're here 👑
• --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. four whole layers, bestie, it's a whole stack of lore 🧚
• --method=<method-name-substring> — string for finding method. it filters all methods in assembly where method name has this parameter as a substring. so like, partial name match energy ✨
• --help — show help for cccheck, listing configuration options. when in doubt, ask the tool itself 🫶

🌸 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. open source legend behavior honestly

🌐 WEB SITE 🌐

Visit http://www.mono-project.com for details 👀

and that's the whole page, bestie! this little love letter lives in the Mono(cccheck) manual, so that's your source/version tag right there — go forth and verify those contracts, mwah 💋🎀