about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test/Runtime/POSIX/DirConsistency.c4
-rw-r--r--test/Runtime/POSIX/DirSeek.c6
-rw-r--r--test/Runtime/POSIX/FDNumbers.c2
-rw-r--r--test/Runtime/POSIX/FD_Fail.c2
-rw-r--r--test/Runtime/POSIX/FD_Fail2.c2
-rw-r--r--test/Runtime/POSIX/Fcntl.c2
-rw-r--r--test/Runtime/POSIX/FilePerm.c2
-rw-r--r--test/Runtime/POSIX/FreeArgv.c2
-rw-r--r--test/Runtime/POSIX/Getenv.c2
-rw-r--r--test/Runtime/POSIX/Ioctl.c2
-rw-r--r--test/Runtime/POSIX/Isatty.c2
-rw-r--r--test/Runtime/POSIX/PrgName.c2
-rw-r--r--test/Runtime/POSIX/Read1.c2
-rw-r--r--test/Runtime/POSIX/SeedAndFail.c4
-rw-r--r--test/Runtime/POSIX/Stdin.c2
-rw-r--r--test/Runtime/POSIX/Write1.c2
-rw-r--r--test/Runtime/POSIX/Write2.c2
-rw-r--r--tools/klee/main.cpp11
-rw-r--r--www/TestingCoreutils.html18
19 files changed, 32 insertions, 39 deletions
diff --git a/test/Runtime/POSIX/DirConsistency.c b/test/Runtime/POSIX/DirConsistency.c
index 613655e9..30696650 100644
--- a/test/Runtime/POSIX/DirConsistency.c
+++ b/test/Runtime/POSIX/DirConsistency.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --run-in=/tmp --use-random-search --init-env --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
+// RUN: %klee --run-in=/tmp --use-random-search --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
 // RUN: %llvmgcc -D_FILE_OFFSET_BITS=64 %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --run-in=/tmp --use-random-search --init-env --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
+// RUN: %klee --run-in=/tmp --use-random-search --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
 // RUN: sort %t1.log %t2.log | uniq -c > %t3.log
 // RUN: grep -q "4 COUNT" %t3.log
 
diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c
index 1735fdb8..81336a68 100644
--- a/test/Runtime/POSIX/DirSeek.c
+++ b/test/Runtime/POSIX/DirSeek.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --run-in=/tmp --init-env --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 2 2
-// RUN: %klee --run-in=/tmp --init-env --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2
-// RUN: %klee --run-in=/tmp --init-env --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 0 2
+// RUN: %klee --run-in=/tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 2 2
+// RUN: %klee --run-in=/tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2
+// RUN: %klee --run-in=/tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 0 2
 
 // For this test really to work as intended it needs to be run in a
 // directory large enough to cause uclibc to do multiple getdents
diff --git a/test/Runtime/POSIX/FDNumbers.c b/test/Runtime/POSIX/FDNumbers.c
index e576f9bb..3228c8a9 100644
--- a/test/Runtime/POSIX/FDNumbers.c
+++ b/test/Runtime/POSIX/FDNumbers.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --init-env --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
 
 #include <assert.h>
 #include <fcntl.h>
diff --git a/test/Runtime/POSIX/FD_Fail.c b/test/Runtime/POSIX/FD_Fail.c
index cf1d4d5a..a4bf2fc2 100644
--- a/test/Runtime/POSIX/FD_Fail.c
+++ b/test/Runtime/POSIX/FD_Fail.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --libc=uclibc --posix-runtime --init-env %t1.bc --sym-files 0 0 --max-fail 1 > %t.log
+// RUN: %klee --libc=uclibc --posix-runtime %t1.bc --sym-files 0 0 --max-fail 1 > %t.log
 // RUN: grep -q "fread(): ok" %t.log
 // RUN: grep -q "fread(): fail" %t.log
 // RUN: grep -q "fclose(): ok" %t.log
diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c
index 1eaeb649..062f7027 100644
--- a/test/Runtime/POSIX/FD_Fail2.c
+++ b/test/Runtime/POSIX/FD_Fail2.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --libc=uclibc --posix-runtime --init-env %t1.bc --sym-files 0 0 --max-fail 1
+// RUN: %klee --libc=uclibc --posix-runtime %t1.bc --sym-files 0 0 --max-fail 1
 // RUN: test -f klee-last/test000001.ktest
 // RUN: test -f klee-last/test000002.ktest
 // RUN: test -f klee-last/test000003.ktest
diff --git a/test/Runtime/POSIX/Fcntl.c b/test/Runtime/POSIX/Fcntl.c
index 139fb1f3..1b37e711 100644
--- a/test/Runtime/POSIX/Fcntl.c
+++ b/test/Runtime/POSIX/Fcntl.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --init-env --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
 
 #include <assert.h>
 #include <fcntl.h>
