summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-04 18:15:45 +0100
committerSon Ho2022-01-04 18:15:45 +0100
commitfb482999dd7b26a3910ae9ee2dfe650c99cc140f (patch)
tree38c7509dc9319d6f30da019e7052ba72a6014838 /src
parent4eac971ff729dde4054a4e5473e0de1a156ed6ca (diff)
Make a minor modification
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 745142b6..1c54d9a4 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3814,6 +3814,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
( ctx,
{ V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }
)))
+ | Symbolic _ -> raise Unimplemented
| _ -> failwith "Invalid input for `discriminant`")
| E.Aggregate (aggregate_kind, ops) -> (
(* Evaluate the operands *)