ClamUsage

Clam provides a Python script clam.py to analyze either C/C++ or LLVM bitcode programs.

By default, Clam analyzes programs with the zones numerical abstract domain. Users can choose other numerical abstract domains by typing the option --crab-dom=VAL. The possible values of VAL are:

• int: intervals
• ric: reduced product of int and congruences
• term-int: int with uninterpreted functions
• dis-int: disjunctive intervals based on Clousot's DisInt domain
• term-dis-int: dis-int with uninterpreted functions
• boxes: disjunctive intervals based on LDDs (only if -DUSE_LDD=ON)
• zones: Zones domain using DBMs in Split Normal Form
• soct: Octagon domain using DBMs in Split Normal Form
• oct: Octagon domain (Apron if -DUSE_APRON=ON or Elina if -DUSE_ELINA=ON)
• pk: Polyhedra domain (Apron if -DUSE_APRON=ON or Elina if -DUSE_ELINA=ON)
• rtz: reduced product of term-dis-int with zones
• w-int: wrapped interval domain

For domains without narrowing operator (for instance boxes, dis-int, and pk), you need to set the option:

--crab-narrowing-iterations=N

where N is the number of descending iterations (e.g., N=2).

You may want also to set the option:

--crab-widening-delay=N

where N is the number of fixpoint iterations before triggering widening (e.g., N=1).

The widening operators do not use thresholds by default. To use them, type the option

--crab-widening-jump-set=N

where N is the maximum number of thresholds.

We also provide the option --crab-track=VAL to indicate the level of abstraction of the translation. The possible values of VAL are:

• num: translate only operations over LLVM registers of integer and boolean types.
• sing-mem: num + translate all singleton memory objects (e.g., non-taken-address globals and stack variables).
• mem: num + translates all memory objects.

Clam runs a memory abstract domain (technical details here) that delegates all the numerical reasoning to the abstract domain selected by --crab-dom. This memory domain is enabled with option --crab-track=mem.

By default, all the analyses are run in an intra-procedural manner. Whenever possible, we recommend to run Clam with option --inline. This option will inline all function calls if the callee is not recursive. If inlining is not desired or too expensive, enable the option --crab-inter to run the inter-procedural version. Clam implements a standard top-down inter-procedural analysis with memoization. The analysis supports recursive functions.

Clam provides the very experimental option --crab-backward to enable an iterative forward-backward analysis that might produce more precise results. The backward analysis computes necessary preconditions of the error states (if program is annotated with assertions) which are used to refine the set of initial states so that the forward analysis can refine its results.

Note that apart from inferring invariants or preconditions, Clam allows checking for assertions. To do that, programs must be annotated with __CRAB_assert(c) where c is any expression that evaluates to a boolean. This and other similar functions are defined in this header file

Then, you can type:

clam.py test.c --crab-check=assert

and you should see something like this:

user-defined assertion checker using SplitDBM
2  Number of total safe checks
0  Number of total error checks
0  Number of total warning checks

Finally, Clam can optimize the LLVM bitcode using the invariants produced by itself. The option --crab-opt=dce removes dead code. The option --crab-opt=replace-with-constants replace values with constants. Clam can also insert the invariants into the LLVM bitcode via verifier.assume instructions (the option --crab-promote-assume replaces verifier.assume instructions with llvm.assume intrinsics). The options --crab-opt=add-invariants --crab-opt-invariants-loc=block-entry adds the invariants that hold at each basic block entry, the options --crab-opt=add=invariants --crab-opt-invariants-loc=loop-header adds the invariants that hold at each loop header, while options --crab-opt=add-invariants --crab-opt-invariants-loc=after-load adds the invariants that hold right after each LLVM load instruction. To see the final LLVM bitcode just add the option -o out.bc.