From b1d7d77a2b8380833853e6bdb000f2383ddd5814 Mon Sep 17 00:00:00 2001
From: Cristian Cadar
Date: Thu, 5 Apr 2012 17:47:31 +0000
Subject: Removed unnecessary --init-env option.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154110 91177308-0d34-0410-b5e6-96231b3b80d8
---
test/Runtime/POSIX/DirConsistency.c | 4 ++--
test/Runtime/POSIX/DirSeek.c | 6 +++---
test/Runtime/POSIX/FDNumbers.c | 2 +-
test/Runtime/POSIX/FD_Fail.c | 2 +-
test/Runtime/POSIX/FD_Fail2.c | 2 +-
test/Runtime/POSIX/Fcntl.c | 2 +-
test/Runtime/POSIX/FilePerm.c | 2 +-
test/Runtime/POSIX/FreeArgv.c | 2 +-
test/Runtime/POSIX/Getenv.c | 2 +-
test/Runtime/POSIX/Ioctl.c | 2 +-
test/Runtime/POSIX/Isatty.c | 2 +-
test/Runtime/POSIX/PrgName.c | 2 +-
test/Runtime/POSIX/Read1.c | 2 +-
test/Runtime/POSIX/SeedAndFail.c | 4 ++--
test/Runtime/POSIX/Stdin.c | 2 +-
test/Runtime/POSIX/Write1.c | 2 +-
test/Runtime/POSIX/Write2.c | 2 +-
tools/klee/main.cpp | 11 ++---------
www/TestingCoreutils.html | 18 +++++++++---------
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
#include
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
#include
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
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
#include
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
#include
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
#include
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
#include
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
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 --sym-argvs + file model options"),
cl::init(false));
cl::opt
@@ -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
- InitEnv("init-env",
- cl::desc("Create custom environment. Options that can be passed as arguments to the programs are: --sym-argv --sym-argvs + file model options"));
cl::opt
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
- When using uClibc and the POSIX runtime, KLEE offers an additional
- argument --init-env which replaces the programs main()
- function with a special function (klee_init_env) 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 main() function with a special function
+ (klee_init_env) 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 --help yields:
-src$ klee --libc=uclibc --posix-runtime --init-env ./echo.bc --help
+src$ klee --libc=uclibc --posix-runtime ./echo.bc --help
...
usage: (klee_init_env) [options] [program arguments]
@@ -388,7 +388,7 @@ usage: (klee_init_env) [options] [program arguments]
-src$ klee --libc=uclibc --posix-runtime --init-env ./echo.bc --sym-arg 3
+src$ klee --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3
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
-src$ klee --optimize --libc=uclibc --posix-runtime --init-env ./echo.bc --sym-arg 3
+src$ klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-arg 3
...
KLEE: done: total instructions = 123251
KLEE: done: completed paths = 25
@@ -802,7 +802,7 @@ Lines executed:50.50% of 101
-src$ klee --only-output-states-covering-new --optimize --libc=uclibc --posix-runtime --init-env ./echo.bc --sym-args 0 2 4
+src$ klee --only-output-states-covering-new --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-args 0 2 4
...
KLEE: done: total instructions = 7437521
KLEE: done: completed paths = 9963
--
cgit 1.4.1