diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2015-02-27 19:03:46 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2015-02-27 19:03:46 +0000 |
commit | 1c10b2b52a4f91f62bc9ef632032d7f0ade0307c (patch) | |
tree | 6ba801b9e1aa4c24fd87fa830674881ffe7802e6 /lib | |
parent | 35117b9f9273d2465abe56ef11f89ca7477e3d91 (diff) | |
download | klee-1c10b2b52a4f91f62bc9ef632032d7f0ade0307c.tar.gz |
Improved some comments and fixed some formatting issues in the Array factory patch.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 2 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 4 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 17 | ||||
-rw-r--r-- | lib/Expr/Parser.cpp | 2 |
4 files changed, 12 insertions, 13 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8631061f..c78c9f8a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2925,7 +2925,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, static unsigned id; const Array *array = Array::CreateArray("rrws_arr" + llvm::utostr(++id), - Expr::getMinBytesForWidth(e->getWidth())); + Expr::getMinBytesForWidth(e->getWidth())); ref<Expr> res = Expr::createTempRead(array, e->getWidth()); ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res)); llvm::errs() << "Making symbolic: " << eq << "\n"; diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index b9f6afd0..1dd1e1fd 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -223,8 +223,8 @@ const UpdateList &ObjectState::getUpdates() const { // FIXME: Leaked. static unsigned id = 0; const Array *array = Array::CreateArray("const_arr" + llvm::utostr(++id), size, - &Contents[0], - &Contents[0] + Contents.size()); + &Contents[0], + &Contents[0] + Contents.size()); updates = UpdateList(array, 0); // Apply the remaining (non-constant) writes. diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 46ea30fc..baa85663 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -501,31 +501,30 @@ const Array * Array::CreateArray(const std::string &_name, uint64_t _size, const ref<ConstantExpr> *constantValuesBegin, const ref<ConstantExpr> *constantValuesEnd, Expr::Width _domain, - Expr::Width _range){ + Expr::Width _range) { const Array * array = new Array(_name, _size, constantValuesBegin, constantValuesEnd, _domain,_range); - if(array->constantValues.size() == 0){ - //means is a symbolic array and we should look up the values; + if (array->constantValues.size() == 0) { // symbolic array unsigned hash = array->hash(); std::vector<const Array *> * bucket = Array::symbolicArraySingletonMap[hash]; - if(bucket){ - for(std::vector<const Array*>::const_iterator it = bucket->begin(); - it != bucket->end(); it ++){ + if (bucket){ + for (std::vector<const Array*>::const_iterator it = bucket->begin(); + it != bucket->end(); it ++){ const Array* prospect = *it; - if(prospect->size == array->size && prospect->name == array->name){ + if (prospect->size == array->size && prospect->name == array->name){ delete array; return prospect; } } bucket->push_back(array); return array; - }else{ + } else { bucket = new std::vector<const Array *>(); bucket->push_back(array); Array::symbolicArraySingletonMap[hash] = bucket; return array; } - }else{ + } else { // concrete array return array; } } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 9df08903..23a292fa 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -522,7 +522,7 @@ DeclResult ParserImpl::ParseArrayDecl() { const Array *Root; if (!Values.empty()) Root = Array::CreateArray(Label->Name, Size.get(), - &Values[0], &Values[0] + Values.size()); + &Values[0], &Values[0] + Values.size()); else Root = Array::CreateArray(Label->Name, Size.get()); ArrayDecl *AD = new ArrayDecl(Label, Size.get(), |