diff options
9 files changed, 9 insertions, 9 deletions
diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_assume.c b/test/Replay/libkleeruntest/replay_invalid_klee_assume.c index 12ac006e..10da5615 100644 --- a/test/Replay/libkleeruntest/replay_invalid_klee_assume.c +++ b/test/Replay/libkleeruntest/replay_invalid_klee_assume.c @@ -6,7 +6,7 @@ // Now try to replay with libkleeRuntest but build the binary to use a different // value for the `klee_assume()` call. -// RUN: %cc -DASSUME_VALUE=32 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc -DASSUME_VALUE=32 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // Check that the default is to exit with an error // RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_choose.c b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c index 62f514bf..62cdcec3 100644 --- a/test/Replay/libkleeruntest/replay_invalid_klee_choose.c +++ b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c @@ -6,7 +6,7 @@ // Now try to replay with libkleeRuntest but build the binary to use a different // bound for `klee_choose()`. -// RUN: %cc -DBOUND_VALUE=2 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc -DBOUND_VALUE=2 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // Check that the default is to exit with an error // RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_range.c b/test/Replay/libkleeruntest/replay_invalid_klee_range.c index c7d62027..6542199e 100644 --- a/test/Replay/libkleeruntest/replay_invalid_klee_range.c +++ b/test/Replay/libkleeruntest/replay_invalid_klee_range.c @@ -6,7 +6,7 @@ // Now try to replay with libkleeRuntest but build the binary to use a different // bound for `klee_range()`. -// RUN: %cc -DBOUND_VALUE=2 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc -DBOUND_VALUE=2 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // Check that the default is to exit with an error // RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s diff --git a/test/Replay/libkleeruntest/replay_invalid_num_objects.c b/test/Replay/libkleeruntest/replay_invalid_num_objects.c index 43bc4867..39b389df 100644 --- a/test/Replay/libkleeruntest/replay_invalid_num_objects.c +++ b/test/Replay/libkleeruntest/replay_invalid_num_objects.c @@ -6,7 +6,7 @@ // Now try to replay with libkleeRuntest but build the binary so it // makes two calls to klee_make_symbolic. -// RUN: %cc -DEXTRA_MAKE_SYMBOLIC %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc -DEXTRA_MAKE_SYMBOLIC %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // Check that the default is to exit with an error // RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s diff --git a/test/Replay/libkleeruntest/replay_invalid_object_names.c b/test/Replay/libkleeruntest/replay_invalid_object_names.c index 9c75bebc..0285024c 100644 --- a/test/Replay/libkleeruntest/replay_invalid_object_names.c +++ b/test/Replay/libkleeruntest/replay_invalid_object_names.c @@ -5,7 +5,7 @@ // Now try to replay with libkleeRuntest but build the binary to use a different // object name -// RUN: %cc -DOBJ_NAME=wrong_name -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc -DOBJ_NAME=wrong_name -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // Check that the default is to exit with an error // RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s diff --git a/test/Replay/libkleeruntest/replay_invalid_object_size.c b/test/Replay/libkleeruntest/replay_invalid_object_size.c index a1513ef9..504a3bd0 100644 --- a/test/Replay/libkleeruntest/replay_invalid_object_size.c +++ b/test/Replay/libkleeruntest/replay_invalid_object_size.c @@ -6,7 +6,7 @@ // Now try to replay with libkleeRuntest but build the binary to use a different // size for variable `x`. -// RUN: %cc -DINT_TYPE=uint32_t -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc -DINT_TYPE=uint32_t -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // Check that the default is to exit with an error // RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s diff --git a/test/Replay/libkleeruntest/replay_posix_runtime.c b/test/Replay/libkleeruntest/replay_posix_runtime.c index 70d8a1d9..ac56179b 100644 --- a/test/Replay/libkleeruntest/replay_posix_runtime.c +++ b/test/Replay/libkleeruntest/replay_posix_runtime.c @@ -7,7 +7,7 @@ // RUN: test -f %t.klee-out/test000002.ktest // Now try to replay with libkleeRuntest -// RUN: %cc %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // RUN: %ktest-tool %t.klee-out/test000001.ktest | FileCheck -check-prefix=CHECKMODEL %s // RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner | FileCheck -check-prefix=TESTONE %s // RUN: env KTEST_FILE=%t.klee-out/test000002.ktest %t_runner | FileCheck -check-prefix=TESTTWO %s diff --git a/test/Replay/libkleeruntest/replay_simple.c b/test/Replay/libkleeruntest/replay_simple.c index cb9dfb85..77e2f5d2 100644 --- a/test/Replay/libkleeruntest/replay_simple.c +++ b/test/Replay/libkleeruntest/replay_simple.c @@ -5,7 +5,7 @@ // RUN: test -f %t.klee-out/test000002.ktest // Now try to replay with libkleeRuntest -// RUN: %cc %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner | FileCheck -check-prefix=TESTONE %s // RUN: env KTEST_FILE=%t.klee-out/test000002.ktest %t_runner | FileCheck -check-prefix=TESTTWO %s diff --git a/test/Replay/libkleeruntest/replay_two_objects.c b/test/Replay/libkleeruntest/replay_two_objects.c index f5be657c..779e1b65 100644 --- a/test/Replay/libkleeruntest/replay_two_objects.c +++ b/test/Replay/libkleeruntest/replay_two_objects.c @@ -5,7 +5,7 @@ // RUN: test ! -f %t.klee-out/test000002.ktest // Now try to replay with libkleeRuntest -// RUN: %cc -DPRINT_VALUES %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %cc -DPRINT_VALUES %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner | FileCheck -check-prefix=TESTONE %s #include "klee/klee.h" |