klee
Assignment.cpp
Go to the documentation of this file.
1//===-- Assignment.cpp ----------------------------------------------------===//
2//
3// The KLEE Symbolic Virtual Machine
4//
5// This file is distributed under the University of Illinois Open Source
6// License. See LICENSE.TXT for details.
7//
8//===----------------------------------------------------------------------===//
9
11
12namespace klee {
13
15 if (bindings.size() == 0) {
16 llvm::errs() << "No bindings\n";
17 return;
18 }
19 for (bindings_ty::iterator i = bindings.begin(), e = bindings.end(); i != e;
20 ++i) {
21 llvm::errs() << (*i).first->name << "\n[";
22 for (int j = 0, k = (*i).second.size(); j < k; ++j)
23 llvm::errs() << (int)(*i).second[j] << ",";
24 llvm::errs() << "]\n";
25 }
26}
27
29 ConstraintSet result;
30 for (const auto &binding : bindings) {
31 const auto &array = binding.first;
32 const auto &values = binding.second;
33
34 for (unsigned arrayIndex = 0; arrayIndex < array->size; ++arrayIndex) {
35 unsigned char value = values[arrayIndex];
36 result.push_back(EqExpr::create(
38 ConstantExpr::alloc(arrayIndex, array->getDomain())),
39 ConstantExpr::alloc(value, array->getRange())));
40 }
41 }
42 return result;
43}
44}
ConstraintSet createConstraintsFromAssignment() const
Definition: Assignment.cpp:28
bindings_ty bindings
Definition: Assignment.h:26
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:1065
void push_back(const ref< Expr > &e)
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:538
Class representing a complete list of updates into an array.
Definition: Expr.h:539
Definition: main.cpp:291