Wiki

Clone wiki

llStar / Usage

llStar takes as input a bitcode program, a set of specifications for the functions it declares and defines, and a set of logic rules to reason about symbolic states. It then attempts to prove the specifications correct.

llStar can output various diagnoses on the console. By default, it also records proof steps in an output directory, together with a .dot file describing the symbolic execution of all the functions in the bitcode module.

The options of llStar are described by running llstar -help:

Usage: llstar [options] source_file
  -q Run in quiet mode
  -v Verbose proofs
  -log Set log modes (exec,load,logic,phase,prove,specs,symb,parse,cfg,smt)
  -nosmt Don't use the SMT solver
  -p SMT solver path
  -b Background predicate
  -ai Colon separated list of AI plugins filenames
  -join On abstraction join heaps over their numeric part
  -memleaks Checks for memory leaks (default: true)
  -d Set debug modes (deprecated, see -log)
  -l logic file name (default: $SOURCE.logic or logic)
  -s spec file name (default: $SOURCE.spec or spec)
  -a abstraction rules file name (default: $SOURCE.abs or abs)
  -abduct_file abduction rules file name (default: $SOURCE.abduct or abduct)
  -abduct toggles abduction on
  -autostructs enable automatic struct-folding/unfolding rules generation
  -autolists enable automatic list abstraction rules generation
  -noautostructs disable automatic struct-folding/unfolding rules generation
  -noautolists disable automatic list abstraction rules generation
  -outdir directory where to output llStar results
  -outputll output ASCII bitcode to specified file (leave empty to disable) (default: [outdir]/[bitcode_base_name].ll)
  -runopts run a few (hardcoded) LLVM optimisation passes before verification (default: false)
  -help  Display this list of options
  --help  Display this list of options

Updated