diff options
author | Son Ho | 2022-01-06 18:20:24 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 18:20:24 +0100 |
commit | f3982cbe9782405b50b04c948ba7cb0bd89ef85f (patch) | |
tree | 2df26310f1e67980a8b6f6ff278bd71bf0791eb4 /src/InterpreterUtils.ml | |
parent | 7137e0733650e0ce37eff4ff805c95543f2c1161 (diff) |
Make the symbolic, borrow, region and abstration counters global and
stateful
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterUtils.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index fcc6050f..40ef0d05 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -45,11 +45,10 @@ let mk_place_from_var_id (var_id : V.VarId.id) : E.place = { var_id; projection = [] } (** Create a fresh symbolic value *) -let mk_fresh_symbolic_value (ty : T.rty) (ctx : C.eval_ctx) : - C.eval_ctx * V.symbolic_value = - let ctx, sv_id = C.fresh_symbolic_value_id ctx in +let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value = + let sv_id = C.fresh_symbolic_value_id () in let svalue = { V.sv_id; V.sv_ty = ty } in - (ctx, svalue) + svalue (** Create a typed value from a symbolic value. *) let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) : |