#include "stdint.h"
#include "stddef.h"

Include dependency graph for klee.h:

This graph shows which files directly or indirectly include this file:

Macros
#define	klee_assert(expr)

#define	KLEE_GET_VALUE_PROTO(suffix, type) type klee_get_value##suffix(type expr)

Functions
void	klee_define_fixed_object (void *addr, size_t nbytes)

void	klee_make_symbolic (void addr, size_t nbytes, const char name)

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

int	klee_int (const char *name)

	__attribute__ ((noreturn)) void klee_silent_exit(int status)

size_t	klee_get_obj_size (void *ptr)

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

uintptr_t	klee_choose (uintptr_t n)

unsigned	klee_is_symbolic (uintptr_t n)

unsigned	klee_is_replay (void)

void	klee_assume (uintptr_t condition)

void	klee_warning (const char *message)

void	klee_warning_once (const char *message)

void	klee_prefer_cex (void *object, uintptr_t condition)

void	klee_posix_prefer_cex (void *object, uintptr_t condition)

void	klee_mark_global (void *object)

	KLEE_GET_VALUE_PROTO (f, float)

	KLEE_GET_VALUE_PROTO (d, double)

	KLEE_GET_VALUE_PROTO (l, long)

	KLEE_GET_VALUE_PROTO (ll, long long)

	KLEE_GET_VALUE_PROTO (_i32, int32_t)

	KLEE_GET_VALUE_PROTO (_i64, int64_t)

void	klee_check_memory_access (const void *address, size_t size)

void	klee_set_forking (unsigned enable)

void	klee_stack_trace (void)

void	klee_print_range (const char *name, int arg)

void	klee_open_merge (void)

void	klee_close_merge (void)

int	klee_get_errno (void)

Variables
int	line

int const char *	message

int const char const char *	suffix

Macro Definition Documentation

◆ klee_assert

#define klee_assert ( expr )

Value:

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

Definition at line 93 of file klee.h.

◆ KLEE_GET_VALUE_PROTO

#define KLEE_GET_VALUE_PROTO	(	suffix,
		type
	)	type klee_get_value##suffix(type expr)

Definition at line 124 of file klee.h.

Function Documentation

◆ attribute()

__attribute__ ( (noreturn) )

◆ klee_assume()

void klee_assume ( uintptr_t condition )

Definition at line 440 of file klee-replay.c.

◆ klee_check_memory_access()

void klee_check_memory_access	(	const void *	address,
		size_t	size
	)

◆ klee_choose()

uintptr_t klee_choose ( uintptr_t n )

◆ klee_close_merge()

void klee_close_merge ( void )

◆ klee_define_fixed_object()

void klee_define_fixed_object	(	void *	addr,
		size_t	nbytes
	)

◆ klee_get_errno()

int klee_get_errno ( void )

Definition at line 428 of file klee-replay.c.

◆ klee_get_obj_size()

size_t klee_get_obj_size ( void * ptr )

◆ KLEE_GET_VALUE_PROTO() [1/6]

KLEE_GET_VALUE_PROTO	(	_i32	,
		int32_t
	)

◆ KLEE_GET_VALUE_PROTO() [2/6]

KLEE_GET_VALUE_PROTO	(	_i64	,
		int64_t
	)

◆ KLEE_GET_VALUE_PROTO() [3/6]

KLEE_GET_VALUE_PROTO	(	d	,
		double
	)

◆ KLEE_GET_VALUE_PROTO() [4/6]

KLEE_GET_VALUE_PROTO	(	f	,
		float
	)

◆ KLEE_GET_VALUE_PROTO() [5/6]

KLEE_GET_VALUE_PROTO	(	l	,
		long
	)

◆ KLEE_GET_VALUE_PROTO() [6/6]

KLEE_GET_VALUE_PROTO	(	ll	,
		long long
	)

◆ klee_int()

int klee_int ( const char * name )

◆ klee_is_replay()

unsigned klee_is_replay ( void )

◆ klee_is_symbolic()

unsigned klee_is_symbolic ( uintptr_t n )

Definition at line 447 of file klee-replay.c.

◆ klee_make_symbolic()

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

Definition at line 459 of file klee-replay.c.

References __emit_error(), KTestObject::bytes, input, KTestObject::name, KTestObject::numBytes, KTest::numObjects, obj_index, and KTest::objects.

Referenced by klee_range().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ klee_mark_global()

void klee_mark_global ( void * object )

Definition at line 517 of file klee-replay.c.

◆ klee_open_merge()

void klee_open_merge ( void )

◆ klee_posix_prefer_cex()

void klee_posix_prefer_cex	(	void *	object,
		uintptr_t	condition
	)

Definition at line 455 of file klee-replay.c.

◆ klee_prefer_cex()

void klee_prefer_cex	(	void *	object,
		uintptr_t	condition
	)

Definition at line 451 of file klee-replay.c.

◆ klee_print_expr()

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

◆ klee_print_range()

void klee_print_range	(	const char *	name,
		int	arg
	)

◆ klee_range()

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

Definition at line 489 of file klee-replay.c.

References klee_make_symbolic().

Here is the call graph for this function:

◆ klee_set_forking()

void klee_set_forking ( unsigned enable )

◆ klee_stack_trace()

void klee_stack_trace ( void )

◆ klee_warning()

void klee_warning ( const char * message )

◆ klee_warning_once()

void klee_warning_once ( const char * message )

Variable Documentation

◆ line

int line

Definition at line 74 of file klee.h.

Referenced by buildInstructionToLineMap(), DebugInfoExtractor::getInstructionInfo(), main(), and KleeHandler::processTestCase().

◆ message

int const char* message

Definition at line 75 of file klee.h.

Referenced by klee_report_error(), klee::ExprPPrinter::printOne(), klee::Executor::terminateStateEarly(), klee::Executor::terminateStateOnError(), klee::Executor::terminateStateOnExecError(), klee::Executor::terminateStateOnSolverError(), and klee::Executor::terminateStateOnUserError().

◆ suffix

int const char const char* suffix

Definition at line 76 of file klee.h.

Referenced by KleeHandler::getTestFilename(), KleeHandler::openTestFile(), and klee::Executor::terminateStateOnError().

Macros

Functions

Variables