diff options
Diffstat (limited to 'compiler/InterpreterStatements.ml')
-rw-r--r-- | compiler/InterpreterStatements.ml | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 15962ee3..14dd59b1 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -39,12 +39,12 @@ let drop_value (config : C.config) (p : E.place) : cm_fun = let replace cf (v : V.typed_value) ctx = (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows it may contain *) - let mv = InterpreterPaths.read_place config access p ctx in + let mv = InterpreterPaths.read_place access p ctx in let dummy_id = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dummy_id mv in (* Update the destination to ⊥ *) let nv = { v with value = V.Bottom } in - let ctx = write_place config access p nv ctx in + let ctx = write_place access p nv ctx in log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" @@ -119,14 +119,14 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) : fun ctx -> (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows *) - let mv = InterpreterPaths.read_place config Write p ctx in + let mv = InterpreterPaths.read_place Write p ctx in let dest_vid = C.fresh_dummy_var_id () in let ctx = C.ctx_push_dummy_var ctx dest_vid mv in (* Write to the destination *) (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) assert (not (bottom_in_value ctx.ended_regions rv)); (* Update the destination *) - let ctx = write_place config Write p rv ctx in + let ctx = write_place Write p rv ctx in (* Debug *) log#ldebug (lazy @@ -540,9 +540,7 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) match (region_params, type_params, args) with | [], [ boxed_ty ], [ E.Move input_box_place ] -> (* Required type checking *) - let input_box = - InterpreterPaths.read_place config Write input_box_place ctx - in + let input_box = InterpreterPaths.read_place Write input_box_place ctx in (let input_ty = ty_get_box input_box.V.ty in assert (input_ty = boxed_ty)); @@ -783,7 +781,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = * checking the invariants *) let cc = greedy_expand_symbolic_values config in (* Sanity check *) - let cc = comp cc (Inv.cf_check_invariants config) in + let cc = comp cc Inv.cf_check_invariants in (* Evaluate *) let cf_eval_st cf : m_fun = @@ -1279,7 +1277,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) * (see the documentation of {!config} for more information) *) let cc = - if config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output + if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output then comp cc end_abs_with_no_loans else cc in @@ -1382,7 +1380,7 @@ and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun = * checking the invariants *) let cc = greedy_expand_symbolic_values config in (* Sanity check *) - let cc = comp_check_ctx cc (Inv.check_invariants config) in + let cc = comp_check_ctx cc Inv.check_invariants in (* Continue *) cc (cf res) in |