klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee.h
Go to the documentation of this file.
1 //===-- klee.h --------------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef __KLEE_H__
11 #define __KLEE_H__
12 
13 #include "stdint.h"
14 #include "stddef.h"
15 
16 #ifdef __cplusplus
17 extern "C" {
18 #endif
19 
20  /* Add an accesible memory object at a user specified location. It
21  is the users responsibility to make sure that these memory
22  objects do not overlap. These memory objects will also
23  (obviously) not correctly interact with external function
24  calls. */
25  void klee_define_fixed_object(void *addr, size_t nbytes);
26 
35  void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
36 
42  int klee_range(int begin, int end, const char *name);
43 
48  int klee_int(const char *name);
49 
53  void klee_silent_exit(int status);
54 
57  void klee_abort(void);
58 
67  void klee_report_error(const char *file,
68  int line,
69  const char *message,
70  const char *suffix);
71 
72  /* called by checking code to get size of memory. */
73  size_t klee_get_obj_size(void *ptr);
74 
75  /* print the tree associated w/ a given expression. */
76  void klee_print_expr(const char *msg, ...);
77 
78  /* NB: this *does not* fork n times and return [0,n) in children.
79  * It makes n be symbolic and returns: caller must compare N times.
80  */
81  uintptr_t klee_choose(uintptr_t n);
82 
83  /* special klee assert macro. this assert should be used when path consistency
84  * across platforms is desired (e.g., in tests).
85  * NB: __assert_fail is a klee "special" function
86  */
87 # define klee_assert(expr) \
88  ((expr) \
89  ? (void) (0) \
90  : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \
91 
92  /* Return true if the given value is symbolic (represented by an
93  * expression) in the current state. This is primarily for debugging
94  * and writing tests but can also be used to enable prints in replay
95  * mode.
96  */
97  unsigned klee_is_symbolic(uintptr_t n);
98 
99 
100  /* The following intrinsics are primarily intended for internal use
101  and may have peculiar semantics. */
102 
103  void klee_assume(uintptr_t condition);
104  void klee_warning(const char *message);
105  void klee_warning_once(const char *message);
106  void klee_prefer_cex(void *object, uintptr_t condition);
107  void klee_mark_global(void *object);
108 
109  /* Return a possible constant value for the input expression. This
110  allows programs to forcibly concretize values on their own. */
111 #define KLEE_GET_VALUE_PROTO(suffix, type) type klee_get_value##suffix(type expr)
112 
113  KLEE_GET_VALUE_PROTO(f, float);
114  KLEE_GET_VALUE_PROTO(d, double);
115  KLEE_GET_VALUE_PROTO(l, long);
116  KLEE_GET_VALUE_PROTO(ll, long long);
117  KLEE_GET_VALUE_PROTO(_i32, int32_t);
118  KLEE_GET_VALUE_PROTO(_i64, int64_t);
119 
120 #undef KLEE_GET_VALUE_PROTO
121 
122  /* Ensure that memory in the range [address, address+size) is
123  accessible to the program. If some byte in the range is not
124  accessible an error will be generated and the state
125  terminated.
126 
127  The current implementation requires both address and size to be
128  constants and that the range lie within a single object. */
129  void klee_check_memory_access(const void *address, size_t size);
130 
131  /* Enable/disable forking. */
132  void klee_set_forking(unsigned enable);
133 
134  /* klee_alias_function("foo", "bar") will replace, at runtime (on
135  the current path and all paths spawned on the current path), all
136  calls to foo() by calls to bar(). foo() and bar() have to exist
137  and have identical types. Use klee_alias_function("foo", "foo")
138  to undo. Be aware that some special functions, such as exit(),
139  may not always work. */
140  void klee_alias_function(const char* fn_name, const char* new_fn_name);
141 
142  /* Print stack trace. */
143  void klee_stack_trace(void);
144 
145 #ifdef __cplusplus
146 }
147 #endif
148 
149 #endif /* __KLEE_H__ */
void klee_alias_function(const char *fn_name, const char *new_fn_name)
int const char const char * suffix
Definition: klee.h:68
__attribute__((noreturn)) void klee_silent_exit(int status)
klee_abort - Abort the current KLEE process.
void klee_warning_once(const char *message)
int const char * message
Definition: klee.h:68
void klee_mark_global(void *object)
Definition: klee-replay.c:471
void klee_prefer_cex(void *object, uintptr_t condition)
Definition: klee-replay.c:409
void klee_assume(uintptr_t condition)
Definition: klee-replay.c:398
void klee_print_expr(const char *msg,...)
void klee_define_fixed_object(void *addr, size_t nbytes)
void klee_stack_trace(void)
void klee_report_error(const char *file, int line, const char *message, const char *suffix)
Definition: klee-replay.c:466
int klee_range(int begin, int end, const char *name)
Definition: klee-replay.c:443
unsigned klee_is_symbolic(uintptr_t n)
Definition: klee-replay.c:405
void noreturn
Definition: Common.h:31
int line
Definition: klee.h:68
void klee_set_forking(unsigned enable)
uintptr_t klee_choose(uintptr_t n)
size_t klee_get_obj_size(void *ptr)
#define KLEE_GET_VALUE_PROTO(suffix, type)
Definition: klee.h:111
void klee_warning(const char *message)
void klee_make_symbolic(void *addr, size_t nbytes, const char *name)
Definition: klee-replay.c:413
void klee_check_memory_access(const void *address, size_t size)
int klee_int(const char *name)