diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/klee.h | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/include/klee/klee.h b/include/klee/klee.h index fafdd55f..07528595 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -16,7 +16,7 @@ #ifdef __cplusplus extern "C" { #endif - + /* Add an accesible memory object at a user specified location. It * is the users responsibility to make sure that these memory * objects do not overlap. These memory objects will also @@ -74,18 +74,18 @@ extern "C" { int line, const char *message, const char *suffix); - + /* called by checking code to get size of memory. */ size_t klee_get_obj_size(void *ptr); - + /* print the tree associated w/ a given expression. */ void klee_print_expr(const char *msg, ...); - + /* NB: this *does not* fork n times and return [0,n) in children. * It makes n be symbolic and returns: caller must compare N times. */ uintptr_t klee_choose(uintptr_t n); - + /* special klee assert macro. this assert should be used when path consistency * across platforms is desired (e.g., in tests). * NB: __assert_fail is a klee "special" function @@ -106,7 +106,7 @@ extern "C" { /* Return true if replaying a concrete test case using the libkleeRuntime library * Return false if executing symbolically in KLEE. */ - unsigned klee_is_replay(); + unsigned klee_is_replay(void); /* The following intrinsics are primarily intended for internal use @@ -136,7 +136,7 @@ extern "C" { accessible to the program. If some byte in the range is not accessible an error will be generated and the state terminated. - + The current implementation requires both address and size to be constants and that the range lie within a single object. */ void klee_check_memory_access(const void *address, size_t size); @@ -151,10 +151,10 @@ extern "C" { void klee_print_range(const char * name, int arg ); /* Open a merge */ - void klee_open_merge(); + void klee_open_merge(void); /* Merge all paths of the state that went through klee_open_merge */ - void klee_close_merge(); + void klee_close_merge(void); /* Get errno value of the current state */ int klee_get_errno(void); |