diff options
author | Frank Busse <bb0xfb@gmail.com> | 2019-07-31 14:37:37 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-08-01 16:53:44 +0100 |
commit | 04f5031ce572fa7488c9d97155207a3f5832e212 (patch) | |
tree | 59513df3660a22c380f0e68fd132ba2cda069efc /test/Runtime/POSIX/GenBout.c | |
parent | a243341556a81122bf45cc086a6a94b8b0d69bea (diff) | |
download | klee-04f5031ce572fa7488c9d97155207a3f5832e212.tar.gz |
tests: fix Gen(Random)Bout.c: cd - command not found
Diffstat (limited to 'test/Runtime/POSIX/GenBout.c')
-rw-r--r-- | test/Runtime/POSIX/GenBout.c | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/test/Runtime/POSIX/GenBout.c b/test/Runtime/POSIX/GenBout.c index 1aac748c..ab09f39b 100644 --- a/test/Runtime/POSIX/GenBout.c +++ b/test/Runtime/POSIX/GenBout.c @@ -1,12 +1,16 @@ // -- Core testing commands // RUN: rm -rf %t.out -// RUN: mkdir -p %t.out && cd %t.out -// RUN: echo -n aaaa > %t.aaaa.txt -// RUN: echo -n bbbb > %t.bbbb.txt -// RUN: echo -n cccc > %t.cccc.txt -// RUN: %gen-bout -o -p -q file1 --sym-stdin %t.aaaa.txt --sym-file %t.bbbb.txt --sym-stdout %t.cccc.txt +// RUN: rm -f %t.bout +// RUN: mkdir -p %t.out +// RUN: echo -n aaaa > %t.out/aaaa.txt +// RUN: echo -n bbbb > %t.out/bbbb.txt +// RUN: echo -n cccc > %t.out/cccc.txt +// RUN: %gen-bout -o -p -q file1 --bout-file %t.bout --sym-stdin %t.out/aaaa.txt --sym-file %t.out/bbbb.txt --sym-stdout %t.out/cccc.txt // RUN: %cc %s -O0 -o %t -// RUN: %klee-replay %t file.bout 2>&1 | grep "klee-replay: EXIT STATUS: NORMAL" +// RUN: %klee-replay %t %t.bout 2> %t.out/out.txt +// RUN: FileCheck --input-file=%t.out/out.txt %s + +// CHECK: klee-replay: EXIT STATUS: NORMAL #include <sys/types.h> #include <sys/stat.h> @@ -41,8 +45,6 @@ int check_file(const char *file_name, const int file_size) { } int main(int argc, char **argv) { - int i = 0; - if (argc != 5) return 1; |