diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-04-01 14:08:43 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-07-01 15:52:40 +0100 |
| commit | 8a0f1af7500e10dadd97300f242424917d2e9902 (patch) | |
| tree | 48d86b5a1dca9513e4bd1ba8a96441adc0be5169 /lib/Core/ExecutionState.cpp | |
| parent | da5d238b5a78b54f89728132d71cfa6f8be16d21 (diff) | |
| download | klee-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/Core/ExecutionState.cpp')
| -rw-r--r-- | lib/Core/ExecutionState.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 0b848f41..5e95ca9b 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -101,7 +101,6 @@ ExecutionState::ExecutionState(const ExecutionState& state): depth(state.depth), addressSpace(state.addressSpace), constraints(state.constraints), - queryCost(state.queryCost), pathOS(state.pathOS), symPathOS(state.symPathOS), coveredLines(state.coveredLines), |