diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-08-13 22:11:27 +0100 |
|---|---|---|
| committer | MartinNowack <martin.nowack@gmail.com> | 2019-08-14 16:26:48 +0100 |
| commit | 0012e87b747dc9a46cec4ed5708e72afc1eb8d3c (patch) | |
| tree | 4814023a765f2a7440f7ad15d5221f136912bd55 | |
| parent | e3d84e2888b51f271f53c2b368f76f958b6ff1dc (diff) | |
| download | klee-0012e87b747dc9a46cec4ed5708e72afc1eb8d3c.tar.gz | |
Rewrote the checks in GenRandomBout.c to remove dependency on bash and use FileCheck instead (FreeBSD tests on Travis CI fail otherwise)
| -rw-r--r-- | test/Replay/klee-replay/GenRandomBout.c | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/test/Replay/klee-replay/GenRandomBout.c b/test/Replay/klee-replay/GenRandomBout.c index 0620e778..9f609a40 100644 --- a/test/Replay/klee-replay/GenRandomBout.c +++ b/test/Replay/klee-replay/GenRandomBout.c @@ -4,14 +4,24 @@ // RUN: %cc %s -O0 -o %t // RUN: %klee-replay %t %t.bout 2> %t.out // RUN: FileCheck --input-file=%t.out %s +// CHECK: KLEE-REPLAY: NOTE: EXIT STATUS: NORMAL // // -- Option error handling tests -// RUN: bash -c '%gen-random-bout || :' 2>&1 | grep "Usage" -// RUN: bash -c '%gen-random-bout 0 --unexpected-option || :' 2>&1 | grep "Unexpected" -// RUN: bash -c '%gen-random-bout 100 --sym-args 5 3 || :' 2>&1 | grep "ran out of" -// RUN: bash -c '%gen-random-bout 100 --sym-args 5 3 10 || :' 2>&1 | grep "should be no more" - -// CHECK: KLEE-REPLAY: NOTE: EXIT STATUS: NORMAL +// RUN: not %gen-random-bout 2> %t1 +// RUN: FileCheck -check-prefix=CHECK-USAGE -input-file=%t1 %s +// CHECK-USAGE: Usage +// +// RUN: not %gen-random-bout 0 --unexpected-option 2> %t2 +// RUN: FileCheck -check-prefix=CHECK-UNEXPECTED -input-file=%t2 %s +// CHECK-UNEXPECTED: Unexpected +// +// RUN: not %gen-random-bout 100 --sym-args 5 3 2> %t3 +// RUN: FileCheck -check-prefix=CHECK-RANOUT -input-file=%t3 %s +// CHECK-RANOUT: ran out of +// +// RUN: not %gen-random-bout 100 --sym-args 5 3 10 2> %t4 +// RUN: FileCheck -check-prefix=CHECK-NOMORE -input-file=%t4 %s +// CHECK-NOMORE: should be no more #include <sys/types.h> #include <sys/stat.h> |