summaryrefslogtreecommitdiff
path: root/src/InterpreterStatements.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-12 20:28:08 +0100
committerSon Ho2022-01-12 20:28:08 +0100
commitcca136848b4310a02b78f2567d7c476df8c88025 (patch)
tree0816dd7790bd425e4150100e3722698eed80f2ae /src/InterpreterStatements.ml
parent14f7c587a6100fe0b2985e3afd123f79fde8d468 (diff)
Update end_borrow to check if there are loans in borrowed values
Diffstat (limited to '')
-rw-r--r--src/InterpreterStatements.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 23fe8d3b..cda682a3 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -810,7 +810,7 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
| ret_ty :: locals -> (ret_ty, locals)
| _ -> failwith "Unreachable"
in
- let ctx = C.ctx_push_var ctx ret_var (C.mk_bottom ret_var.var_ty) in
+ let ctx = C.ctx_push_var ctx ret_var (mk_bottom ret_var.var_ty) in
(* 2. Push the input values *)
let input_locals, locals = Utils.list_split_at locals def.A.arg_count in