Sergey Morozov

Klee ignores concretization effects in `callExternalFunction`

6

Consider the following code: ```c #include #include #include "klee/klee.h" int main() { int x = klee_int("x"); int y = abs(x); if (x >= 0) { klee_assert(y == x); } }...

https://github.com/UnitTestBot/klee/blob/e1a2b064fcb0fe4a891c18f6310334b4ff6a87f7/lib/Core/Executor.cpp#L2918 ``` case Instruction::BitCast: { ref result = eval(ki, 0, state).value; BitCastInst *bc = cast(ki->inst); if(UseGEPExpr && isGEPExpr(result)) { unsigned size = bc->getType()->isPointerTy() ? kmodule->targetData->getTypeStoreSize(ki->inst->getType()->getPointerElementType()) : kmodule->targetData->getTypeStoreSize(ki->inst->getType()); gepExprBases[result] = {gepExprBases[result].first,...