summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/InterpreterBorrows.ml16
-rw-r--r--src/InterpreterExpansion.ml41
2 files changed, 28 insertions, 29 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 =
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index b3a0e3f2..734160f9 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -428,34 +428,29 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
fun cf ctx ->
match rty with
(* "Regular" ADTs *)
- | T.Adt (T.AdtId def_id, regions, types) -> (
+ | T.Adt (T.AdtId def_id, regions, types) ->
(* Compute the expanded value - there should be exactly one because we
* don't allow to expand enumerations with strictly more than one variant *)
let expand_enumerations = false in
- match
+ let seel =
compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
def_id regions types ctx
- with
- | seel ->
- (* Check for branching *)
- assert (List.length seel <= 1 || allow_branching);
- (* Apply in the context *)
- let ctxl =
- List.map
- (fun see ->
- apply_symbolic_expansion_non_borrow config original_sv see ctx)
- seel
- in
- (* Continue *)
- let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in
- (* Synthesize *)
- let res = S.synthesize_symbolic_expansion original_sv resl in
- (* Return *)
- Some res
- | _ ->
- failwith
- "expand_symbolic_value_no_branching: the expansion lead to \
- branching")
+ in
+ (* Check for branching *)
+ assert (List.length seel <= 1 || allow_branching);
+ (* Apply in the context *)
+ let ctxl =
+ List.map
+ (fun see ->
+ apply_symbolic_expansion_non_borrow config original_sv see ctx)
+ seel
+ in
+ (* Continue *)
+ let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in
+ (* Synthesize *)
+ let res = S.synthesize_symbolic_expansion original_sv resl in
+ (* Return *)
+ Some res
(* Tuples *)
| T.Adt (T.Tuple, [], tys) ->
(* Generate the field values *)