CPAchecker configuration
========================

Configuration of CPAchecker is done via command-line arguments and
configuration files in the syntax of Java properties files.


Command-line options
--------------------
Several configuration options can be set on the command-line with the
following arguments (see below to learn what the options mean):

-help			print list of command-line argumments and exit
-config <FILE>		sets configuration file name
-cpas <CPAS>		sets "cpa = compositeCPA.CompositeCPA" and "CompositeCPA.cpas = <CPAS>"
-outputpath <DIR>	sets "output.path = <DIR>"
-logfile <FILE>		sets "log.file = <FILE>"
-nolog			sets "log.level = OFF" and "log.consoleLevel = OFF"
-entryfunction <FUNC>	sets "analysis.entryFunction = <FUNC>"
-dfs			sets "analysis.traversal = DFS"
-bfs			sets "analysis.traversal = BFS"
-topsort		sets "analysis.traversal = TOPSORT"
-setprop <KEY>=<VALUE>	sets any option: "KEY = VALUE"

Either "-help", "-config" or "-cpas" has to be specified.

If an option appears on the command line as well as in the configuration file,
the value from the command line overrides the one from the file.

All other arguments to CPAchecker are interpreted as code files that should be
analyzed (option analysis.programs). However, currently only one such file has
to be specified.


Specifying the CPA(s)
---------------------
The CPA that CPAchecker uses is specified with the "cpa" option (default:
compositeCPA.CompositeCPA). The syntax of the value is "package.ClassName Alias",
where the alias is an optional unique identifier for this instance of the
CPA. Without an alias, the class name is used as identifier. Configuration
options that should be used for only one instance of a CPA can be prefixed
with "alias.". Their values override the options without this prefix.

Wrapper CPAs like ARTCPA and CompositeCPA take one option "cpa" or "cpas"
to specify the wrapped CPA, depending whether this CPA wraps one or
several other CPAs (the latter is only used for CompositeCPA). This option
has to be prefixed with the identifier of the CPA as described above.

