klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee.h File Reference
#include "stdint.h"
#include "stddef.h"
Include dependency graph for klee.h:

Go to the source code of 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_abort(void)
 klee_abort - Abort the current KLEE process. More...
 
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)
 
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_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_alias_function (const char *fn_name, const char *new_fn_name)
 
void klee_stack_trace (void)
 

Variables

int line
 
int const char * message
 
int const char const char * suffix
 

Macro Definition Documentation

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

Definition at line 87 of file klee.h.

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

Definition at line 111 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.
void klee_alias_function ( const char *  fn_name,
const char *  new_fn_name 
)
void klee_assume ( uintptr_t  condition)

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

void klee_check_memory_access ( const void *  address,
size_t  size 
)
uintptr_t klee_choose ( uintptr_t  n)
void klee_define_fixed_object ( void *  addr,
size_t  nbytes 
)
size_t klee_get_obj_size ( void *  ptr)
KLEE_GET_VALUE_PROTO ( ,
float   
)
KLEE_GET_VALUE_PROTO ( ,
double   
)
KLEE_GET_VALUE_PROTO ( ,
long   
)
KLEE_GET_VALUE_PROTO ( ll  ,
long  long 
)
KLEE_GET_VALUE_PROTO ( _i32  ,
int32_t   
)
KLEE_GET_VALUE_PROTO ( _i64  ,
int64_t   
)
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 ( uintptr_t  n)

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

void klee_make_symbolic ( void *  addr,
size_t  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.

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

References __emit_error(), KTestObject::bytes, 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:

void klee_mark_global ( void *  object)

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

void klee_prefer_cex ( void *  object,
uintptr_t  condition 
)

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

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.

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

References klee_make_symbolic().

Here is the call graph for this function:

void klee_set_forking ( unsigned  enable)
void klee_stack_trace ( void  )
void klee_warning ( const char *  message)
void klee_warning_once ( const char *  message)

Variable Documentation

int line
int const char* message

Definition at line 68 of file klee.h.

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

int const char const char* suffix

Definition at line 68 of file klee.h.

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