summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoops.ml
diff options
context:
space:
mode:
authorSon Ho2024-03-08 21:35:27 +0100
committerSon Ho2024-03-08 21:35:27 +0100
commit4c29c8ac811da52bf630a24b04b5f9ca67aa67c6 (patch)
tree48b9a5bcb26b9b5152f857098d1b53165c0f032e /compiler/InterpreterLoops.ml
parent677d7678f6b88075332a7e9ee6befc7c887b6a4f (diff)
Fix a last issue
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterLoops.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 55836e48..1d774e0e 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -190,6 +190,9 @@ let eval_loop_symbolic (config : config) (meta : meta)
Moreover, we list the borrows in the same order as the loans (this
is important in {!SymbolicToPure}, where we expect the given back
values to have a specific order.
+
+ Also, we filter the backward functions which and
+ return nothing.
*)
let compute_abs_given_back_tys (abs : abs) : rty list =
let is_borrow (av : typed_avalue) : bool =