aboutsummaryrefslogtreecommitdiffhomepage
path: root/runtime
diff options
context:
space:
mode:
Diffstat (limited to 'runtime')
-rw-r--r--runtime/POSIX/fd.c14
1 files changed, 10 insertions, 4 deletions
diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index a2cbe0ab..ae08183f 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -1352,19 +1352,25 @@ static const char *__concretize_string(const char *s) {
char *sc = __concretize_ptr(s);
unsigned i;
- for (i=0; ; ++i) {
+ for (i = 0;; ++i, ++sc) {
char c = *sc;
+ // Avoid writing read-only memory locations
+ if (!klee_is_symbolic(c)) {
+ if (!c)
+ break;
+ continue;
+ }
if (!(i&(i-1))) {
if (!c) {
- *sc++ = 0;
+ *sc = 0;
break;
} else if (c=='/') {
- *sc++ = '/';
+ *sc = '/';
}
} else {
char cc = (char) klee_get_valuel((long)c);
klee_assume(cc == c);
- *sc++ = cc;
+ *sc = cc;
if (!cc) break;
}
}