Hello,
I believe there's a bug in ObjectState::read. On big endian architectures,
ObjectState::read will always return a one byte value. I actually don't
have a test case for this, it's just something I noticed while perusing
code. Patch for lib/Core/Memory.cpp attached.
-Tom
--- Memory.cpp 2011-10-23 21:19:48.000000000 -0700
+++ Memory.cpp 2011-11-03 13:49:22.000000000 -0700
@@ -450,7 +450,7 @@
ref<Expr> Byte = read8(AddExpr::create(offset,
ConstantExpr::create(idx,
Expr::Int32)));
- Res = idx ? ConcatExpr::create(Byte, Res) : Byte;
+ Res = i ? ConcatExpr::create(Byte, Res) : Byte;
}
return Res;
@@ -468,7 +468,7 @@
for (unsigned i = 0; i != NumBytes; ++i) {
unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
ref<Expr> Byte = read8(offset + idx);
- Res = idx ? ConcatExpr::create(Byte, Res) : Byte;
+ Res = i ? ConcatExpr::create(Byte, Res) : Byte;
}
return Res;
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
