aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tools/klee/main.cpp7
1 files changed, 6 insertions, 1 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 9d445ac7..4bbf85f8 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -694,7 +694,12 @@ static const char *modelledExternals[] = {
"klee_check_memory_access",
"klee_define_fixed_object",
"klee_get_errno",
- "klee_get_value",
+ "klee_get_valuef",
+ "klee_get_valued",
+ "klee_get_valuel",
+ "klee_get_valuell",
+ "klee_get_value_i32",
+ "klee_get_value_i64",
"klee_get_obj_size",
"klee_is_symbolic",
"klee_make_symbolic",