summaryrefslogtreecommitdiff
path: root/src/InterpreterExpressions.ml
diff options
context:
space:
mode:
authorSon Ho2022-09-22 17:44:04 +0200
committerSon Ho2022-09-22 17:44:04 +0200
commitf106fd4ad0a221611c840bf0af0b1c2ff23f3d0f (patch)
tree5542040036e571d75e2a42842dc68c628f7618dc /src/InterpreterExpressions.ml
parent53481c4326c0f3c17b372880a9a19ee2eb45907d (diff)
Make minor modifications
Diffstat (limited to '')
-rw-r--r--src/InterpreterExpressions.ml15
1 files changed, 6 insertions, 9 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 4598895e..4a4f3353 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -110,14 +110,13 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool)
ctx
(** Convert an operand constant operand value to a typed value *)
-let constant_to_typed_value (ty : T.ety)
- (cv : V.constant_value) : V.typed_value =
+let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value
+ =
(* Check the type while converting - we actually need some information
- * contained in the type *)
+ * contained in the type *)
log#ldebug
(lazy
- ("constant_to_typed_value:" ^ "\n- cv: "
- ^ PV.constant_value_to_string cv));
+ ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv));
match (ty, cv) with
(* Scalar, boolean... *)
| T.Bool, Bool v -> { V.value = V.Concrete (Bool v); ty }
@@ -128,10 +127,8 @@ let constant_to_typed_value (ty : T.ety)
assert (int_ty = v.int_ty);
assert (check_scalar_value_in_range v);
{ V.value = V.Concrete (V.Scalar v); ty }
- (* Remaining cases (invalid) - listing as much as we can on purpose
- (allows to catch errors at compilation if the definitions change) *)
- | _, _ ->
- failwith "Improperly typed constant value"
+ (* Remaining cases (invalid) *)
+ | _, _ -> failwith "Improperly typed constant value"
(** Reorganize the environment in preparation for the evaluation of an operand.