 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
82.9% |
58 / 70 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
68.6% |
48 / 70 |
| |
|
Line Coverage: |
97.0% |
64 / 66 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/Expr.h"
4 : // FIXME: This should not be here.
5 : #include "klee/Memory.h"
6 :
7 : #include <cassert>
8 :
9 : using namespace klee;
10 :
11 : ///
12 :
13 : UpdateNode::UpdateNode(const UpdateNode *_next,
14 : const ref<Expr> &_index,
15 9458: const ref<Expr> &_value)
16 : : refCount(0),
17 : stpArray(0),
18 : next(_next),
19 : index(_index),
20 18916: value(_value) {
0: branch 0 not taken
9458: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
21 9458: assert(_value.getWidth() == Expr::Int8 && "Update value should be 8-bit wide.");
22 9458: computeHash();
9415: branch 0 taken
43: branch 1 taken
43: branch 2 taken
43: branch 3 taken
23 9458: if (next) {
24 9415: ++next->refCount;
25 9415: size = 1 + next->size;
26 : }
27 43: else size = 1;
28 9458: }
29 :
30 : extern "C" void vc_DeleteExpr(void*);
31 :
32 9458: UpdateNode::~UpdateNode() {
33 : // XXX gross
695: branch 0 taken
8763: branch 1 taken
8763: branch 2 taken
8763: branch 3 taken
34 9458: if (stpArray)
35 695: ::vc_DeleteExpr(stpArray);
36 9458: }
37 :
38 288: int UpdateNode::compare(const UpdateNode &b) const {
0: branch 1 not taken
288: branch 2 taken
39 288: if (int i = index.compare(b.index))
40 0: return i;
41 288: return value.compare(b.value);
42 : }
43 :
44 9458: unsigned UpdateNode::computeHash() {
45 28374: hashValue = index.hash() ^ value.hash();
9415: branch 0 taken
43: branch 1 taken
46 9458: if (next)
47 18830: hashValue ^= next->hash();
48 9458: return hashValue;
49 : }
50 :
51 : ///
52 :
53 768379: UpdateList::UpdateList(const MemoryObject *_root, bool _isRooted, const UpdateNode *_head)
54 : : root(_root),
55 : head(_head),
56 768379: isRooted(_isRooted) {
768379: branch 0 taken
768379: branch 1 taken
0: branch 2 not taken
768379: branch 3 taken
57 768379: if (head) ++head->refCount;
58 768379: }
59 :
60 43090: UpdateList::UpdateList(const UpdateList &b)
61 : : root(b.root),
62 : head(b.head),
63 43090: isRooted(b.isRooted) {
43090: branch 0 taken
43090: branch 1 taken
537: branch 2 taken
42553: branch 3 taken
64 43090: if (head) ++head->refCount;
65 43090: }
66 :
67 811469: UpdateList::~UpdateList() {
68 : // We need to be careful and avoid recursion here. We do this in
69 : // cooperation with the private dtor of UpdateNode which does not
70 : // recursively free its tail.
9998: branch 0 taken
810929: branch 1 taken
9458: branch 2 taken
540: branch 3 taken
9458: branch 4 taken
811469: branch 5 taken
811469: branch 6 taken
811469: branch 7 taken
811469: branch 8 taken
811469: branch 9 taken
811469: branch 10 taken
811469: branch 11 taken
71 1632396: while (head && --head->refCount==0) {
72 9458: const UpdateNode *n = head->next;
9458: branch 0 taken
0: branch 1 not taken
9458: branch 4 taken
9458: branch 5 taken
73 9458: delete head;
74 9458: head = n;
75 : }
76 811469: }
77 :
78 13: UpdateList &UpdateList::operator=(const UpdateList &b) {
3: branch 0 taken
10: branch 1 taken
79 13: if (b.head) ++b.head->refCount;
0: branch 0 not taken
13: branch 1 taken
13: branch 2 taken
13: branch 3 taken
0: branch 4 not taken
13: branch 5 taken
13: branch 6 taken
13: branch 7 taken
80 13: if (head && --head->refCount==0) delete head;
81 13: root = b.root;
82 13: head = b.head;
83 13: isRooted = b.isRooted;
84 13: return *this;
85 : }
86 :
87 9458: void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
9415: branch 0 taken
43: branch 1 taken
88 9458: if (head) --head->refCount;
89 9458: head = new UpdateNode(head, index, value);
90 9458: ++head->refCount;
91 9458: }
92 :
93 1194003: int UpdateList::compare(const UpdateList &b) const {
94 : // use object id to increase determinism
1410: branch 0 taken
1192593: branch 1 taken
95 1194003: if (root->id != b.root->id)
530: branch 0 taken
880: branch 1 taken
96 1410: return root->id<b.root->id ? -1 : 1;
97 :
0: branch 0 not taken
1192593: branch 1 taken
98 1192593: if (getSize() < b.getSize()) return -1;
0: branch 0 not taken
1192593: branch 1 taken
99 1192593: else if (getSize() > b.getSize()) return 1;
100 :
101 : // XXX build comparison into update, make fast
102 1192593: const UpdateNode *an=head, *bn=b.head;
14308: branch 0 taken
1178573: branch 1 taken
103 1192881: for (; an && bn; an=an->next,bn=bn->next) {
14020: branch 0 taken
288: branch 1 taken
104 14308: if (an==bn) { // exploit shared list structure
105 14020: return 0;
106 : } else {
0: branch 1 not taken
288: branch 2 taken
107 288: if (int res = an->compare(*bn))
108 0: return res;
109 : }
110 : }
0: branch 0 not taken
1178573: branch 1 taken
111 1178573: assert(!an && !bn);
112 1178573: return 0;
113 : }
114 :
115 5512: unsigned UpdateList::hash() const {
116 5512: unsigned res = root->id * Expr::MAGIC_HASH_CONSTANT;
307: branch 0 taken
5205: branch 1 taken
117 5512: if (head)
118 614: res ^= head->hash();
119 5512: return res;
120 : }
Generated: 2009-05-17 22:47 by zcov