diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2013-08-16 02:25:21 -0700 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2013-08-16 02:25:21 -0700 |
commit | c4147c2ad9ba1e74642e1a3de31be8f4446cc7f3 (patch) | |
tree | 9028ba3b5565e0d95b93cf55c7c05a4fb83f4488 /lib/Core | |
parent | 87968a53a31aaddb0c15b5d7078f6df05904fa0a (diff) | |
parent | 51f7cb3a3b494bd38ad9b3aec72a32f7973b8a06 (diff) | |
download | klee-c4147c2ad9ba1e74642e1a3de31be8f4446cc7f3.tar.gz |
Merge pull request #9 from delcypher/refactor-arg-init
Slight refactor of code initialising memory for argments/environment c-strings
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b57b1956..184b0983 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3219,24 +3219,20 @@ void Executor::runFunctionAsMain(Function *f, ObjectState *argvOS = bindObjectInState(*state, argvMO, false); for (int i=0; i<argc+1+envc+1+1; i++) { - MemoryObject *arg; - if (i==argc || i>=argc+1+envc) { - arg = 0; + // Write NULL pointer + argvOS->write(i * NumPtrBytes, Expr::createPointer(0)); } else { char *s = i<argc ? argv[i] : envp[i-(argc+1)]; int j, len = strlen(s); - arg = memory->allocate(len+1, false, true, state->pc->inst); + MemoryObject *arg = memory->allocate(len+1, false, true, state->pc->inst); ObjectState *os = bindObjectInState(*state, arg, false); for (j=0; j<len+1; j++) os->write8(j, s[j]); - } - if (arg) { + // Write pointer to newly allocated and initialised argv/envp c-string argvOS->write(i * NumPtrBytes, arg->getBaseExpr()); - } else { - argvOS->write(i * NumPtrBytes, Expr::createPointer(0)); } } } |