Comment out unsupported KLEE functions
We don't declare the functions to ensure compilation fails fast, not linking. We keep the commented prototype for the sake of documentation, instead of just deleting it. We may also eventually be able to impl the functions if we extend the DeepState API.
This commit is contained in:
parent
994d29b2d3
commit
27b2a490ee
@ -23,8 +23,8 @@
|
||||
|
||||
DEEPSTATE_BEGIN_EXTERN_C
|
||||
|
||||
/* TODO(joe): Implement */
|
||||
static void klee_define_fixed_object(void *addr, size_t nbytes);
|
||||
/* Unsupported. */
|
||||
/* static void klee_define_fixed_object(void *addr, size_t nbytes); */
|
||||
|
||||
static void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
|
||||
DeepState_SymbolizeData(addr, addr + nbytes);
|
||||
@ -40,8 +40,8 @@ DEEPSTATE_NORETURN static void klee_silent_exit(int status) {
|
||||
exit(status);
|
||||
}
|
||||
|
||||
/* TODO(joe): Implement */
|
||||
static size_t klee_get_obj_size(void *ptr);
|
||||
/* Unsupported. */
|
||||
/* static size_t klee_get_obj_size(void *ptr); */
|
||||
|
||||
static void klee_print_expr(const char *msg, ...) {
|
||||
/* KLEE debugging command, no DeepState equivalent. */
|
||||
@ -54,8 +54,8 @@ static uintptr_t klee_choose(uintptr_t n);
|
||||
/* TODO(joe): Implement */
|
||||
static unsigned klee_is_symbolic(uintptr_t n);
|
||||
|
||||
/* TODO(joe): Implement */
|
||||
static void klee_assume(uintptr_t condition);
|
||||
/* Unsupported. */
|
||||
/* static void klee_assume(uintptr_t condition); */
|
||||
|
||||
static void klee_warning(const char *message) {
|
||||
DeepState_Log(DeepState_LogWarning, message);
|
||||
@ -73,8 +73,8 @@ static void klee_posix_prefer_cex(void *object, uintptr_t condition) {
|
||||
/* KLEE engine command, no DeepState equivalent. */
|
||||
}
|
||||
|
||||
/* TODO(joe): Implement */
|
||||
static void klee_mark_global(void *object);
|
||||
/* Unsupported. */
|
||||
/* static void klee_mark_global(void *object); */
|
||||
|
||||
/* TODO(joe): Implement */
|
||||
static KLEE_GET_VALUE(f, float);
|
||||
@ -94,15 +94,16 @@ static KLEE_GET_VALUE(_i32, int32_t);
|
||||
/* TODO(joe): Implement */
|
||||
static KLEE_GET_VALUE(_i64, int64_t);
|
||||
|
||||
/* TODO(joe): Implement */
|
||||
static void klee_check_memory_access(const void *address, size_t size);
|
||||
/* Unsupported. */
|
||||
/* static void klee_check_memory_access(const void *address, size_t size); */
|
||||
|
||||
static void klee_set_forking(unsigned enable) {
|
||||
/* KLEE engine command, no DeepState equivalent. */
|
||||
}
|
||||
|
||||
/* TODO(joe): Implement */
|
||||
static void klee_alias_function(const char *fn_name, const char *new_fn_name);
|
||||
/* Unsupported. */
|
||||
/* static void
|
||||
* klee_alias_function(const char *fn_name, const char *new_fn_name); */
|
||||
|
||||
static void klee_stack_trace(void) {
|
||||
/* KLEE debugging command, no DeepState equivalent. */
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user