diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-11-04 16:42:51 +0000 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-02-19 12:05:22 +0000 |
| commit | 41ee94afe029c891e8960141ba71a3451a42d6ae (patch) | |
| tree | 34b07f757751cac3097a3a2736e1166e1e346787 /lib/Solver | |
| parent | 9cfa329a77d3dfec4746ca307c6da1b3e904cbfa (diff) | |
| download | klee-41ee94afe029c891e8960141ba71a3451a42d6ae.tar.gz | |
Use `ref<>` for MemoryObject handling
This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 3112495d..376ffe25 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -182,7 +182,7 @@ MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root, if (!hashed) { un_expr = evaluate(_solver, metaSMT::logic::Array::store( - getArrayForUpdate(root, un->next), + getArrayForUpdate(root, un->next.get()), construct(un->index, 0), construct(un->value, 0))); _arr_hash.hashUpdateNodeExpr(un, un_expr); } @@ -680,10 +680,10 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) { assert(re && re->updates.root); *width_out = re->updates.root->getRange(); // FixMe call method of Array - res = evaluate(_solver, - metaSMT::logic::Array::select( - getArrayForUpdate(re->updates.root, re->updates.head), - construct(re->index, 0))); + res = evaluate(_solver, metaSMT::logic::Array::select( + getArrayForUpdate(re->updates.root, + re->updates.head.get()), + construct(re->index, 0))); break; } |