summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--klee/test/Runtime/POSIX/DirConsistency.c4
-rw-r--r--klee/test/Runtime/POSIX/DirSeek.c6
-rw-r--r--klee/test/Runtime/POSIX/FDNumbers.c2
-rw-r--r--klee/test/Runtime/POSIX/FD_Fail.c2
-rw-r--r--klee/test/Runtime/POSIX/FD_Fail2.c2
-rw-r--r--klee/test/Runtime/POSIX/Fcntl.c2
-rw-r--r--klee/test/Runtime/POSIX/FilePerm.c2
-rw-r--r--klee/test/Runtime/POSIX/FreeArgv.c2
-rw-r--r--klee/test/Runtime/POSIX/Getenv.c2
-rw-r--r--klee/test/Runtime/POSIX/Ioctl.c2
-rw-r--r--klee/test/Runtime/POSIX/Isatty.c2
-rw-r--r--klee/test/Runtime/POSIX/PrgName.c2
-rw-r--r--klee/test/Runtime/POSIX/Read1.c2
-rw-r--r--klee/test/Runtime/POSIX/SeedAndFail.c4
-rw-r--r--klee/test/Runtime/POSIX/Stdin.c2
-rw-r--r--klee/test/Runtime/POSIX/Write1.c2
-rw-r--r--klee/test/Runtime/POSIX/Write2.c2
-rw-r--r--klee/tools/klee/main.cpp11
-rw-r--r--klee/www/TestingCoreutils.html18
19 files changed, 32 insertions, 39 deletions
diff --git a/klee/test/Runtime/POSIX/DirConsistency.c b/klee/test/Runtime/POSIX/DirConsistency.c
index 613655e9c23..30696650102 100644
--- a/klee/test/Runtime/POSIX/DirConsistency.c
+++ b/klee/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/klee/test/Runtime/POSIX/DirSeek.c b/klee/test/Runtime/POSIX/DirSeek.c
index 1735fdb850c..81336a689ba 100644
--- a/klee/test/Runtime/POSIX/DirSeek.c
+++ b/klee/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/klee/test/Runtime/POSIX/FDNumbers.c b/klee/test/Runtime/POSIX/FDNumbers.c
index e576f9bbe23..3228c8a9f2d 100644
--- a/klee/test/Runtime/POSIX/FDNumbers.c
+++ b/klee/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/klee/test/Runtime/POSIX/FD_Fail.c b/klee/test/Runtime/POSIX/FD_Fail.c
index cf1d4d5a758..a4bf2fc2222 100644
--- a/klee/test/Runtime/POSIX/FD_Fail.c
+++ b/klee/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/klee/test/Runtime/POSIX/FD_Fail2.c b/klee/test/Runtime/POSIX/FD_Fail2.c
index 1eaeb649186..062f7027006 100644
--- a/klee/test/Runtime/POSIX/FD_Fail2.c
+++ b/klee/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/klee/test/Runtime/POSIX/Fcntl.c b/klee/test/Runtime/POSIX/Fcntl.c
index 139fb1f3ed1..1b37e711b1f 100644
--- a/klee/test/Runtime/POSIX/Fcntl.c
+++ b/klee/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/klee/test/Runtime/POSIX/FilePerm.c b/klee/test/Runtime/POSIX/FilePerm.c
index 0cb0a7e8ee1..d387c2a961d 100644
--- a/klee/test/Runtime/POSIX/FilePerm.c
+++ b/klee/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/klee/test/Runtime/POSIX/FreeArgv.c b/klee/test/Runtime/POSIX/FreeArgv.c
index 37909b80a8b..ceec4de2d5e 100644
--- a/klee/test/Runtime/POSIX/FreeArgv.c
+++ b/klee/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/klee/test/Runtime/POSIX/Getenv.c b/klee/test/Runtime/POSIX/Getenv.c
index 7ec667882de..9d5672f7dbf 100644
--- a/klee/test/Runtime/POSIX/Getenv.c
+++ b/klee/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/klee/test/Runtime/POSIX/Ioctl.c b/klee/test/Runtime/POSIX/Ioctl.c
index 0e7b2cad651..93ce4b5c784 100644
--- a/klee/test/Runtime/POSIX/Ioctl.c
+++ b/klee/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/klee/test/Runtime/POSIX/Isatty.c b/klee/test/Runtime/POSIX/Isatty.c
index 294312dc74c..4f8d142577a 100644
--- a/klee/test/Runtime/POSIX/Isatty.c
+++ b/klee/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/klee/test/Runtime/POSIX/PrgName.c b/klee/test/Runtime/POSIX/PrgName.c
index 5bed4335cdf..dc6a4b8c55c 100644
--- a/klee/test/Runtime/POSIX/PrgName.c
+++ b/klee/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/klee/test/Runtime/POSIX/Read1.c b/klee/test/Runtime/POSIX/Read1.c
index 3b24bfb9eee..66831073b6a 100644
--- a/klee/test/Runtime/POSIX/Read1.c
+++ b/klee/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/klee/test/Runtime/POSIX/SeedAndFail.c b/klee/test/Runtime/POSIX/SeedAndFail.c
index 4d81e2d78a9..db02217a42b 100644
--- a/klee/test/Runtime/POSIX/SeedAndFail.c
+++ b/klee/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/klee/test/Runtime/POSIX/Stdin.c b/klee/test/Runtime/POSIX/Stdin.c
index 065533a1667..e7e3f2ff19d 100644
--- a/klee/test/Runtime/POSIX/Stdin.c
+++ b/klee/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/klee/test/Runtime/POSIX/Write1.c b/klee/test/Runtime/POSIX/Write1.c
index 73902363ccd..16132b8284f 100644
--- a/klee/test/Runtime/POSIX/Write1.c
+++ b/klee/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/klee/test/Runtime/POSIX/Write2.c b/klee/test/Runtime/POSIX/Write2.c
index 4865b479e65..9801e70c6b4 100644
--- a/klee/test/Runtime/POSIX/Write2.c
+++ b/klee/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/klee/tools/klee/main.cpp b/klee/tools/klee/main.cpp
index 78e0d3948fc..68ef98d48e4 100644
--- a/klee/tools/klee/main.cpp
+++ b/klee/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/klee/www/TestingCoreutils.html b/klee/www/TestingCoreutils.html
index 07169efefab..3465382f253 100644
--- a/klee/www/TestingCoreutils.html
+++ b/klee/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 v1.2.3 (git 2.25.1) at 2024-07-10 21:20:13 +0000