[klee-dev] Making a copy of std::vector<const Array*> objects

Younghwan Go yhwan at ndsl.kaist.edu
Tue Jul 29 14:36:16 BST 2014


Hello everyone,

I've been working on modifying klee to pass multiple queries to stp
solver at the same time. I got the most part working but faced a problem
when gathering "std::vector<const Array*> objects", which store the
symbolic objects to be passed to the solver.

Since it's a vector of class pointer, I tried to copy every element
while iterating through the vector as shown below.

std::vector<const Array*> new_objects;
for (std::vector<const Array*>::const_iterator it = objects.begin(), ie
= objects.end(); it != ie; ++it) {
const Array *array = *it;
const Array *copy = array->clone();
new_objects.push_back(copy); *// crash here*
}

Since the class Array didn't provide any copy constructor, I implemented
my own version in Expr.h as below.

Array(const Array &orig) : name(orig.name), size(orig.size),
constantValues(orig.constantValues), domain(orig.domain),
range(orig.range) {
computeHash();
}
Array* clone() const { return (new Array(*this)); }

I'm guessing that the copying is done incorrectly, which causes
push_back() function to crash. If anyone can shed some light on this,
it'll be a great help. Also if anyone knows a better way to copy objects
vector, please share!

Regards,
Younghwan

-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list