summaryrefslogtreecommitdiff
path: root/src/InterpreterUtils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/InterpreterUtils.ml')
-rw-r--r--src/InterpreterUtils.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 27d65a62..7a2e22f7 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -249,3 +249,13 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
obj#visit_typed_value () v;
false
with Found -> true
+
+(** Return the place used in an rvalue, if that makes sense.
+ This is used to compute meta-data, to find pretty names.
+ *)
+let rvalue_get_place (rv : E.rvalue) : E.place option =
+ match rv with
+ | Use (Copy p | Move p) -> Some p
+ | Use (Constant _) -> None
+ | Ref (p, _) -> Some p
+ | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> None