Add checks for correct usage of the POSIX model, together with an associated test.

2 files changed, 40 insertions, 0 deletions

diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 265c3bfd..511a926c 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -144,6 +144,9 @@ usage: (klee_init_env) [options] [program arguments]\n\
       max_argvs = __str_to_int(argv[k++], msg);
       max_len = __str_to_int(argv[k++], msg);
 
+      if ( (min_argvs > max_argvs) || (min_argvs == 0 && max_argvs == 0) )
+        __emit_error("Invalid range to --sym-args");
+
       n_args = klee_range(min_argvs, max_argvs+1, "n_args");
       for (i=0; i < n_args; i++) {
         sym_arg_name[3] = '0' + sym_arg_num++;
@@ -157,11 +160,20 @@ usage: (klee_init_env) [options] [program arguments]\n\
 
       if (k+2 >= argc)
 	__emit_error(msg);
+
+      if (sym_files != 0)
+        __emit_error("Multiple --sym-files are not allowed.\n");
       
       k++;
       sym_files = __str_to_int(argv[k++], msg);
       sym_file_len = __str_to_int(argv[k++], msg);
 
+      if (sym_files == 0)
+        __emit_error("The first argument to --sym-files (number of files) cannot be 0\n");
+
+      if (sym_file_len == 0)
+        __emit_error("The second argument to --sym-files (file size) cannot be 0\n");
+
     } else if (__streq(argv[k], "--sym-stdin") ||
                __streq(argv[k], "-sym-stdin")) {
       const char *msg =
diff --git a/test/Runtime/POSIX/Usage.c b/test/Runtime/POSIX/Usage.c
new file mode 100644
index 00000000..ce338e5c
--- /dev/null
+++ b/test/Runtime/POSIX/Usage.c
@@ -0,0 +1,28 @@
+// This test checks for the (in)correct use of --sym-files and --sym-args
+
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+
+// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --posix-runtime %t.bc --sym-files 1 10 --sym-files 2 10 &> %t1
+// RUN: grep "Multiple --sym-files are not allowed" %t1
+// RUN: rm -rf %t.klee-out
+
+// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --posix-runtime %t.bc --sym-files 0 10 &> %t2
+// RUN: grep "The first argument to --sym-files (number of files) cannot be 0" %t2
+// RUN: rm -rf %t.klee-out
+
+// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --posix-runtime %t.bc --sym-files 2 0 &> %t3
+// RUN: grep "The second argument to --sym-files (file size) cannot be 0" %t3
+// RUN: rm -rf %t.klee-out
+
+// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --posix-runtime %t.bc --sym-args 3 2 10 &> %t4
+// RUN: grep "Invalid range to --sym-args" %t4
+// RUN: rm -rf %t.klee-out
+
+// RUN: not %klee --output-dir=%t.klee-out --exit-on-error --posix-runtime %t.bc --sym-args 0 0 10 &> %t5
+// RUN: grep "Invalid range to --sym-args" %t5
+// RUN: rm -rf %t.klee-out
+
+int main(int argc, char** argv) {
+  return 0;
+}