about summary refs log tree commit diff homepage
path: root/lib/Expr/ExprUtil.cpp
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-04-01 14:08:43 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-07-01 15:52:40 +0100
commit8a0f1af7500e10dadd97300f242424917d2e9902 (patch)
tree48d86b5a1dca9513e4bd1ba8a96441adc0be5169 /lib/Expr/ExprUtil.cpp
parentda5d238b5a78b54f89728132d71cfa6f8be16d21 (diff)
downloadklee-8a0f1af7500e10dadd97300f242424917d2e9902.tar.gz
Use constraint sets and separate metadata for timing solver invocation
Decouple ExecutionState from TimingSolver

Instead of providing an execution state to the timing solver use a set of
constraints and an additional object for metadata.

Fixes:
* correct accounting of metadata to a specific state
* accounting of all solver invocations (e.g. solver-getRange was not
accounted)
* allows to invoke the solver without a state (avoids costly copying of
states/constraints)
Diffstat (limited to 'lib/Expr/ExprUtil.cpp')
0 files changed, 0 insertions, 0 deletions