 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
59.1% |
13 / 22 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
90.9% |
20 / 22 |
| |
|
Line Coverage: |
64.5% |
20 / 31 |
| |
 |
|
 |
1 : #include "klee/util/ExprEvaluator.h"
2 : // FIXME: This should not be here.
3 : #include "klee/Memory.h"
4 :
5 : using namespace klee;
6 :
7 : ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
8 20746: unsigned index) {
128438: branch 2 taken
17351: branch 3 taken
9 145789: for (const UpdateNode *un=ul.head; un; un=un->next) {
10 128438: ref<Expr> ui = visit(un->index);
11 :
128438: branch 0 taken
0: branch 1 not taken
12 128438: if (ui.isConstant()) {
3395: branch 0 taken
125043: branch 1 taken
13 128438: if (ui.getConstantValue() == index)
14 6790: return Action::changeTo(visit(un->value));
15 : } else {
16 : // update index is unknown, so may or may not be index, we
17 : // cannot guarantee value. we can rewrite to read at this
18 : // version though (mostly for debugging).
19 :
20 0: UpdateList fwd(ul.root, un, 0);
21 : return Action::changeTo(ReadExpr::create(fwd,
22 0: ref<Expr>(index,Expr::Int32)));
23 : }
24 : }
25 :
26 34702: return Action::changeTo(getInitialValue(*ul.root, index));
27 : }
28 :
29 20746: ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
30 20746: ref<Expr> v = visit(re.index);
31 :
20746: branch 0 taken
0: branch 1 not taken
32 20746: if (v.isConstant()) {
33 41492: return evalRead(re.updates, v.getConstantValue());
34 : } else {
35 0: return Action::doChildren();
36 20746: }
37 : }
38 :
39 : // we need to check for div by zero during partial evaluation,
40 : // if this occurs then simply ignore the 0 divisor and use the
41 : // original expression.
42 8: ExprVisitor::Action ExprEvaluator::protectedDivOperation(const BinaryExpr &e) {
43 : ref<Expr> kids[2] = { visit(e.left),
44 8: visit(e.right) };
45 :
8: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
8: branch 3 taken
0: branch 4 not taken
8: branch 5 taken
46 16: if (kids[1].isConstant() && !kids[1].getConstantValue())
47 0: kids[1] = e.right;
48 :
0: branch 1 not taken
8: branch 2 taken
0: branch 4 not taken
0: branch 5 not taken
8: branch 6 taken
0: branch 7 not taken
49 8: if (kids[0]!=e.left || kids[1]!=e.right) {
50 16: return Action::changeTo(e.rebuild(kids));
51 : } else {
52 0: return Action::skipChildren();
16: branch 0 taken
8: branch 1 taken
53 8: }
54 : }
55 :
56 0: ExprVisitor::Action ExprEvaluator::visitUDiv(const UDivExpr &e) {
57 0: return protectedDivOperation(e);
58 : }
59 8: ExprVisitor::Action ExprEvaluator::visitSDiv(const SDivExpr &e) {
60 8: return protectedDivOperation(e);
61 : }
62 0: ExprVisitor::Action ExprEvaluator::visitURem(const URemExpr &e) {
63 0: return protectedDivOperation(e);
64 : }
65 0: ExprVisitor::Action ExprEvaluator::visitSRem(const SRemExpr &e) {
66 0: return protectedDivOperation(e);
67 : }
Generated: 2009-05-17 22:47 by zcov