diff options
author | Son Ho | 2022-01-06 10:43:08 +0100 |
---|---|---|
committer | Son Ho | 2022-01-06 10:43:08 +0100 |
commit | 9de2ecb71504ff0c31f0825dbe5d54ddf3d9d4a1 (patch) | |
tree | 1bc01541aa4612d19da1943fc750280814389ab3 /src | |
parent | ea2d6637cfd9f6e17d1b411fb03e9f6c50edc331 (diff) |
Move some definitions
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterExpressions.ml | 20 | ||||
-rw-r--r-- | src/InterpreterStatements.ml | 20 |
2 files changed, 20 insertions, 20 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 83651ba5..1b2a9859 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -31,26 +31,6 @@ let prepare_rplace (config : C.config) (access : access_kind) (p : E.place) let v = read_place_unwrap config access p ctx in (ctx, v) -(** Drop a value at a given place *) -let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx - = - L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); - (* Prepare the place (by ending the loans, then the borrows) *) - let ctx, v = prepare_lplace config p ctx in - (* Replace the value with [Bottom] *) - let nv = { v with value = V.Bottom } in - let ctx = write_place_unwrap config Write p nv ctx in - ctx - -(** Assign a value to a given place *) -let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) - (p : E.place) : C.eval_ctx = - (* Prepare the destination *) - let ctx, _ = prepare_lplace config p ctx in - (* Update the destination *) - let ctx = write_place_unwrap config Write p v ctx in - ctx - (** Convert a constant operand value to a typed value *) let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) (cv : E.operand_constant_value) : V.typed_value = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index ec61b5e0..d52ec0e7 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -22,6 +22,26 @@ open InterpreterExpressions (** Result of evaluating a statement *) type statement_eval_res = Unit | Break of int | Continue of int | Return +(** Drop a value at a given place *) +let drop_value (config : C.config) (ctx : C.eval_ctx) (p : E.place) : C.eval_ctx + = + L.log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); + (* Prepare the place (by ending the loans, then the borrows) *) + let ctx, v = prepare_lplace config p ctx in + (* Replace the value with [Bottom] *) + let nv = { v with value = V.Bottom } in + let ctx = write_place_unwrap config Write p nv ctx in + ctx + +(** Assign a value to a given place *) +let assign_to_place (config : C.config) (ctx : C.eval_ctx) (v : V.typed_value) + (p : E.place) : C.eval_ctx = + (* Prepare the destination *) + let ctx, _ = prepare_lplace config p ctx in + (* Update the destination *) + let ctx = write_place_unwrap config Write p v ctx in + ctx + (** Updates the discriminant of a value at a given place. There are two situations: |