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 --- runtime/Intrinsic/klee_int.c | 2 +- runtime/Intrinsic/klee_make_symbolic.c | 14 -------------- runtime/Intrinsic/klee_range.c | 5 +++-- runtime/POSIX/fd_init.c | 16 ++++++++-------- runtime/POSIX/klee_init_env.c | 2 +- runtime/POSIX/misc.c | 2 +- runtime/Runtest/intrinsics.c | 12 ++++-------- runtime/klee-libc/klee-choose.c | 2 +- 8 files changed, 19 insertions(+), 36 deletions(-) delete mode 100644 runtime/Intrinsic/klee_make_symbolic.c (limited to 'runtime') diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c index 88ec5026..56f0f9dc 100644 --- a/runtime/Intrinsic/klee_int.c +++ b/runtime/Intrinsic/klee_int.c @@ -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; } diff --git a/runtime/Intrinsic/klee_make_symbolic.c b/runtime/Intrinsic/klee_make_symbolic.c deleted file mode 100644 index b9dec2a7..00000000 --- a/runtime/Intrinsic/klee_make_symbolic.c +++ /dev/null @@ -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 - -void klee_make_symbolic(void *addr, unsigned nbytes) { - klee_make_symbolic_name(addr, nbytes, "unnamed"); -} diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c index 59d1a05e..5da6a7a5 100644 --- a/runtime/Intrinsic/klee_range.c +++ b/runtime/Intrinsic/klee_range.c @@ -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) { diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index 61e49893..d976b0b4 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -56,9 +56,9 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, 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 void __create_new_dfile(exe_disk_file_t *dfile, unsigned size, 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 @@ void klee_init_fds(unsigned n_files, unsigned file_length, __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 */ diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index 83e9fde6..f5609973 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -62,7 +62,7 @@ static char *__get_sym_str(int numChars, char *name) { 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= n) fprintf(stderr, "ERROR: max = %d, got = %d\n", n, x); assert(x < n); @@ -136,9 +132,9 @@ unsigned klee_get_value(unsigned x) { 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=end) { fprintf(stderr, "KLEE: ERROR: invalid klee_range(%u,%u,%s) value, got: %u\n", diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c index 106b4f89..347933df 100644 --- a/runtime/klee-libc/klee-choose.c +++ b/runtime/klee-libc/klee-choose.c @@ -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) -- cgit 1.4.1