From 2cb1bf002d7d91634c49ed5e5e05a6409bb539a5 Mon Sep 17 00:00:00 2001 From: Joe Ranweiler Date: Sat, 24 Feb 2018 14:38:26 -0800 Subject: [PATCH] Add impl for `klee_choose()` --- src/include/deepstate/Klee.h | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/include/deepstate/Klee.h b/src/include/deepstate/Klee.h index 3f90341..2c8a4c5 100644 --- a/src/include/deepstate/Klee.h +++ b/src/include/deepstate/Klee.h @@ -52,8 +52,16 @@ static void klee_print_expr(const char *msg, ...) { /* See impl in `runtime/Runtest/intrinsics.c`. */ } -/* TODO(joe): Implement */ -static uintptr_t klee_choose(uintptr_t n); +static uintptr_t klee_choose(uintptr_t n) { + uintptr_t out; + klee_make_symbolic(&out, sizeof(out), "klee_choose"); + + if (n <= out) { + klee_silent_exit(0); + } + + return out; +} /* Unsupported. */ /* static unsigned klee_is_symbolic(uintptr_t n); */