diff options
| author | Son Ho | 2022-01-05 07:47:36 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-05 07:47:36 +0100 |
| commit | 3114dea5e2155eeb52581952159107dfa239ccdc (patch) | |
| tree | db93ef951d1c167ae6241e2dd3da0440da5d2a97 /src/InterpreterUtils.ml | |
| parent | 1e83bc8b14c97170833a5af721e58ff746d61317 (diff) | |
Start inserting calls to dummy synthesis functions in Interpreter.ml
Diffstat (limited to 'src/InterpreterUtils.ml')
| -rw-r--r-- | src/InterpreterUtils.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 9e891348..4633664f 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -620,3 +620,10 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue) (* Check that we updated at least one borrow *) assert !r; ctx + +(** TODO: move to InterpreterSymbolic or sth *) +type symbolic_expansion = + | SeConcrete of V.constant_value + | SeAdt of (T.VariantId.id option * V.symbolic_proj_comp list) + | SeMutRef of V.BorrowId.id * V.symbolic_proj_comp + | SeSharedRef of V.BorrowId.set_t * V.symbolic_proj_comp |