diff options
| -rw-r--r-- | include/klee/Internal/Module/KInstruction.h | 12 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 8 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 4 | ||||
| -rw-r--r-- | test/CXX/ArrayNew.cpp | 5 |
4 files changed, 14 insertions, 15 deletions
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h index c91d37ab..89b9dbfc 100644 --- a/include/klee/Internal/Module/KInstruction.h +++ b/include/klee/Internal/Module/KInstruction.h @@ -10,6 +10,7 @@ #ifndef KLEE_KINSTRUCTION_H #define KLEE_KINSTRUCTION_H +#include "llvm/Support/DataTypes.h" #include <vector> namespace llvm { @@ -41,8 +42,15 @@ namespace klee { }; struct KGEPInstruction : KInstruction { - std::vector< std::pair<unsigned, unsigned> > indices; - unsigned offset; + /// indices - The list of variable sized adjustments to add to the pointer + /// operand to execute the instruction. The first element is the operand + /// index into the GetElementPtr instruction, and the second element is the + /// element size to multiple that index by. + std::vector< std::pair<unsigned, uint64_t> > indices; + + /// offset - A constant offset to add to the pointer operand to execute the + /// insturction. + uint64_t offset; }; } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e17d8d93..c69570ae 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1861,10 +1861,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki); ref<Expr> base = eval(ki, 0, state).value; - for (std::vector< std::pair<unsigned, unsigned> >::iterator + for (std::vector< std::pair<unsigned, uint64_t> >::iterator it = kgepi->indices.begin(), ie = kgepi->indices.end(); it != ie; ++it) { - unsigned elementSize = it->second; + uint64_t elementSize = it->second; ref<Expr> index = eval(ki, it->first, state).value; base = AddExpr::create(base, MulExpr::create(Expr::createCoerceToPointerType(index), @@ -2199,7 +2199,7 @@ void Executor::bindInstructionConstants(KInstruction *KI) { KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(KI); ref<ConstantExpr> constantOffset = ConstantExpr::alloc(0, Context::get().getPointerWidth()); - unsigned index = 1; + uint64_t index = 1; for (gep_type_iterator ii = gep_type_begin(gepi), ie = gep_type_end(gepi); ii != ie; ++ii) { if (const StructType *st = dyn_cast<StructType>(*ii)) { @@ -2210,7 +2210,7 @@ void Executor::bindInstructionConstants(KInstruction *KI) { Context::get().getPointerWidth())); } else { const SequentialType *st = cast<SequentialType>(*ii); - unsigned elementSize = + uint64_t elementSize = kmodule->targetData->getTypeStoreSize(st->getElementType()); Value *operand = ii.getOperand(); if (Constant *c = dyn_cast<Constant>(operand)) { diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index c23d626c..45202c19 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -330,8 +330,6 @@ void SpecialFunctionHandler::handleDelete(ExecutionState &state, void SpecialFunctionHandler::handleNewArray(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - // FIXME: This is broken, it doesn't allocate space for the count. - // XXX should type check args assert(arguments.size()==1 && "invalid number of arguments to new[]"); executor.executeAlloc(state, arguments[0], false, target); @@ -340,8 +338,6 @@ void SpecialFunctionHandler::handleNewArray(ExecutionState &state, void SpecialFunctionHandler::handleDeleteArray(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - // FIXME: This is broken, it doesn't allocate space for the count. - // XXX should type check args assert(arguments.size()==1 && "invalid number of arguments to delete[]"); executor.executeFree(state, arguments[0]); diff --git a/test/CXX/ArrayNew.cpp b/test/CXX/ArrayNew.cpp index 3402283f..e6a41ddf 100644 --- a/test/CXX/ArrayNew.cpp +++ b/test/CXX/ArrayNew.cpp @@ -1,10 +1,5 @@ -// FIXME: KLEE's new[] and delete[] implementations are broken, they don't -// allocate space for the count. - // RUN: %llvmgxx %s --emit-llvm -O0 -c -o %t1.bc // RUN: %klee --no-output --exit-on-error --no-externals %t1.bc -// RUN: false -// XFAIL: * #include <cassert> |