diff --git a/test/Runtime/POSIX/FilePerm.c b/test/Runtime/POSIX/FilePerm.c
index 0cb0a7e8..d387c2a9 100644
--- a/test/Runtime/POSIX/FilePerm.c
+++ b/test/Runtime/POSIX/FilePerm.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --posix-runtime --init-env %t.bc --sym-files 1 10 --sym-stdout 2>%t.log 
+// RUN: %klee --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log 
 // RUN: test -f klee-last/test000001.ktest
 // RUN: test -f klee-last/test000002.ktest
 // RUN: test -f klee-last/test000003.ktest
diff --git a/test/Runtime/POSIX/FreeArgv.c b/test/Runtime/POSIX/FreeArgv.c
index 37909b80..ceec4de2 100644
--- a/test/Runtime/POSIX/FreeArgv.c
+++ b/test/Runtime/POSIX/FreeArgv.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --init-env --posix-runtime %t.bc --sym-args 1 1 1
+// RUN: %klee --posix-runtime %t.bc --sym-args 1 1 1
 // RUN: test -f klee-last/test000001.free.err
 // RUN: test -f klee-last/test000002.free.err
 // RUN: test -f klee-last/test000003.free.err
diff --git a/test/Runtime/POSIX/Getenv.c b/test/Runtime/POSIX/Getenv.c
index 7ec66788..9d5672f7 100644
--- a/test/Runtime/POSIX/Getenv.c
+++ b/test/Runtime/POSIX/Getenv.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --init-env --libc=klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: %klee --libc=klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
 
 #include <assert.h>
 
diff --git a/test/Runtime/POSIX/Ioctl.c b/test/Runtime/POSIX/Ioctl.c
index 0e7b2cad..93ce4b5c 100644
--- a/test/Runtime/POSIX/Ioctl.c
+++ b/test/Runtime/POSIX/Ioctl.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --init-env --posix-runtime --exit-on-error %t.bc --sym-files 0 4
+// RUN: %klee --posix-runtime --exit-on-error %t.bc --sym-files 0 4
 
 #include <assert.h>
 #include <fcntl.h>
diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c
index 294312dc..4f8d1425 100644
--- a/test/Runtime/POSIX/Isatty.c
+++ b/test/Runtime/POSIX/Isatty.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 0 10 --sym-stdout 2>%t.log
+// RUN: %klee --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout 2>%t.log
 
 // RUN: test -f klee-last/test000001.ktest
 // RUN: test -f klee-last/test000002.ktest
diff --git a/test/Runtime/POSIX/PrgName.c b/test/Runtime/POSIX/PrgName.c
index 5bed4335..dc6a4b8c 100644
--- a/test/Runtime/POSIX/PrgName.c
+++ b/test/Runtime/POSIX/PrgName.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
-// RUN: %klee --init-env --posix-runtime --exit-on-error %t2.bc --sym-arg 10 >%t.log
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-arg 10 >%t.log
 // RUN: test -f klee-last/test000001.ktest
 // RUN: test -f klee-last/test000002.ktest
 // RUN: grep -q "No" %t.log
diff --git a/test/Runtime/POSIX/Read1.c b/test/Runtime/POSIX/Read1.c
index 3b24bfb9..66831073 100644
--- a/test/Runtime/POSIX/Read1.c
+++ b/test/Runtime/POSIX/Read1.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --exit-on-error --posix-runtime --init-env %t.bc --sym-files 1 8 >%t.log
+// RUN: %klee --exit-on-error --posix-runtime %t.bc --sym-files 1 8 >%t.log
 
 #include <unistd.h>
 #include <sys/types.h>
diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c
index 4d81e2d7..db02217a 100644
--- a/test/Runtime/POSIX/SeedAndFail.c
+++ b/test/Runtime/POSIX/SeedAndFail.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf tmp-123
-// RUN: %klee --libc=klee --output-dir=tmp-123 --posix-runtime --init-env %t.bc --sym-files 1 10  2>%t.log
-// RUN: %klee --seed-out-dir=tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 1 10 --max-fail 1
+// RUN: %klee --libc=klee --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10  2>%t.log
+// RUN: %klee --seed-out-dir=tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1
 // RUN: ls klee-last | grep -c assert | grep 4
 
 
diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c
index 065533a1..e7e3f2ff 100644
--- a/test/Runtime/POSIX/Stdin.c
+++ b/test/Runtime/POSIX/Stdin.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --init-env --libc=klee --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
+// RUN: %klee --libc=klee --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
 // RUN: grep "mode:file" %t.log
 // RUN: grep "mode:dir" %t.log
 // RUN: grep "mode:chr" %t.log
