wrapper.tassadar.conf

[passes]
# "pre"-kind passes will be run before those supplied by cl
pre = module-print
pre = adaptor
# pre = decompose-functions
pre = mem2reg
# pre = force-inline
# pre = mem2reg
pre = gvl
pre = mem2reg
pre = meta-inserter
pre = annotation-processor
# pre = malloc-mutator
pre = indvars
pre = loop-simplify
pre = loop-rotate
pre = loop-deroll
pre = kill-uglygeps
pre = adce
pre = sccp
pre = ipsccp
pre = instcombine
pre = simplifycfg
pre = sink
pre = mergereturn
pre = mem2reg
pre = basicaa
pre = globalsmodref-aa
pre = scev-aa
pre = anders-aa
pre = module-print

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

[libs]
load = lib/andersen/lib/libAndersen.so

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

[logging]
ini = log.tests.ini

[run]
clangExec = /opt/clang/3.5.1/bin/clang
skipClangDriver = true

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

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

[analysis]
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 = false
psa-mode = one-for-all
psa-check-unreachable = false

collect-models = true

ext-functions = resources/stdLib.json

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

use-range-stores = true

[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 = 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
use-tactic = elim-uncnstr
use-tactic = ctx-simplify
use-tactic = propagate-values
use-tactic = max-bv-sharing
force-timeout = 60000
print-simplified = off