From ea6e216751979131b269ed31873edbe7e8b752a3 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Fri, 22 May 2009 16:27:06 +0000 Subject: Add "name" argument to klee_make_symbolic, and kill off klee_make_symbolic_name. - For compatibility we still accept 2 argument form of klee_make_symbolic, but this will go away eventually. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72265 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/klee.h | 46 ++++++++++++++++++++++++++++++---------------- 1 file changed, 30 insertions(+), 16 deletions(-) (limited to 'include') diff --git a/include/klee/klee.h b/include/klee/klee.h index 698a61c4..3d2d1782 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -21,31 +21,45 @@ extern "C" { calls. */ void klee_define_fixed_object(void *addr, unsigned nbytes); - /* make the contents of the object pointed to by addr symbolic. addr - * should always be the start of the object and nbytes must be its - * entire size. name is an optional name (can be the empty string) - */ - void klee_make_symbolic_name(void *addr, unsigned nbytes, - const char *name); - - void klee_make_symbolic(void *addr, unsigned nbytes); - - /* Return symbolic value in the (signed) interval [begin,end) */ + /// klee_make_symbolic - Make the contents of the object pointer to by \arg + /// addr symbolic. + /// + /// \arg addr - The start of the object. + /// \arg nbytes - The number of bytes to make symbolic; currently this *must* + /// be the entire contents of the object. + /// \arg name - An optional name, used for identifying the object in messages, + /// output files, etc. + void klee_make_symbolic(void *addr, unsigned nbytes, const char *name); + + /// klee_range - Construct a symbolic value in the signed interval + /// [begin,end). + /// + /// \arg name - An optional name, used for identifying the object in messages, + /// output files, etc. int klee_range(int begin, int end, const char *name); - /* Return a symbolic integer */ + /// klee_int - Construct an unconstrained symbolic integer. + /// + /// \arg name - An optional name, used for identifying the object in messages, + /// output files, etc. int klee_int(const char *name); - void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment); - - /* terminate the state without generating a test file */ + /// klee_silent_exit - Terminate the current KLEE process without generating a + /// test file. __attribute__((noreturn)) void klee_silent_exit(int status); - + + /// klee_abort - Abort the current KLEE process. __attribute__((noreturn)) void klee_abort(void); - /** Report an error and terminate the state. */ + /// klee_report_error - Report a user defined error and terminate the current + /// KLEE process. + /// + /// \arg file - The filename to report in the error message. + /// \arg line - The line number to report in the error message. + /// \arg message - A string to include in the error message. + /// \arg suffix - The suffix to use for error files. __attribute__((noreturn)) void klee_report_error(const char *file, int line, -- cgit 1.4.1