summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
authorSon Ho2021-11-29 22:23:08 +0100
committerSon Ho2021-11-29 22:23:08 +0100
commit46c0648948caa9f57cdd7e8561470e598eb814ab (patch)
tree5400dd3f19ed6eddca8a6fadcf98ea97986c60e5 /src/Interpreter.ml
parentfffbaa6e2d571343d2b8e49615d7de65d0783dc3 (diff)
Fix a small mistake
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r--src/Interpreter.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 38da6c25..00adf68a 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1329,9 +1329,7 @@ let rec collect_borrows_at_place (config : C.config) (access : access_kind)
let rec inspect_update v : unit =
match v.V.value with
| V.Concrete _ -> ()
- | V.Bottom ->
- failwith "Unreachable"
- (* note that we don't really need to fail here *)
+ | V.Bottom -> ()
| V.Symbolic _ ->
(* Nothing to do for symbolic values - note that if the value needs
to be copied, etc. we perform additional checks later *)