about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2019-07-31 14:37:23 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-08-01 16:53:44 +0100
commita243341556a81122bf45cc086a6a94b8b0d69bea (patch)
tree5be6c53843f42adc9d7f6a60df5032d3b1a404d6
parent7640a09981b6376da2ec75be7caf76661ef15f28 (diff)
downloadklee-a243341556a81122bf45cc086a6a94b8b0d69bea.tar.gz
gen(-random)-bout: add --bout-file flag
-rw-r--r--runtime/POSIX/klee_init_env.c2
-rw-r--r--tools/gen-bout/gen-bout.cpp42
-rw-r--r--tools/gen-random-bout/gen-random-bout.cpp13
3 files changed, 37 insertions, 20 deletions
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index b55a90a6..80d3a104 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -208,6 +208,8 @@ usage: (klee_init_env) [options] [program arguments]\n\
     } else if (__streq(argv[k], "--fd-fail") || __streq(argv[k], "-fd-fail")) {
       fd_fail = 1;
       k++;
+    } else if (__streq(argv[k], "--bout-file") || __streq(argv[k], "-bout-file")) {
+      k += 2;
     } else if (__streq(argv[k], "--max-fail") ||
                __streq(argv[k], "-max-fail")) {
       const char *msg = "--max-fail expects an integer argument <max-failures>";
diff --git a/tools/gen-bout/gen-bout.cpp b/tools/gen-bout/gen-bout.cpp
index d8754251..dfc02fda 100644
--- a/tools/gen-bout/gen-bout.cpp
+++ b/tools/gen-bout/gen-bout.cpp
@@ -49,22 +49,23 @@ static void push_range(KTest *b, const char *name, unsigned value) {
 
 void print_usage_and_exit(char *program_name) {
   fprintf(stderr,
-          "%s: Tool for generating ktest file with concrete input, "
-          "e.g., for using a concrete crashing input as a ktest seed.\n",
-          program_name);
-  fprintf(stderr, "Usage: %s <arguments>\n", program_name);
-  fprintf(stderr, "       <arguments> are the command-line arguments of the "
-                  "programs, with the following treated as special:\n");
-  fprintf(stderr, "       --sym-stdin <filename>      - Specifying a file that "
-                  "is the content of the stdin (only once).\n");
-  fprintf(stderr, "       --sym-stdout <filename>     - Specifying a file that "
-                  "is the content of the stdout (only once).\n");
-  fprintf(stderr, "       --sym-file <filename>       - Specifying a file that "
-                  "is the content of a file named A provided for the program "
-                  "(only once).\n");
-  fprintf(stderr, "   Ex: %s -o -p -q file1 --sym-stdin file2 --sym-file file3 "
-                  "--sym-stdout file4\n",
-          program_name);
+          "%s: Tool for generating a ktest file from concrete input, "
+          "e.g., for using a concrete crashing input as a ktest seed.\n"
+          "Usage: %s <arguments>\n"
+          "       <arguments> are the command-line arguments of the "
+          "program, with the following treated as special:\n"
+          "       --bout-file <filename>      - Specifying the output "
+          "file name for the ktest file (default: file.bout).\n"
+          "       --sym-stdin <filename>      - Specifying a file that "
+          "is the content of stdin (only once).\n"
+          "       --sym-stdout <filename>     - Specifying a file that "
+          "is the content of stdout (only once).\n"
+          "       --sym-file <filename>       - Specifying a file that "
+          "is the content of a file named A provided for the program "
+          "(only once).\n"
+          "   Ex: %s -o -p -q file1 --sym-stdin file2 --sym-file file3 "
+          "--sym-stdout file4\n",
+          program_name, program_name, program_name);
   exit(1);
 }
 
@@ -75,6 +76,7 @@ int main(int argc, char *argv[]) {
   char *stdin_content_filename = NULL;
   char *content_filenames_list[1024];
   char **argv_copy;
+  char *bout_file = NULL;
 
   if (argc < 2)
     print_usage_and_exit(argv[0]);
@@ -121,6 +123,12 @@ int main(int argc, char *argv[]) {
         print_usage_and_exit(argv[0]);
 
       content_filenames_list[file_counter++] = argv[i];
+    } else if (strcmp(argv[i], "--bout-file") == 0 ||
+               strcmp(argv[i], "-bout-file") == 0) {
+      if (++i == (unsigned)argc)
+        print_usage_and_exit(argv[0]);
+
+      bout_file = argv[i];
     } else {
       long nbytes = strlen(argv[i]) + 1;
       static int total_args = 0;
@@ -260,7 +268,7 @@ int main(int argc, char *argv[]) {
 
   push_range(&b, "model_version", 1);
 
-  if (!kTest_toFile(&b, "file.bout"))
+  if (!kTest_toFile(&b, bout_file ? bout_file : "file.bout"))
     assert(0);
 
   for (int i = 0; i < (int)b.numObjects; ++i) {
diff --git a/tools/gen-random-bout/gen-random-bout.cpp b/tools/gen-random-bout/gen-random-bout.cpp
index de1c6085..7d539606 100644
--- a/tools/gen-random-bout/gen-random-bout.cpp
+++ b/tools/gen-random-bout/gen-random-bout.cpp
@@ -138,13 +138,14 @@ int main(int argc, char *argv[]) {
   unsigned total_files = 0;
   unsigned file_sizes[MAX_FILE_SIZES];
   char **argv_copy;
+  char *bout_file = NULL;
 
   if (argc < 2) {
     error_exit(
         "Usage: %s <random-seed> <argument-types>\n"
         "       If <random-seed> is 0, time(NULL)*getpid() is used as a seed\n"
         "       <argument-types> are the ones accepted by KLEE: --sym-args, "
-        "--sym-files etc.\n"
+        "--sym-files etc. and --bout-file <filename> for the output file (default: random.bout).\n"
         "   Ex: %s 100 --sym-args 0 2 2 --sym-files 1 8\n",
         argv[0], argv[0]);
   }
@@ -226,6 +227,12 @@ int main(int argc, char *argv[]) {
         file_sizes[total_files++] = nbytes;
       }
 
+    } else if (strcmp(argv[i], "--bout-file") == 0 ||
+               strcmp(argv[i], "-bout-file") == 0) {
+      if ((unsigned)argc == ++i)
+        error_exit("Missing file name for --bout-file");
+
+      bout_file = argv[i];
     } else {
       error_exit("Unexpected option <%s>\n", argv[i]);
     }
@@ -273,8 +280,8 @@ int main(int argc, char *argv[]) {
   }
   push_range(&b, "model_version", 1);
 
-  if (!kTest_toFile(&b, "file.bout")) {
-    error_exit("Error in storing data into file.bout\n");
+  if (!kTest_toFile(&b, bout_file ? bout_file : "random.bout")) {
+    error_exit("Error in storing data into random.bout\n");
   }
 
   for (i = 0; i < b.numObjects; ++i) {