[llvm-commits] [klee] r72265 - in /klee/trunk: examples/regexp/ examples/sort/ include/klee/ lib/Core/ runtime/Intrinsic/ runtime/POSIX/ runtime/Runtest/ runtime/klee-libc/ test/ test/Coverage/ test/Feature/ test/regression/ tools/klee/ www/code-examples/
Daniel Dunbar
daniel at zuster.org
Fri May 22 09:27:08 PDT 2009
Author: ddunbar
Date: Fri May 22 11:27:06 2009
New Revision: 72265
URL: http://llvm.org/viewvc/llvm-project?rev=72265&view=rev
Log:
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.
Removed:
klee/trunk/runtime/Intrinsic/klee_make_symbolic.c
Modified:
klee/trunk/examples/regexp/Regexp.c
klee/trunk/examples/sort/sort.c
klee/trunk/include/klee/klee.h
klee/trunk/lib/Core/SpecialFunctionHandler.cpp
klee/trunk/runtime/Intrinsic/klee_int.c
klee/trunk/runtime/Intrinsic/klee_range.c
klee/trunk/runtime/POSIX/fd_init.c
klee/trunk/runtime/POSIX/klee_init_env.c
klee/trunk/runtime/POSIX/misc.c
klee/trunk/runtime/Runtest/intrinsics.c
klee/trunk/runtime/klee-libc/klee-choose.c
klee/trunk/test/Coverage/ReplayOutDir.c
klee/trunk/test/Feature/AliasFunction.c
klee/trunk/test/Feature/AliasFunctionExit.c
klee/trunk/test/Feature/MakeSymbolicName.c
klee/trunk/test/Feature/NamedSeedMatching.c
klee/trunk/test/Feature/const_array_opt1.c
klee/trunk/test/Makefile
klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
klee/trunk/test/regression/2008-04-10-bad-alloca-free.c
klee/trunk/tools/klee/main.cpp
klee/trunk/www/code-examples/demo.c
Modified: klee/trunk/examples/regexp/Regexp.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/examples/regexp/Regexp.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/examples/regexp/Regexp.c (original)
+++ klee/trunk/examples/regexp/Regexp.c Fri May 22 11:27:06 2009
@@ -53,7 +53,7 @@
char re[SIZE];
// Make the input symbolic.
- klee_make_symbolic_name(re, sizeof re, "re");
+ klee_make_symbolic(re, sizeof re, "re");
// Try to match against a constant string "hello".
match(re, "hello");
Modified: klee/trunk/examples/sort/sort.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/examples/sort/sort.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/examples/sort/sort.c (original)
+++ klee/trunk/examples/sort/sort.c Fri May 22 11:27:06 2009
@@ -71,7 +71,7 @@
int main() {
int input[4] = { 4, 3, 2, 1};
- klee_make_symbolic(&input, sizeof(input));
+ klee_make_symbolic(&input, sizeof(input), "input");
test(input, 4);
return 0;
Modified: klee/trunk/include/klee/klee.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/klee.h?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/include/klee/klee.h (original)
+++ klee/trunk/include/klee/klee.h Fri May 22 11:27:06 2009
@@ -21,31 +21,45 @@
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,
Modified: klee/trunk/lib/Core/SpecialFunctionHandler.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/SpecialFunctionHandler.cpp?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/lib/Core/SpecialFunctionHandler.cpp (original)
+++ klee/trunk/lib/Core/SpecialFunctionHandler.cpp Fri May 22 11:27:06 2009
@@ -72,7 +72,7 @@
add("klee_get_obj_size", handleGetObjSize, true),
add("klee_get_errno", handleGetErrno, true),
add("klee_is_symbolic", handleIsSymbolic, true),
- add("klee_make_symbolic_name", handleMakeSymbolic, false),
+ add("klee_make_symbolic", handleMakeSymbolic, false),
add("klee_mark_global", handleMarkGlobal, false),
add("klee_malloc_n", handleMallocN, true),
add("klee_merge", handleMerge, false),
@@ -670,8 +670,18 @@
void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
KInstruction *target,
std::vector<ref<Expr> > &arguments) {
- assert(arguments.size()==3 &&
- "invalid number of arguments to klee_make_symbolic[_name]");
+ std::string name;
+
+ // FIXME: For backwards compatibility, we should eventually enforce the
+ // correct arguments.
+ if (arguments.size() == 2) {
+ name = "unnamed";
+ } else {
+ // FIXME: Should be a user.err, not an assert.
+ assert(arguments.size()==3 &&
+ "invalid number of arguments to klee_make_symbolic");
+ name = readStringAtAddress(state, arguments[2]);
+ }
Executor::ExactResolutionList rl;
executor.resolveExact(state, arguments[0], rl, "make_symbolic");
@@ -679,7 +689,6 @@
for (Executor::ExactResolutionList::iterator it = rl.begin(),
ie = rl.end(); it != ie; ++it) {
MemoryObject *mo = (MemoryObject*) it->first.first;
- std::string name = readStringAtAddress(state, arguments[2]);
mo->setName(name);
const ObjectState *old = it->first.second;
Modified: klee/trunk/runtime/Intrinsic/klee_int.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/Intrinsic/klee_int.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/runtime/Intrinsic/klee_int.c (original)
+++ klee/trunk/runtime/Intrinsic/klee_int.c Fri May 22 11:27:06 2009
@@ -12,6 +12,6 @@
int klee_int(const char *name) {
int x;
- klee_make_symbolic_name(&x, sizeof x, name);
+ klee_make_symbolic(&x, sizeof x, name);
return x;
}
Removed: klee/trunk/runtime/Intrinsic/klee_make_symbolic.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/Intrinsic/klee_make_symbolic.c?rev=72264&view=auto
==============================================================================
--- klee/trunk/runtime/Intrinsic/klee_make_symbolic.c (original)
+++ klee/trunk/runtime/Intrinsic/klee_make_symbolic.c (removed)
@@ -1,14 +0,0 @@
-//===-- klee_make_symbolic.c ----------------------------------------------===//
-//
-// The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include <klee/klee.h>
-
-void klee_make_symbolic(void *addr, unsigned nbytes) {
- klee_make_symbolic_name(addr, nbytes, "unnamed");
-}
Modified: klee/trunk/runtime/Intrinsic/klee_range.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/Intrinsic/klee_range.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/runtime/Intrinsic/klee_range.c (original)
+++ klee/trunk/runtime/Intrinsic/klee_range.c Fri May 22 11:27:06 2009
@@ -13,12 +13,13 @@
int klee_range(int start, int end, const char* name) {
int x;
- assert(start < end);
+ if (start >= end)
+ klee_report_error(__FILE__, __LINE__, "invalid range", "user");
if (start+1==end) {
return start;
} else {
- klee_make_symbolic_name(&x, sizeof x, name);
+ klee_make_symbolic(&x, sizeof x, name);
/* Make nicer constraint when simple... */
if (start==0) {
Modified: klee/trunk/runtime/POSIX/fd_init.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/POSIX/fd_init.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/runtime/POSIX/fd_init.c (original)
+++ klee/trunk/runtime/POSIX/fd_init.c Fri May 22 11:27:06 2009
@@ -56,9 +56,9 @@
dfile->size = size;
dfile->contents = malloc(dfile->size);
- klee_make_symbolic_name(dfile->contents, dfile->size, name);
+ klee_make_symbolic(dfile->contents, dfile->size, name);
- klee_make_symbolic_name(s, sizeof(*s), sname);
+ klee_make_symbolic(s, sizeof(*s), sname);
/* For broken tests */
if (!klee_is_symbolic(s->st_ino) &&
@@ -96,7 +96,7 @@
static unsigned __sym_uint32(const char *name) {
unsigned x;
- klee_make_symbolic_name(&x, sizeof x, name);
+ klee_make_symbolic(&x, sizeof x, name);
return x;
}
@@ -139,11 +139,11 @@
__exe_fs.ftruncate_fail = malloc(sizeof(*__exe_fs.ftruncate_fail));
__exe_fs.getcwd_fail = malloc(sizeof(*__exe_fs.getcwd_fail));
- klee_make_symbolic_name(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
- klee_make_symbolic_name(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
- klee_make_symbolic_name(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
- klee_make_symbolic_name(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
- klee_make_symbolic_name(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
+ klee_make_symbolic(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
+ klee_make_symbolic(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
+ klee_make_symbolic(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
+ klee_make_symbolic(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
+ klee_make_symbolic(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
}
/* setting symbolic stdout */
Modified: klee/trunk/runtime/POSIX/klee_init_env.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/POSIX/klee_init_env.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/runtime/POSIX/klee_init_env.c (original)
+++ klee/trunk/runtime/POSIX/klee_init_env.c Fri May 22 11:27:06 2009
@@ -62,7 +62,7 @@
int i;
char *s = malloc(numChars+1);
klee_mark_global(s);
- klee_make_symbolic_name(s, numChars+1, name);
+ klee_make_symbolic(s, numChars+1, name);
for (i=0; i<numChars; i++)
klee_prefer_cex(s, __isprint(s[i]));
Modified: klee/trunk/runtime/POSIX/misc.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/POSIX/misc.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/runtime/POSIX/misc.c (original)
+++ klee/trunk/runtime/POSIX/misc.c Fri May 22 11:27:06 2009
@@ -69,7 +69,7 @@
if (__klee_sym_env_count < __klee_sym_env_nvars) {
if (klee_range(0, 2, name)) {
char *s = malloc(__klee_sym_env_var_size+1);
- klee_make_symbolic(s, __klee_sym_env_var_size+1);
+ klee_make_symbolic(s, __klee_sym_env_var_size+1. "env");
s[__klee_sym_env_var_size] = '\0';
memcpy(__klee_sym_env[__klee_sym_env_count].name, name, len+1);
Modified: klee/trunk/runtime/Runtest/intrinsics.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/Runtest/intrinsics.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/runtime/Runtest/intrinsics.c (original)
+++ klee/trunk/runtime/Runtest/intrinsics.c Fri May 22 11:27:06 2009
@@ -31,7 +31,7 @@
return x & 0xFF;
}
-void klee_make_symbolic_name(void *array, unsigned nbytes, const char *name) {
+void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
static int rand_init = -1;
if (rand_init == -1) {
@@ -94,10 +94,6 @@
}
}
-void klee_make_symbolic(void *array, unsigned nbytes) {
- klee_make_symbolic_name(array, nbytes, "unnamed");
-}
-
void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment) {
#if 1
return mmap((void*) 0x90000000, nelems*size, PROT_READ|PROT_WRITE,
@@ -119,7 +115,7 @@
unsigned klee_choose(unsigned n) {
unsigned x;
- klee_make_symbolic(&x, sizeof x);
+ klee_make_symbolic(&x, sizeof x, "klee_choose");
if(x >= n)
fprintf(stderr, "ERROR: max = %d, got = %d\n", n, x);
assert(x < n);
@@ -136,9 +132,9 @@
return x;
}
-int klee_range_name(int begin, int end, const char* name) {
+int klee_range(int begin, int end, const char* name) {
int x;
- klee_make_symbolic_name(&x, sizeof x, name);
+ klee_make_symbolic(&x, sizeof x, name);
if (x<begin || x>=end) {
fprintf(stderr,
"KLEE: ERROR: invalid klee_range(%u,%u,%s) value, got: %u\n",
Modified: klee/trunk/runtime/klee-libc/klee-choose.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/klee-libc/klee-choose.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/runtime/klee-libc/klee-choose.c (original)
+++ klee/trunk/runtime/klee-libc/klee-choose.c Fri May 22 11:27:06 2009
@@ -11,7 +11,7 @@
unsigned klee_choose(unsigned n) {
unsigned x;
- klee_make_symbolic(&x, sizeof x);
+ klee_make_symbolic(&x, sizeof x, "klee_choose");
// NB: this will *not* work if they don't compare to n values.
if(x >= n)
Modified: klee/trunk/test/Coverage/ReplayOutDir.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Coverage/ReplayOutDir.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/Coverage/ReplayOutDir.c (original)
+++ klee/trunk/test/Coverage/ReplayOutDir.c Fri May 22 11:27:06 2009
@@ -5,7 +5,7 @@
int main() {
int i;
- klee_make_symbolic(&i, sizeof i);
+ klee_make_symbolic(&i, sizeof i, "i");
klee_print_range("i", i);
return 0;
}
Modified: klee/trunk/test/Feature/AliasFunction.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/AliasFunction.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/Feature/AliasFunction.c (original)
+++ klee/trunk/test/Feature/AliasFunction.c Fri May 22 11:27:06 2009
@@ -11,7 +11,7 @@
int main() {
int x;
- klee_make_symbolic_name(&x, sizeof(x), "x");
+ klee_make_symbolic(&x, sizeof(x), "x");
// no aliases
foo();
Modified: klee/trunk/test/Feature/AliasFunctionExit.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/AliasFunctionExit.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/Feature/AliasFunctionExit.c (original)
+++ klee/trunk/test/Feature/AliasFunctionExit.c Fri May 22 11:27:06 2009
@@ -22,7 +22,7 @@
int main() {
int x;
- klee_make_symbolic_name(&x, sizeof(x), "x");
+ klee_make_symbolic(&x, sizeof(x), "x");
klee_alias_function("exit", "end");
start(x);
Modified: klee/trunk/test/Feature/MakeSymbolicName.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/MakeSymbolicName.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/Feature/MakeSymbolicName.c (original)
+++ klee/trunk/test/Feature/MakeSymbolicName.c Fri May 22 11:27:06 2009
@@ -7,7 +7,7 @@
int a[4] = {1, 2, 3, 4};
unsigned i;
- klee_make_symbolic_name(&i, sizeof(i), "index");
+ klee_make_symbolic(&i, sizeof(i), "index");
if (i > 3)
klee_silent_exit(0);
Modified: klee/trunk/test/Feature/NamedSeedMatching.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/NamedSeedMatching.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/Feature/NamedSeedMatching.c (original)
+++ klee/trunk/test/Feature/NamedSeedMatching.c Fri May 22 11:27:06 2009
@@ -16,20 +16,20 @@
int a, b, c, x;
if (argc==2 && strcmp(argv[1], "initial") == 0) {
- klee_make_symbolic_name(&a, sizeof a, "a");
- klee_make_symbolic_name(&b, sizeof b, "b");
- klee_make_symbolic_name(&c, sizeof c, "c");
- klee_make_symbolic_name(&x, sizeof x, "a");
+ klee_make_symbolic(&a, sizeof a, "a");
+ klee_make_symbolic(&b, sizeof b, "b");
+ klee_make_symbolic(&c, sizeof c, "c");
+ klee_make_symbolic(&x, sizeof x, "a");
klee_assume(a == 3);
klee_assume(b == 4);
klee_assume(c == 5);
klee_assume(x == 6);
} else {
- klee_make_symbolic_name(&a, sizeof a, "a");
- klee_make_symbolic_name(&c, sizeof c, "c");
- klee_make_symbolic_name(&b, sizeof b, "b");
- klee_make_symbolic_name(&x, sizeof x, "a");
+ klee_make_symbolic(&a, sizeof a, "a");
+ klee_make_symbolic(&c, sizeof c, "c");
+ klee_make_symbolic(&b, sizeof b, "b");
+ klee_make_symbolic(&x, sizeof x, "a");
}
if (a==3) printf("a==3\n");
Modified: klee/trunk/test/Feature/const_array_opt1.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/const_array_opt1.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/Feature/const_array_opt1.c (original)
+++ klee/trunk/test/Feature/const_array_opt1.c Fri May 22 11:27:06 2009
@@ -20,7 +20,7 @@
for (i=0; i<N; i++)
a[i] = i % 256;
- klee_make_symbolic_name(k, sizeof(k), "k");
+ klee_make_symbolic(k, sizeof(k), "k");
for (i=0; i<N_IDX; i++) {
if (k[i] >= N)
Modified: klee/trunk/test/Makefile
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Makefile?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/Makefile (original)
+++ klee/trunk/test/Makefile Fri May 22 11:27:06 2009
@@ -89,8 +89,8 @@
@echo 'set compile_c "$(CC) $(CPP.Flags) $(C.Flags) $(CompileCommonOpts) -c "' >>site.tmp
@echo 'set compile_cxx "$(CXX) $(CPP.Flags) $(CXX.Flags) $(CompileCommonOpts) - c"' >> site.tmp
@echo 'set link "$(CXX) $(CPP.Flags) $(CXX.Flags) $(CompileCommonOpts) $(LD.Flags)"' >>site.tmp
- @echo 'set llvmgcc "$(LLVMGCC)"' >> site.tmp
- @echo 'set llvmgxx "$(LLVMGCC)"' >> site.tmp
+ @echo 'set llvmgcc "$(LLVMGCC) -m32"' >> site.tmp
+ @echo 'set llvmgxx "$(LLVMGCC) -m32"' >> site.tmp
@echo 'set llvmgccmajvers "$(LLVMGCC_MAJVERS)"' >> site.tmp
@echo 'set shlibext "$(SHLIBEXT)"' >> site.tmp
@echo '## All variables above are generated by configure. Do Not Edit ## ' >>site.tmp
Modified: klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c (original)
+++ klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c Fri May 22 11:27:06 2009
@@ -5,13 +5,13 @@
int main() {
unsigned x, y[4];
- klee_make_symbolic(&x,sizeof x);
+ klee_make_symbolic(&x, sizeof x, "x");
if (x>=4) klee_silent_exit(0);
y[x] = 0;
if (x) { // force branch so y is copied
- klee_make_symbolic(&y, sizeof y);
+ klee_make_symbolic(&y, sizeof y, "y");
if (y[x]==0) klee_silent_exit(0);
return 0; // should be reachable
} else {
Modified: klee/trunk/test/regression/2008-04-10-bad-alloca-free.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/regression/2008-04-10-bad-alloca-free.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/test/regression/2008-04-10-bad-alloca-free.c (original)
+++ klee/trunk/test/regression/2008-04-10-bad-alloca-free.c Fri May 22 11:27:06 2009
@@ -2,7 +2,7 @@
// RUN: %klee --exit-on-error %t1.bc
void f(int *addr) {
- klee_make_symbolic_name(addr, sizeof *addr, "moo");
+ klee_make_symbolic(addr, sizeof *addr, "moo");
}
int main() {
Modified: klee/trunk/tools/klee/main.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/tools/klee/main.cpp?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/tools/klee/main.cpp (original)
+++ klee/trunk/tools/klee/main.cpp Fri May 22 11:27:06 2009
@@ -661,7 +661,7 @@
"klee_get_value",
"klee_get_obj_size",
"klee_is_symbolic",
- "klee_make_symbolic_name",
+ "klee_make_symbolic",
"klee_mark_global",
"klee_malloc_n",
"klee_merge",
Modified: klee/trunk/www/code-examples/demo.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/code-examples/demo.c?rev=72265&r1=72264&r2=72265&view=diff
==============================================================================
--- klee/trunk/www/code-examples/demo.c (original)
+++ klee/trunk/www/code-examples/demo.c Fri May 22 11:27:06 2009
@@ -6,6 +6,6 @@
int main() {
char c;
- klee_make_symbolic_name(&c, sizeof(c), "input");
+ klee_make_symbolic(&c, sizeof(c), "input");
return my_islower(c);
}
More information about the llvm-commits
mailing list