wrapper.conf

[passes]
# "pre"-kind passes will be run before those supplied by cl
pre = mem2reg
# pre = module-print
pre = malloc-mutator
pre = function-bitcast-killer
pre = module-print
pre = ir-interpreter

pre = adaptor
pre = kill-struct-values
pre = mem2reg
# pre = force-inline
# pre = mem2reg
# pre = gvl
pre = mem2reg
pre = meta-inserter
pre = mem2reg
pre = decompose-functions
pre = mem2reg
pre = annotation-processor
pre = malloc-mutator
pre = indvars
pre = loop-simplify
pre = loop-rotate
pre = loop-deroll
pre = loop-breaker
# pre = kill-uglygeps
# pre = ipsccp
pre = sccp
pre = dce
pre = instcombine
pre = simplifycfg
pre = sink
pre = mergereturn
pre = mem2reg
pre = basicaa
pre = globalsmodref-aa
pre = scev-aa
# pre = anders-aa
# pre = ds-aa
pre = module-print
# pre = decompiler

# post = module-print # "post"-kind passes will be run after those supplied by cl
# post = tassadar-checker
# post = reanimator
post = defect-summary
post = location-summary
# post = decompiler
# post = stats

[libs]
# load = lib/andersen/lib/libAndersen.so
# load = lib/dsaa/lib/libDsaa.so

[opt]
# load = -inline-threshold=0
# load = -debug
# load = -debug-pass=Executions
# load = -unroll-threshold=100500
# load = -unroll-count=10
# load = -unroll-allow-partial=true
# load = -unroll-runtime=true

[logging]
ini = log.ini

[run]
clangExec = /opt/clang/3.5.1/bin/clang
skipClangDriver = false
compileOnly = false

[output]
# dump-output = json
# dump-output-file = %s.report
# dump-coverage = false
# dump-coverage-file = %s.coverage
# dump-smt2-states = z3-states

smt-query-logging = off

[z3]
params = z3.params
tactics = z3.tactics

[analysis]
smt-engine = boolector

deroll-count = 3
# max-deroll-count = 1
deroll-backstab = yes
adaptive-deroll = yes

default-malloc-size = 2048
# nullable-mallocs = false
memory-defaults-to-unknown = true
skip-static-init = true
psa-mode = one-for-all
psa-check-unreachable = false
optimize-states = true

collect-models = true

ext-functions = resources/stdLib.json
ext-functions = resources/pthread.json
ext-functions = resources/posix.json

sanity-check = false
sanity-check-timeout = 5
dd-number = 1000
dd-timeout = 5

use-range-stores = false

root-function = main

persistent-defect-data = true

do-aggressive-choice-optimization = true

use-local-aa = on
do-slicing = on
memory-spaces = on

[summary]
# sum-mode = interpol
# sum-mode = inline
# model-sampling = false
sampling-solver = z3
# sampling-solver = mathsat
sampling-count-limit = 16
sampling-attempt-limit = 32
# sampling-attempt-limit = 100

[adapt]
assert = __VERIFIER_assert
assert = ASSERT
assume = __VERIFIER_assume
assume = ASSUME
error-label = ERROR
# break-undefs = true

[checkers]
# includes = find_alignment
# includes = main
# includes = __main
# includes = mainFunc
# excludes = ASSERT
# excludes = ASSUME

[statistics]
show = *.*

[executor]
function = main
function = __main

[decompose-functions]
exclude = strlen
exclude = strcpy
# exclude = strchr
exclude = memchr

[z3]
aggressive-simplify = off
force-timeout = 3000
print-simplified = off
log-formulae = on

[portfolio]
force-timeout = 1000
use-solver = boolector
use-solver = z3
use-solver = cvc4

[database]
# Wat?

[absint]
numeric = octagon

init-globals = on

enable-ps-interpreter = off
enable-ir-interpreter = off

print-module = off
enable-octagon-printing = off
checker-logging = off