diff options
Diffstat (limited to 'src/InterpreterBorrows.ml')
| -rw-r--r-- | src/InterpreterBorrows.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 38447fd1..eea60833 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -952,9 +952,11 @@ and end_borrows (config : C.config) (chain : borrow_or_abs_ids) (allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) : cm_fun = fun cf -> - V.BorrowId.Set.fold - (fun id cf -> end_borrow config chain allowed_abs id cf) - lset cf + (* This is not necessary, but we prefer to reorder the borrow ids, + * so that we actually end from the smallest id to the highest id - just + * a matter of taste, and may make debugging easier *) + let ids = V.BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in + List.fold_left (fun cf id -> end_borrow config chain allowed_abs id cf) cf ids and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) (abs_id : V.AbstractionId.id) : cm_fun = @@ -1035,9 +1037,11 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) and end_abstractions (config : C.config) (chain : borrow_or_abs_ids) (abs_ids : V.AbstractionId.Set.t) : cm_fun = fun cf -> - V.AbstractionId.Set.fold - (fun id cf -> end_abstraction config chain id cf) - abs_ids cf + (* This is not necessary, but we prefer to reorder the abstraction ids, + * so that we actually end from the smallest id to the highest id - just + * a matter of taste, and may make debugging easier *) + let abs_ids = V.AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in + List.fold_left (fun cf id -> end_abstraction config chain id cf) cf abs_ids and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids) (abs_id : V.AbstractionId.id) : cm_fun = |