From 63f22739f929c24f96a43d9c058453e553c7f462 Mon Sep 17 00:00:00 2001 From: Joe Ranweiler Date: Sat, 24 Feb 2018 14:04:28 -0800 Subject: [PATCH] Impl supported `klee_get_val` functions We will extend the DeepState API to support the others. --- src/include/deepstate/Klee.h | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h index 2d34f59..9408f67 100644 --- a/src/include/deepstate/Klee.h +++ b/src/include/deepstate/Klee.h @@ -80,23 +80,27 @@ static void klee_posix_prefer_cex(void *object, uintptr_t condition) { #define KLEE_GET_VALUE(suffix, type) type klee_get_value ## suffix(type val) -/* TODO(joe): Implement */ -static KLEE_GET_VALUE(f, float); +/* Unsupported. */ +/* static KLEE_GET_VALUE(f, float); */ + +/* Unsupported. */ +/* static KLEE_GET_VALUE(d, double); */ + +static KLEE_GET_VALUE(l, long) { + DeepState_MinInt(val); +} + +/* Unsupported. */ +/* static KLEE_GET_VALUE(ll, long long) */ /* TODO(joe): Implement */ -static KLEE_GET_VALUE(d, double); +static KLEE_GET_VALUE(_i32, int32_t) { + DeepState_MinInt(val); +} /* TODO(joe): Implement */ -static KLEE_GET_VALUE(l, long); - -/* TODO(joe): Implement */ -static KLEE_GET_VALUE(ll, long long); - -/* TODO(joe): Implement */ -static KLEE_GET_VALUE(_i32, int32_t); - -/* TODO(joe): Implement */ -static KLEE_GET_VALUE(_i64, int64_t); +/* Unsupported. */ +/* static KLEE_GET_VALUE(_i64, int64_t); */ #undef KLEE_GET_VALUE