diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-09 05:40:06 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-09 05:40:06 +0000 |
commit | 1b0dfab63d317509f7cbf4d4cc2643fc86e90e4d (patch) | |
tree | 201c0a8be926b662df36c052dd95a08e53e188e8 /lib/Core/SeedInfo.cpp | |
parent | 6b97844651c092af6ff525d82f4f15c04cd927dc (diff) | |
download | klee-1b0dfab63d317509f7cbf4d4cc2643fc86e90e4d.tar.gz |
Kill off UpdateList::isRooted flag.
- The right way to handle this is by using constant arrays, where the semantics are easier to define and implement. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73124 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Core/SeedInfo.cpp')
-rw-r--r-- | lib/Core/SeedInfo.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 6fcfe596..dc3ff931 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -87,7 +87,7 @@ void SeedInfo::patchSeed(const ExecutionState &state, it = directReads.begin(), ie = directReads.end(); it != ie; ++it) { const Array *array = it->first; unsigned i = it->second; - ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0), + ref<Expr> read = ReadExpr::create(UpdateList(array, 0), ConstantExpr::alloc(i, Expr::Int32)); // If not in bindings then this can't be a violation? @@ -124,7 +124,7 @@ void SeedInfo::patchSeed(const ExecutionState &state, ie = assignment.bindings.end(); it != ie; ++it) { const Array *array = it->first; for (unsigned i=0; i<array->size; ++i) { - ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0), + ref<Expr> read = ReadExpr::create(UpdateList(array, 0), ConstantExpr::alloc(i, Expr::Int32)); ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)); bool res; |