diff --git a/test/Runtime/POSIX/Write1.c b/test/Runtime/POSIX/Write1.c
index 73902363..16132b82 100644
--- a/test/Runtime/POSIX/Write1.c
+++ b/test/Runtime/POSIX/Write1.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --exit-on-error --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
+// RUN: %klee --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
 
 #include <stdio.h>
 #include <assert.h>
diff --git a/test/Runtime/POSIX/Write2.c b/test/Runtime/POSIX/Write2.c
index 4865b479..9801e70c 100644
--- a/test/Runtime/POSIX/Write2.c
+++ b/test/Runtime/POSIX/Write2.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --exit-on-error --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
+// RUN: %klee --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
 
 #include <stdio.h>
 #include <assert.h>
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 78e0d394..68ef98d4 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -132,7 +132,7 @@ namespace {
     
   cl::opt<bool>
   WithPOSIXRuntime("posix-runtime", 
-		cl::desc("Link with POSIX runtime"),
+		cl::desc("Link with POSIX runtime.  Options that can be passed as arguments to the programs are: --sym-argv <max-len>  --sym-argvs <min-argvs> <max-argvs> <max-len> + file model options"),
 		cl::init(false));
     
   cl::opt<bool>
@@ -184,10 +184,6 @@ namespace {
   MakeConcreteSymbolic("make-concrete-symbolic",
                        cl::desc("Rate at which to make concrete reads symbolic (0=off)"),
                        cl::init(0));
-
-  cl::opt<bool>
-  InitEnv("init-env",
-	  cl::desc("Create custom environment.  Options that can be passed as arguments to the programs are: --sym-argv <max-len>  --sym-argvs <min-argvs> <max-argvs> <max-len> + file model options"));
  
   cl::opt<unsigned>
   StopAfterNTests("stop-after-n-tests",
@@ -1205,10 +1201,7 @@ int main(int argc, char **argv, char **envp) {
     klee_error("error loading program '%s': %s", InputFile.c_str(),
                ErrorMsg.c_str());
 
-  if (WithPOSIXRuntime)
-    InitEnv = true;
-
-  if (InitEnv) {
+  if (WithPOSIXRuntime) {
     int r = initEnv(mainModule);
     if (r != 0)
       return r;
diff --git a/www/TestingCoreutils.html b/www/TestingCoreutils.html
index 07169efe..3465382f 100644
--- a/www/TestingCoreutils.html
+++ b/www/TestingCoreutils.html
@@ -356,17 +356,17 @@ KLEE: done: generated tests = 1
   </p>
   
   <p>
-    When using uClibc and the POSIX runtime, KLEE offers an additional
-    argument <tt>--init-env</tt> which replaces the programs <tt>main()</tt>
-    function with a special function (<tt>klee_init_env</tt>) provided inside
-    the runtime library. This function alters the normal command line processing
-    of the application, in particular to support construction of symbolic
+    When using uClibc and the POSIX runtime, KLEE replaces the
+    program's <tt>main()</tt> function with a special function
+    (<tt>klee_init_env</tt>) provided inside the runtime library. This
+    function alters the normal command line processing of the
+    application, in particular to support construction of symbolic
     arguments. For example, passing <tt>--help</tt> yields:
   </p>
 
   <div class="instr">
     <pre>
-<b>src$ klee --libc=uclibc --posix-runtime --init-env ./echo.bc --help</b>
+<b>src$ klee --libc=uclibc --posix-runtime ./echo.bc --help</b>
 <i>...</i>
 
 usage: (klee_init_env) [options] [program arguments]
@@ -388,7 +388,7 @@ usage: (klee_init_env) [options] [program arguments]
 
   <div class="instr">
     <pre>
-<b>src$ klee --libc=uclibc --posix-runtime --init-env ./echo.bc --sym-arg 3</b>
+<b>src$ klee --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3</b>
 KLEE: NOTE: Using model: /home/ddunbar/public/klee/Release/lib/libkleeRuntimePOSIX.bca
 KLEE: output directory = "klee-out-16"
 KLEE: WARNING: undefined reference to function: __signbitl
@@ -495,7 +495,7 @@ KLEE: done: generated tests = 25<pre>
 
   <div class="instr">
     <pre>
-<b>src$ klee --optimize --libc=uclibc --posix-runtime --init-env ./echo.bc --sym-arg 3</b>
+<b>src$ klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3</b>
 <i>...</i>
 KLEE: done: total instructions = 123251
 KLEE: done: completed paths = 25
@@ -802,7 +802,7 @@ Lines executed:50.50% of 101
 
   <div class="instr">
     <pre>
-<b>src$ klee --only-output-states-covering-new --optimize --libc=uclibc --posix-runtime --init-env ./echo.bc --sym-args 0 2 4</b>
+<b>src$ klee --only-output-states-covering-new --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-args 0 2 4</b>
 <i> ... </i>
 KLEE: done: total instructions = 7437521
 KLEE: done: completed paths = 9963
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 05:35:28 +0000