summaryrefslogtreecommitdiff
path: root/compiler/InterpreterExpansion.ml
diff options
context:
space:
mode:
authorSon Ho2022-12-02 01:09:05 +0100
committerSon HO2023-02-03 11:21:46 +0100
commit43163a5abc4e79d66f517a473e5ee9c4c3410622 (patch)
treeb3f3c641dbccbaf9b738a772844a35b7190e30b2 /compiler/InterpreterExpansion.ml
parentaef15fb2f961df4f935c659d85ff9982fc446cc2 (diff)
Remove the meta-values from the shared and reserved borrow values
Diffstat (limited to 'compiler/InterpreterExpansion.ml')
-rw-r--r--compiler/InterpreterExpansion.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 8a563351..9a61d917 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -340,8 +340,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
method! visit_Symbolic env sv =
if same_symbolic_id sv original_sv then
let bid = fresh_borrow () in
- V.Borrow
- (V.SharedBorrow (mk_typed_value_from_symbolic_value shared_sv, bid))
+ V.Borrow (V.SharedBorrow bid)
else super#visit_Symbolic env sv
method! visit_Abs proj_regions abs =