klee.h File Reference

Go to the source code of this file.

Defines
#define	klee_assert(expr)
Functions
void	klee_define_fixed_object (void *addr, unsigned nbytes)
void	klee_make_symbolic (void *addr, unsigned nbytes, const char *name)
int	klee_range (int begin, int end, const char *name)
int	klee_int (const char *name)
	__attribute__ ((noreturn)) void klee_abort(void)
	klee_abort - Abort the current KLEE process.
unsigned	klee_get_obj_size (void *ptr)
void	klee_print_expr (const char *msg,...)
unsigned	klee_choose (unsigned n)
unsigned	klee_is_symbolic (unsigned n)
void	klee_assume (unsigned condition)
void	klee_warning (const char *message)
void	klee_warning_once (const char *message)
void	klee_prefer_cex (void *object, unsigned condition)
void	klee_mark_global (void *object)
unsigned	klee_get_value (unsigned expr)
void	klee_check_memory_access (const void *address, unsigned size)
void	klee_set_forking (unsigned enable)
void	klee_alias_function (const char *fn_name, const char *new_fn_name)
Variables
int	line
int const char *	message
int const char const char *	suffix

---

Define Documentation

#define klee_assert

(

expr

)

Value:

((expr)                                                               \
   ? (void) (0)                                                         \
   : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__))    \

Definition at line 84 of file klee.h.

---

Function Documentation

__attribute__

(

(noreturn)

)

klee_abort - Abort the current KLEE process.

klee_silent_exit - Terminate the current KLEE process without generating a test file.

klee_report_error - Report a user defined error and terminate the current KLEE process.

• file - The filename to report in the error message.
• line - The line number to report in the error message.
• message - A string to include in the error message.
• suffix - The suffix to use for error files.

Referenced by klee::Executor::initializeGlobals().

Here is the caller graph for this function:

void klee_alias_function	(	const char *	fn_name,
		const char *	new_fn_name
	)

void klee_assume

(

unsigned

condition

)

void klee_check_memory_access	(	const void *	address,
		unsigned	size
	)

unsigned klee_choose

(

unsigned

n

)

void klee_define_fixed_object	(	void *	addr,
		unsigned	nbytes
	)

unsigned klee_get_obj_size

(

void *

ptr

)

unsigned klee_get_value

(

unsigned

expr

)

int klee_int

(

const char *

name

)

klee_int - Construct an unconstrained symbolic integer.

• name - An optional name, used for identifying the object in messages, output files, etc.

unsigned klee_is_symbolic

(

unsigned

n

)

void klee_make_symbolic	(	void *	addr,
		unsigned	nbytes,
		const char *	name
	)

klee_make_symbolic - Make the contents of the object pointer to by

• addr symbolic.

• addr - The start of the object.
• nbytes - The number of bytes to make symbolic; currently this *must* be the entire contents of the object.
• name - An optional name, used for identifying the object in messages, output files, etc.

void klee_mark_global

(

void *

object

)

void klee_prefer_cex	(	void *	object,
		unsigned	condition
	)

void klee_print_expr	(	const char *	msg,
			...
	)

int klee_range	(	int	begin,
		int	end,
		const char *	name
	)

klee_range - Construct a symbolic value in the signed interval [begin,end).

• name - An optional name, used for identifying the object in messages, output files, etc.

void klee_set_forking

(

unsigned

enable

)

void klee_warning

(

const char *

message

)

Referenced by externalsAndGlobalsCheck(), KleeHandler::openOutputFile(), and KleeHandler::processTestCase().

Here is the caller graph for this function:

void klee_warning_once

(

const char *

message

)

Referenced by externalsAndGlobalsCheck().

Here is the caller graph for this function:

---

Variable Documentation

int line

Definition at line 65 of file klee.h.

Referenced by buildInstructionToLineMap(), main(), and readArgumentsFromFile().

int const char* message

Definition at line 65 of file klee.h.

int const char const char* suffix

Definition at line 65 of file klee.h.