A simple example (the first line could be ommitted as it's the default):
cpa = compositeCPA.CompositeCPA
CompositeCPA.cpas = cpa.location.LocationCPA, cpa.explicit.ExplicitAnalysisCPA explicitCPA
explicitCPA.cpas.explicit.threshold = 10

A more complex example:
cpa = cpa.art.ARTCPA art
art.cpa = compositeCPA.CompositeCPA composite
composite.cpas = cpa.location.LocationCPA, cpa.symbpredabs.SymbPredAbsCPA


Valid configuration options and default values
----------------------------------------------

# directory to put all output files in
output.path = test/output/

# name of the log file
log.file = CPALog.txt

# Possible log levels in descending order (lower levels include higher ones): 
# OFF: 		no logs published
# SEVERE: 	error messages
# WARNING: 	warnings
# INFO: 	messages
# FINE: 	logs on main application level
# FINER: 	logs on central CPA algorithm level
# FINEST: 	logs published by specific CPAs
# ALL: 		debugging information
# Care must be taken with levels of FINER or lower, as output files may 
# become quite large and memory usage might become an issue. 

# log level of file output
log.level = OFF

# log level of console output
log.consoleLevel = INFO

# single levels to be excluded from being logged
log.fileExclude =
log.consoleExclude =

# C code file to analyze, normally given on command line
analysis.programs = 

# C dialect for parser (GNUC or C99)
parser.dialect = GNUC

# combine series of simple statements in the CFA (currently not suppported)
cfa.combineBlockStatements = false

# remove all declarations from CFA
cfa.removeDeclarations = false

# don't create interprocedural call/return edges for external function calls
analysis.noExternalCalls = true

# run interprocedural analysis
analysis.interprocedural = true

# add declarations for global variables before entry function
analysis.useGlobalVars = true

# remove paths from CFA that cannot lead to an "error location"
cfa.removeIrrelevantForErrorLocations = false

# export CFA as .dot file
cfa.export = true
cfa.file = cfa.dot

# entry function
analysis.entryFunction = main

# use location mapped reached set
# (faster, elements with different locations cannot be merged)
cpa.useSpecializedReachedSet = true

# use assumption collecting algorithm
analysis.useAssumptionCollector = false

# use CEGAR algorithm for lazy counter-example guided analysis
# You need to specify a refiner with the cegar.refiner option.
# Currently all refiner require the use of the ARTCPA.
analysis.useRefinement = false

# use CBMC to double-check counter-examples
analysis.useCBMC = false

# Which CPA to use?
cpa = compositeCPA.CompositeCPA

# which strategy to adopt for visiting states? dfs, bfs, or topsort
analysis.traversal = dfs

# stop after the first error has been found
analysis.stopAfterError = true

# print reached set to text file
reachedSet.export = true
reachedSet.file = reached.txt

#------------------------------------------------------------------------------
# Algorithm specific options
#------------------------------------------------------------------------------

# write collected assumptions to file
assumptions.export = false
assumptions.file = assumptions.txt

# Which refinement algorithm to use? (give class name, required for CEGAR)
cegar.refiner =

# completely restart analysis on refinement by removing everything from
# the reached set
cegar.restartOnRefinement = false

#------------------------------------------------------------------------------
# CPA specific options
#------------------------------------------------------------------------------

# which merge operator to use for ARTCPA? only use sep here if all other CPAs also use sep
cpas.art.merge = join

# export final ART as .dot file
ART.export = true
ART.file = ART.dot

# which merge operator to use for ExplicitAnalysisCPA (join or sep)
cpas.explicit.merge = sep

# threshold for amount of different values that are tracked for one variable in
# ExplicitAnalysisCPA (0 means infinitely)
cpas.explicit.threshold = 0

# file with automaton specification for ObserverAnalysisCPA
observerAnalysis.inputFile = 

# which merge operator to use for PointerAnalysisCPA? (join or sep)
cpas.pointeranalysis.merge = sep

# print warnings during analysis when unsafe pointer operations are found
cpas.pointeranalysis.printWarnings = true

# which merge operator to use for UninitializedVariablesCPA? (join or sep)
uninitVars.merge = sep

# which stop operator to use for UninitializedVariablesCPA (join or sep)
uninitVars.stop = sep

# print warnings during analysis when uninitialized variables are used
uninitVars.printWarnings = true

#------------------------------------------------------------------------------
# Options for Predicate Abstraction
#------------------------------------------------------------------------------

# collect and print detailed statistics (at the moment, only the
# number of abstraction steps for each location)
cpas.symbpredabs.explicit.extendedStats = false

# which solver to use? (mathsat, simplify, yices)
cpa.symbpredabs.explicit.abstraction.solver = mathsat

# which interpolating solver to use for interpolant generation? (mathsat, csisat)
cpa.symbpredabs.interpolatingProver = mathsat

# don't use abstraction refinement, but read predicates from the map specified
# with fixedPredMap option
cpas.symbpredabs.abstraction.norefinement = false

# when not using refinement, where to get the list of predicates from
# (in MSAT format)
cpas.symbpredabs.abstraction.fixedPredMap = 

# cache queries to mathsat and BDD entailment checks
cpas.symbpredabs.mathsat.useCache = true


# initialize all variables to 0 when they are declared
cpas.symbpredabs.initAllVars = false

# if initAllVars is true, we get rid of all non-determinism. This might not be
# desirable. If the following property is set to a non-empty value, all
# variables starting with this prefix will not be initialized automatically
cpas.symbpredabs.noAutoInitPrefix = __BLAST_NONDET

# use uninterpreted functions for *, & and array access
cpas.symbpredabs.mathsat.lvalsAsUif = false

# encode program variables as INTEGERs in MathSAT, instead of using
# REALs. Since interpolation is not really supported by the laz solver, when
# computing interpolants we still use the LA solver, but encoding variables
# as ints might still be a good idea: we can tighten strict inequalities, and
# split negated equalities
cpas.symbpredabs.mathsat.useIntegers = false


# maximum blocksize before abstraction is forced
# (non-negative number, special values: 0 = don't check threshold, 1 = SBE)
cpas.symbpredabs.blk.threshold = 0

# force abstractions on function call/return
cpas.symbpredabs.blk.functions = true

# force abstractions for each loop iteration
cpas.symbpredabs.blk.loops = true

# require that both the threshold and (functions or loops) have to be fulfilled to compute an abstraction
cpas.symbpredabs.blk.requiredThresholdAndLBE = false


# maximum blocksize before a satisfiability check is done
# (non-negative number, 0 means never, if positive should be smaller than blocksize)
cpas.symbpredabs.satCheckBlockSize = 0


# whether to include the symbolic path formula in the coverage checks or do only the fast abstract checks
cpas.symbpredabs.symbolicCoverageCheck = false

# use a combination of theories (this is incomplete)
cpas.symbpredabs.mathsat.useDtc = false

# try to add some useful static-learning-like axioms for bitwise
# operations (which are encoded as UFs): essentially, we simply collect all
# the numbers used in bitwise operations, and add axioms like (0 & n = 0)
cpas.symbpredabs.useBitwiseAxioms = false

# apply deletion-filter to the abstract counterexample, to get a
# minimal set of blocks, before applying interpolation-based refinement
cpas.symbpredabs.explicit.getUsefulBlocks = false

# use incremental search in counterexample analysis, to find the minimal infeasible prefix
cpas.symbpredabs.shortestCexTrace = false

# if shortestCexTrace is used, start from the end with the incremental search
cpas.symbpredabs.shortestCexTraceUseSuffix = false

# if shortestCexTrace is used, alternatingly search from start and end of the trace
cpas.symbpredabs.shortestCexTraceUseZigZag = false

# whether to use Boolean (false) or Cartesian (true) abstraction
cpas.symbpredabs.abstraction.cartesian = false

# split arithmetic equalities when extracting predicates from interpolants
cpas.symbpredabs.refinement.splitItpAtoms = false

# mimick the behaviour of Blast on refinement: collect all the predicates from
# all the cuts of the abstract counterexample, and add all of them to all relevant
# locations
cpas.symbpredabs.refinement.useBlastWay = false

# refinement will try to build "well-scoped" predicates, by cutting spurious
# traces as explained in Section 5.2 of the paper "Abstractions From Proofs"
# (this does not work with function inlining)
cpas.symbpredabs.refinement.addWellScopedPredicates = false

# refinement will add all discovered predicates to all the locations in the abstract trace
cpas.symbpredabs.refinement.addPredicatesGlobally = false

cpas.symbpredabs.abstraction.explicit.nonAtomicPredicates = false


# where to dump the counterexample formula in case the error location is reached
cpas.symbpredabs.refinement.msatCexFile = cex.msat

# where to dump the final predicate map in case the error location is not reached
cpas.symbpredabs.refinement.finalPredMapFile = predmap.txt

# dump the abstraction formulas in both .msat and .smv formats if they took to long
cpas.symbpredabs.mathsat.dumpHardAbstractionQueries = false

# dump queries made to Simplify theorem prover
cpas.symbpredabs.explicit.abstraction.simplifyDumpQueries = false

# dump all interpolation problems
cpas.symbpredabs.dumpInterpolationProblems = false
