CMC: Integrating CEGAR Model Checking into a C Verification Framework

Overview

CMC is a tool that allows for CEGAR model checking within the Frama-C framework for analysis and verification of C programs. CMC is implemented as a Frama-C plugin (GUI version only) and allows for the verification of statement contracts. It is intended to be used together with other Frama-C plugins especially including those for abstract interpretation (value analysis) and deductive verification (wp).

It is currently in alpha. Please report any bugs/comments to Subash Shankar (subash.shankar12@hu34nter.cuny.edu with the digits removed). We would also love to hear of any applications you may be using the tool on.

Installation Instructions (Linux/Mac only)

These instructions include the versions of the tools that CMC has been tested/developed with, though It will probably also work with other versions except as otherwise stated. You may skip step 2 or 3 if you wish to use only 1 back-end CEGAR tool, though it is recommended that you install both since they won't generally work on the same programs.

  1. Install frama-c (sodium) from source. Note that cmc is not compatible with the standard yum bundle; thus, the need for a source build. CMC will work with fluorine, neon, and sodium, but does not work with frama-c versions predating fluorine.
  2. Install satabs (3.2). The standard distribution also includes the Boom model checker; if you use some other distribution, you will need to first install boom (or other model checker).
  3. Install CPAChecker (1.3.4).
  4. Make sure that  $CPACHECKER/scripts/cpa.sh and satabs (and boom) are in your path.
  5. Download and unpack CMC.
  6. Make sure that cegarmc.ml and cmc-helper.sh are in the same directory (and in your path, if not in $PWD)

To test that everything has been installed properly type:

  1. frama-c-gui -load-script cegarmc.ml -cmc -cmc-checker satabs <prog.c> on a program with a statement contract to be verified.
  2. Select the statement contract (right-click on "\*@" is one way) , and select "Prove contract using CMC" on the popup menu.
  3. CMC should then attempt to verify the statement contract.
  4. Repeat the above using the "-cmc-checker cpa" option.

Usage Instructions

CMC allows for the verification of statement contracts expressed using a subset of ACSL constructs.The options are:

Option
-cmc
 enable cmc plugin
-cmc-help
 this list
-cmc-checker {cpa,satabs}
 CEGAR model checker backend
-cmc-output <filename>
 Name of intermediate file (will be overwritten)
-cmc-context
 Use value analysis to assume initial values for variables in statement (ignored if -val flag is not used)
-cmc-maxcontext <n>
 The number of values to enumerate in the context. If it is unable to determine a context that has fewer than n values, an interval is used. Note that large values of n may adversely affect CEGAR performance since it can also be used to generate more predicates for abstraction
-cmc-numiter <n>
 The number of CEGAR iterations (not supported with cpa checker)
-cpa-timelimit <n>
 Timeout (in seconds) for CEGAR checker (not supported with satabs checker)