 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
75.2% |
714 / 950 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
90.1% |
856 / 950 |
| |
|
Line Coverage: |
100.0% |
49 / 49 |
| |
 |
|
 |
1 : //===- ExprTest.cpp - Expression unit tests -------------------------------===//
2 :
3 : #include "gtest/gtest.h"
4 :
5 : #include "klee/Constraints.h"
6 : #include "klee/Expr.h"
7 : // FIXME: This should not be here.
8 : #include "klee/Memory.h"
9 : #include "klee/Solver.h"
10 :
11 : using namespace klee;
12 :
13 : namespace {
14 :
15 : const int g_constants[] = { -1, 1, 4, 17, 0 };
16 : const Expr::Width g_types[] = { Expr::Bool,
17 : Expr::Int8,
18 : Expr::Int16,
19 : Expr::Int32,
20 : Expr::Int64 };
21 :
22 1017: ref<Expr> getConstant(int value, Expr::Width width) {
23 1017: int64_t ext = value;
24 1017: uint64_t trunc = ext & (((uint64_t) -1LL) >> (64 - width));
25 1017: return ConstantExpr::create(trunc, width);
26 : }
27 :
28 :
29 : template<class T>
30 : void testOperation(Solver &solver,
31 : int value,
32 : Expr::Width operandWidth,
33 571: Expr::Width resultWidth) {
34 : std::vector<Expr::CreateArg> symbolicArgs;
35 :
35: branch 0 taken
5: branch 1 taken
45: branch 2 taken
45: branch 3 taken
45: branch 4 taken
45: branch 5 taken
50: branch 6 taken
25: branch 7 taken
50: branch 8 taken
25: branch 9 taken
10: branch 10 taken
5: branch 11 taken
8: branch 12 taken
4: branch 13 taken
8: branch 14 taken
4: branch 15 taken
8: branch 16 taken
4: branch 17 taken
8: branch 18 taken
4: branch 19 taken
40: branch 20 taken
20: branch 21 taken
40: branch 22 taken
20: branch 23 taken
40: branch 24 taken
20: branch 25 taken
50: branch 26 taken
25: branch 27 taken
50: branch 28 taken
25: branch 29 taken
50: branch 30 taken
25: branch 31 taken
50: branch 32 taken
25: branch 33 taken
50: branch 34 taken
25: branch 35 taken
50: branch 36 taken
25: branch 37 taken
50: branch 38 taken
25: branch 39 taken
50: branch 40 taken
25: branch 41 taken
50: branch 42 taken
25: branch 43 taken
50: branch 44 taken
25: branch 45 taken
50: branch 46 taken
25: branch 47 taken
50: branch 48 taken
25: branch 49 taken
50: branch 50 taken
25: branch 51 taken
36 1588: for (unsigned i = 0; i < T::numKids; i++) {
15: branch 0 taken
20: branch 1 taken
45: branch 2 taken
0: branch 3 not taken
45: branch 4 taken
0: branch 5 not taken
50: branch 6 taken
0: branch 7 not taken
50: branch 8 taken
0: branch 9 not taken
10: branch 10 taken
0: branch 11 not taken
8: branch 12 taken
0: branch 13 not taken
8: branch 14 taken
0: branch 15 not taken
8: branch 16 taken
0: branch 17 not taken
8: branch 18 taken
0: branch 19 not taken
40: branch 20 taken
0: branch 21 not taken
40: branch 22 taken
0: branch 23 not taken
40: branch 24 taken
0: branch 25 not taken
50: branch 26 taken
0: branch 27 not taken
50: branch 28 taken
0: branch 29 not taken
50: branch 30 taken
0: branch 31 not taken
50: branch 32 taken
0: branch 33 not taken
50: branch 34 taken
0: branch 35 not taken
50: branch 36 taken
0: branch 37 not taken
50: branch 38 taken
0: branch 39 not taken
50: branch 40 taken
0: branch 41 not taken
50: branch 42 taken
0: branch 43 not taken
50: branch 44 taken
0: branch 45 not taken
50: branch 46 taken
0: branch 47 not taken
50: branch 48 taken
0: branch 49 not taken
50: branch 50 taken
0: branch 51 not taken
37 1037: if (!T::isValidKidWidth(i, operandWidth))
38 20: return;
39 :
40 1017: unsigned size = Expr::getMinBytesForWidth(operandWidth);
41 1017: MemoryObject *mo = new MemoryObject(0, size, false, false, false, 0);
42 3051: symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(mo,
43 : operandWidth)));
44 : }
45 :
0: branch 0 not taken
5: branch 1 taken
45: branch 2 taken
0: branch 3 not taken
45: branch 4 taken
0: branch 5 not taken
0: branch 6 not taken
25: branch 7 taken
0: branch 8 not taken
25: branch 9 taken
0: branch 10 not taken
5: branch 11 taken
0: branch 12 not taken
4: branch 13 taken
0: branch 14 not taken
4: branch 15 taken
0: branch 16 not taken
4: branch 17 taken
0: branch 18 not taken
4: branch 19 taken
0: branch 20 not taken
20: branch 21 taken
0: branch 22 not taken
20: branch 23 taken
0: branch 24 not taken
20: branch 25 taken
0: branch 26 not taken
25: branch 27 taken
0: branch 28 not taken
25: branch 29 taken
0: branch 30 not taken
25: branch 31 taken
0: branch 32 not taken
25: branch 33 taken
0: branch 34 not taken
25: branch 35 taken
0: branch 36 not taken
25: branch 37 taken
0: branch 38 not taken
25: branch 39 taken
0: branch 40 not taken
25: branch 41 taken
0: branch 42 not taken
25: branch 43 taken
0: branch 44 not taken
25: branch 45 taken
0: branch 46 not taken
25: branch 47 taken
0: branch 48 not taken
25: branch 49 taken
0: branch 50 not taken
25: branch 51 taken
46 551: if (T::needsResultType())
47 90: symbolicArgs.push_back(Expr::CreateArg(resultWidth));
48 :
49 551: ref<Expr> fullySymbolicExpr = Expr::createFromKind(T::kind, symbolicArgs);
50 :
51 : // For each kid, replace the kid with a constant value and verify
52 : // that the fully symbolic expression is equivalent to it when the
53 : // replaced value is appropriated constrained.
15: branch 5 taken
5: branch 6 taken
45: branch 12 taken
45: branch 13 taken
45: branch 19 taken
45: branch 20 taken
50: branch 26 taken
25: branch 27 taken
50: branch 33 taken
25: branch 34 taken
10: branch 40 taken
5: branch 41 taken
8: branch 47 taken
4: branch 48 taken
8: branch 54 taken
4: branch 55 taken
8: branch 61 taken
4: branch 62 taken
8: branch 68 taken
4: branch 69 taken
40: branch 75 taken
20: branch 76 taken
40: branch 82 taken
20: branch 83 taken
40: branch 89 taken
20: branch 90 taken
50: branch 96 taken
25: branch 97 taken
50: branch 103 taken
25: branch 104 taken
50: branch 110 taken
25: branch 111 taken
50: branch 117 taken
25: branch 118 taken
50: branch 124 taken
25: branch 125 taken
50: branch 131 taken
25: branch 132 taken
50: branch 138 taken
25: branch 139 taken
50: branch 145 taken
25: branch 146 taken
50: branch 152 taken
25: branch 153 taken
50: branch 159 taken
25: branch 160 taken
50: branch 166 taken
25: branch 167 taken
50: branch 173 taken
25: branch 174 taken
50: branch 180 taken
25: branch 181 taken
54 1568: for (unsigned kid = 0; kid < T::numKids; kid++) {
55 1017: std::vector<Expr::CreateArg> partiallyConstantArgs(symbolicArgs);
45: branch 0 taken
15: branch 1 taken
45: branch 2 taken
45: branch 3 taken
45: branch 4 taken
45: branch 5 taken
100: branch 6 taken
50: branch 7 taken
100: branch 8 taken
50: branch 9 taken
20: branch 10 taken
10: branch 11 taken
16: branch 12 taken
8: branch 13 taken
16: branch 14 taken
8: branch 15 taken
16: branch 16 taken
8: branch 17 taken
16: branch 18 taken
8: branch 19 taken
80: branch 20 taken
40: branch 21 taken
80: branch 22 taken
40: branch 23 taken
80: branch 24 taken
40: branch 25 taken
100: branch 26 taken
50: branch 27 taken
100: branch 28 taken
50: branch 29 taken
100: branch 30 taken
50: branch 31 taken
100: branch 32 taken
50: branch 33 taken
100: branch 34 taken
50: branch 35 taken
100: branch 36 taken
50: branch 37 taken
100: branch 38 taken
50: branch 39 taken
100: branch 40 taken
50: branch 41 taken
100: branch 42 taken
50: branch 43 taken
100: branch 44 taken
50: branch 45 taken
100: branch 46 taken
50: branch 47 taken
100: branch 48 taken
50: branch 49 taken
100: branch 50 taken
50: branch 51 taken
56 2976: for (unsigned i = 0; i < T::numKids; i++)
15: branch 0 taken
30: branch 1 taken
45: branch 2 taken
0: branch 3 not taken
45: branch 4 taken
0: branch 5 not taken
50: branch 6 taken
50: branch 7 taken
50: branch 8 taken
50: branch 9 taken
10: branch 10 taken
10: branch 11 taken
8: branch 12 taken
8: branch 13 taken
8: branch 14 taken
8: branch 15 taken
8: branch 16 taken
8: branch 17 taken
8: branch 18 taken
8: branch 19 taken
40: branch 20 taken
40: branch 21 taken
40: branch 22 taken
40: branch 23 taken
40: branch 24 taken
40: branch 25 taken
50: branch 26 taken
50: branch 27 taken
50: branch 28 taken
50: branch 29 taken
50: branch 30 taken
50: branch 31 taken
50: branch 32 taken
50: branch 33 taken
50: branch 34 taken
50: branch 35 taken
50: branch 36 taken
50: branch 37 taken
50: branch 38 taken
50: branch 39 taken
50: branch 40 taken
50: branch 41 taken
50: branch 42 taken
50: branch 43 taken
50: branch 44 taken
50: branch 45 taken
50: branch 46 taken
50: branch 47 taken
50: branch 48 taken
50: branch 49 taken
50: branch 50 taken
50: branch 51 taken
57 1959: if (i==kid)
58 3051: partiallyConstantArgs[i] = getConstant(value, operandWidth);
59 :
60 : ref<Expr> expr =
61 : NotOptimizedExpr::create(EqExpr::create(partiallyConstantArgs[kid].expr,
62 2034: symbolicArgs[kid].expr));
63 :
64 : ref<Expr> partiallyConstantExpr =
65 1017: Expr::createFromKind(T::kind, partiallyConstantArgs);
66 :
67 : ref<Expr> queryExpr = EqExpr::create(fullySymbolicExpr,
68 1017: partiallyConstantExpr);
69 :
70 : ConstraintManager constraints;
71 1017: constraints.addConstraint(expr);
72 : bool res;
73 2034: bool success = solver.mustBeTrue(Query(constraints, queryExpr), res);
0: branch 1 not taken
15: branch 2 taken
0: branch 11 not taken
45: branch 12 taken
0: branch 21 not taken
45: branch 22 taken
0: branch 31 not taken
50: branch 32 taken
0: branch 41 not taken
50: branch 42 taken
0: branch 51 not taken
10: branch 52 taken
0: branch 61 not taken
8: branch 62 taken
0: branch 71 not taken
8: branch 72 taken
0: branch 81 not taken
8: branch 82 taken
0: branch 91 not taken
8: branch 92 taken
0: branch 101 not taken
40: branch 102 taken
0: branch 111 not taken
40: branch 112 taken
0: branch 121 not taken
40: branch 122 taken
0: branch 131 not taken
50: branch 132 taken
0: branch 141 not taken
50: branch 142 taken
0: branch 151 not taken
50: branch 152 taken
0: branch 161 not taken
50: branch 162 taken
0: branch 171 not taken
50: branch 172 taken
0: branch 181 not taken
50: branch 182 taken
0: branch 191 not taken
50: branch 192 taken
0: branch 201 not taken
50: branch 202 taken
0: branch 211 not taken
50: branch 212 taken
0: branch 221 not taken
50: branch 222 taken
0: branch 231 not taken
50: branch 232 taken
0: branch 241 not taken
50: branch 242 taken
0: branch 251 not taken
50: branch 252 taken
74 2034: EXPECT_EQ(true, success) << "Constraint solving failed";
75 :
15: branch 0 taken
0: branch 1 not taken
45: branch 2 taken
0: branch 3 not taken
45: branch 4 taken
0: branch 5 not taken
50: branch 6 taken
0: branch 7 not taken
50: branch 8 taken
0: branch 9 not taken
10: branch 10 taken
0: branch 11 not taken
8: branch 12 taken
0: branch 13 not taken
8: branch 14 taken
0: branch 15 not taken
8: branch 16 taken
0: branch 17 not taken
8: branch 18 taken
0: branch 19 not taken
40: branch 20 taken
0: branch 21 not taken
40: branch 22 taken
0: branch 23 not taken
40: branch 24 taken
0: branch 25 not taken
50: branch 26 taken
0: branch 27 not taken
50: branch 28 taken
0: branch 29 not taken
50: branch 30 taken
0: branch 31 not taken
50: branch 32 taken
0: branch 33 not taken
50: branch 34 taken
0: branch 35 not taken
50: branch 36 taken
0: branch 37 not taken
50: branch 38 taken
0: branch 39 not taken
50: branch 40 taken
0: branch 41 not taken
50: branch 42 taken
0: branch 43 not taken
50: branch 44 taken
0: branch 45 not taken
50: branch 46 taken
0: branch 47 not taken
50: branch 48 taken
0: branch 49 not taken
50: branch 50 taken
0: branch 51 not taken
76 1017: if (success) {
0: branch 1 not taken
15: branch 2 taken
0: branch 18 not taken
45: branch 19 taken
0: branch 35 not taken
45: branch 36 taken
0: branch 52 not taken
50: branch 53 taken
0: branch 69 not taken
50: branch 70 taken
0: branch 86 not taken
10: branch 87 taken
0: branch 103 not taken
8: branch 104 taken
0: branch 120 not taken
8: branch 121 taken
0: branch 137 not taken
8: branch 138 taken
0: branch 154 not taken
8: branch 155 taken
0: branch 171 not taken
40: branch 172 taken
0: branch 188 not taken
40: branch 189 taken
0: branch 205 not taken
40: branch 206 taken
0: branch 222 not taken
50: branch 223 taken
0: branch 239 not taken
50: branch 240 taken
0: branch 256 not taken
50: branch 257 taken
0: branch 273 not taken
50: branch 274 taken
0: branch 290 not taken
50: branch 291 taken
0: branch 307 not taken
50: branch 308 taken
0: branch 324 not taken
50: branch 325 taken
0: branch 341 not taken
50: branch 342 taken
0: branch 358 not taken
50: branch 359 taken
0: branch 375 not taken
50: branch 376 taken
0: branch 392 not taken
50: branch 393 taken
0: branch 409 not taken
50: branch 410 taken
0: branch 426 not taken
50: branch 427 taken
77 2585: EXPECT_EQ(true, res) << "Evaluation failed!\n"
78 : << "query " << queryExpr
79 : << " with " << expr;
80 : }
81 : }
82 : }
83 :
84 : template<class T>
85 : void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true,
86 : unsigned maxWidth = 64) {
5: branch 0 taken
1: branch 1 taken
5: branch 2 taken
1: branch 3 taken
5: branch 4 taken
1: branch 5 taken
5: branch 6 taken
1: branch 7 taken
5: branch 8 taken
1: branch 9 taken
5: branch 10 taken
1: branch 11 taken
5: branch 12 taken
1: branch 13 taken
5: branch 14 taken
1: branch 15 taken
5: branch 16 taken
1: branch 17 taken
5: branch 18 taken
1: branch 19 taken
5: branch 20 taken
1: branch 21 taken
5: branch 22 taken
1: branch 23 taken
5: branch 24 taken
1: branch 25 taken
5: branch 26 taken
1: branch 27 taken
5: branch 28 taken
1: branch 29 taken
5: branch 30 taken
1: branch 31 taken
5: branch 32 taken
1: branch 33 taken
5: branch 34 taken
1: branch 35 taken
5: branch 36 taken
1: branch 37 taken
5: branch 38 taken
1: branch 39 taken
5: branch 40 taken
1: branch 41 taken
5: branch 42 taken
1: branch 43 taken
5: branch 44 taken
1: branch 45 taken
5: branch 46 taken
1: branch 47 taken
5: branch 48 taken
1: branch 49 taken
5: branch 50 taken
1: branch 51 taken
87 131: for (unsigned j=0; j<sizeof(g_types)/sizeof(g_types[0]); j++) {
88 130: Expr::Width type = g_types[j];
89 :
5: branch 0 taken
0: branch 1 not taken
5: branch 2 taken
0: branch 3 not taken
5: branch 4 taken
0: branch 5 not taken
5: branch 6 taken
0: branch 7 not taken
5: branch 8 taken
0: branch 9 not taken
2: branch 10 taken
3: branch 11 taken
2: branch 12 taken
3: branch 13 taken
2: branch 14 taken
3: branch 15 taken
2: branch 16 taken
3: branch 17 taken
2: branch 18 taken
3: branch 19 taken
5: branch 20 taken
0: branch 21 not taken
5: branch 22 taken
0: branch 23 not taken
5: branch 24 taken
0: branch 25 not taken
5: branch 26 taken
0: branch 27 not taken
5: branch 28 taken
0: branch 29 not taken
5: branch 30 taken
0: branch 31 not taken
5: branch 32 taken
0: branch 33 not taken
5: branch 34 taken
0: branch 35 not taken
5: branch 36 taken
0: branch 37 not taken
5: branch 38 taken
0: branch 39 not taken
5: branch 40 taken
0: branch 41 not taken
5: branch 42 taken
0: branch 43 not taken
5: branch 44 taken
0: branch 45 not taken
5: branch 46 taken
0: branch 47 not taken
5: branch 48 taken
0: branch 49 not taken
5: branch 50 taken
0: branch 51 not taken
90 130: if (type > maxWidth) continue;
91 :
25: branch 0 taken
5: branch 1 taken
25: branch 2 taken
5: branch 3 taken
25: branch 4 taken
5: branch 5 taken
25: branch 6 taken
5: branch 7 taken
25: branch 8 taken
5: branch 9 taken
10: branch 10 taken
2: branch 11 taken
10: branch 12 taken
2: branch 13 taken
10: branch 14 taken
2: branch 15 taken
10: branch 16 taken
2: branch 17 taken
10: branch 18 taken
2: branch 19 taken
25: branch 20 taken
5: branch 21 taken
25: branch 22 taken
5: branch 23 taken
25: branch 24 taken
5: branch 25 taken
25: branch 26 taken
5: branch 27 taken
25: branch 28 taken
5: branch 29 taken
25: branch 30 taken
5: branch 31 taken
25: branch 32 taken
5: branch 33 taken
25: branch 34 taken
5: branch 35 taken
25: branch 36 taken
5: branch 37 taken
25: branch 38 taken
5: branch 39 taken
25: branch 40 taken
5: branch 41 taken
25: branch 42 taken
5: branch 43 taken
25: branch 44 taken
5: branch 45 taken
25: branch 46 taken
5: branch 47 taken
25: branch 48 taken
5: branch 49 taken
25: branch 50 taken
5: branch 51 taken
92 690: for (unsigned i=0; i<sizeof(g_constants)/sizeof(g_constants[0]); i++) {
93 575: int value = g_constants[i];
0: branch 0 not taken
25: branch 1 taken
25: branch 2 taken
25: branch 3 taken
0: branch 4 not taken
25: branch 5 taken
25: branch 6 taken
25: branch 7 taken
0: branch 8 not taken
25: branch 9 taken
25: branch 10 taken
25: branch 11 taken
0: branch 12 not taken
25: branch 13 taken
25: branch 14 taken
25: branch 15 taken
0: branch 16 not taken
25: branch 17 taken
25: branch 18 taken
25: branch 19 taken
0: branch 20 not taken
10: branch 21 taken
10: branch 22 taken
10: branch 23 taken
10: branch 24 taken
0: branch 25 not taken
8: branch 26 taken
2: branch 27 taken
10: branch 28 taken
0: branch 29 not taken
8: branch 30 taken
2: branch 31 taken
10: branch 32 taken
0: branch 33 not taken
8: branch 34 taken
2: branch 35 taken
10: branch 36 taken
0: branch 37 not taken
8: branch 38 taken
2: branch 39 taken
0: branch 40 not taken
25: branch 41 taken
25: branch 42 taken
25: branch 43 taken
0: branch 44 not taken
25: branch 45 taken
25: branch 46 taken
25: branch 47 taken
0: branch 48 not taken
25: branch 49 taken
25: branch 50 taken
25: branch 51 taken
0: branch 52 not taken
25: branch 53 taken
25: branch 54 taken
25: branch 55 taken
0: branch 56 not taken
25: branch 57 taken
25: branch 58 taken
25: branch 59 taken
0: branch 60 not taken
25: branch 61 taken
25: branch 62 taken
25: branch 63 taken
0: branch 64 not taken
25: branch 65 taken
25: branch 66 taken
25: branch 67 taken
0: branch 68 not taken
25: branch 69 taken
25: branch 70 taken
25: branch 71 taken
0: branch 72 not taken
25: branch 73 taken
25: branch 74 taken
25: branch 75 taken
0: branch 76 not taken
25: branch 77 taken
25: branch 78 taken
25: branch 79 taken
0: branch 80 not taken
25: branch 81 taken
25: branch 82 taken
25: branch 83 taken
0: branch 84 not taken
25: branch 85 taken
25: branch 86 taken
25: branch 87 taken
0: branch 88 not taken
25: branch 89 taken
25: branch 90 taken
25: branch 91 taken
0: branch 92 not taken
25: branch 93 taken
25: branch 94 taken
25: branch 95 taken
0: branch 96 not taken
25: branch 97 taken
25: branch 98 taken
25: branch 99 taken
0: branch 100 not taken
25: branch 101 taken
25: branch 102 taken
25: branch 103 taken
94 575: if (!tryZero && !value) continue;
5: branch 0 taken
20: branch 1 taken
5: branch 2 taken
0: branch 3 not taken
5: branch 4 taken
20: branch 5 taken
5: branch 6 taken
0: branch 7 not taken
5: branch 8 taken
20: branch 9 taken
5: branch 10 taken
0: branch 11 not taken
5: branch 12 taken
20: branch 13 taken
5: branch 14 taken
0: branch 15 not taken
5: branch 16 taken
20: branch 17 taken
5: branch 18 taken
0: branch 19 not taken
5: branch 20 taken
5: branch 21 taken
0: branch 22 not taken
5: branch 23 taken
4: branch 24 taken
4: branch 25 taken
0: branch 26 not taken
4: branch 27 taken
4: branch 28 taken
4: branch 29 taken
0: branch 30 not taken
4: branch 31 taken
4: branch 32 taken
4: branch 33 taken
0: branch 34 not taken
4: branch 35 taken
4: branch 36 taken
4: branch 37 taken
0: branch 38 not taken
4: branch 39 taken
5: branch 40 taken
20: branch 41 taken
0: branch 42 not taken
5: branch 43 taken
5: branch 44 taken
20: branch 45 taken
0: branch 46 not taken
5: branch 47 taken
5: branch 48 taken
20: branch 49 taken
0: branch 50 not taken
5: branch 51 taken
5: branch 52 taken
20: branch 53 taken
5: branch 54 taken
0: branch 55 not taken
5: branch 56 taken
20: branch 57 taken
5: branch 58 taken
0: branch 59 not taken
5: branch 60 taken
20: branch 61 taken
5: branch 62 taken
0: branch 63 not taken
5: branch 64 taken
20: branch 65 taken
5: branch 66 taken
0: branch 67 not taken
5: branch 68 taken
20: branch 69 taken
5: branch 70 taken
0: branch 71 not taken
5: branch 72 taken
20: branch 73 taken
5: branch 74 taken
0: branch 75 not taken
5: branch 76 taken
20: branch 77 taken
5: branch 78 taken
0: branch 79 not taken
5: branch 80 taken
20: branch 81 taken
5: branch 82 taken
0: branch 83 not taken
5: branch 84 taken
20: branch 85 taken
5: branch 86 taken
0: branch 87 not taken
5: branch 88 taken
20: branch 89 taken
5: branch 90 taken
0: branch 91 not taken
5: branch 92 taken
20: branch 93 taken
5: branch 94 taken
0: branch 95 not taken
5: branch 96 taken
20: branch 97 taken
5: branch 98 taken
0: branch 99 not taken
5: branch 100 taken
20: branch 101 taken
5: branch 102 taken
0: branch 103 not taken
95 567: if (type == Expr::Bool && !tryBool) continue;
96 :
25: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
25: branch 3 taken
0: branch 4 not taken
25: branch 5 taken
25: branch 6 taken
0: branch 7 not taken
25: branch 8 taken
0: branch 9 not taken
5: branch 10 taken
0: branch 11 not taken
4: branch 12 taken
0: branch 13 not taken
4: branch 14 taken
0: branch 15 not taken
4: branch 16 taken
0: branch 17 not taken
4: branch 18 taken
0: branch 19 not taken
20: branch 20 taken
0: branch 21 not taken
20: branch 22 taken
0: branch 23 not taken
20: branch 24 taken
0: branch 25 not taken
25: branch 26 taken
0: branch 27 not taken
25: branch 28 taken
0: branch 29 not taken
25: branch 30 taken
0: branch 31 not taken
25: branch 32 taken
0: branch 33 not taken
25: branch 34 taken
0: branch 35 not taken
25: branch 36 taken
0: branch 37 not taken
25: branch 38 taken
0: branch 39 not taken
25: branch 40 taken
0: branch 41 not taken
25: branch 42 taken
0: branch 43 not taken
25: branch 44 taken
0: branch 45 not taken
25: branch 46 taken
0: branch 47 not taken
25: branch 48 taken
0: branch 49 not taken
25: branch 50 taken
0: branch 51 not taken
97 531: if (!T::needsResultType()) {
98 481: testOperation<T>(solver, value, type, type);
99 : continue;
100 : }
101 :
300: branch 0 taken
300: branch 1 taken
125: branch 2 taken
25: branch 3 taken
125: branch 4 taken
25: branch 5 taken
25: branch 6 taken
25: branch 7 taken
25: branch 8 taken
25: branch 9 taken
25: branch 10 taken
25: branch 11 taken
25: branch 12 taken
25: branch 13 taken
25: branch 14 taken
25: branch 15 taken
25: branch 16 taken
25: branch 17 taken
25: branch 18 taken
25: branch 19 taken
25: branch 20 taken
25: branch 21 taken
25: branch 22 taken
25: branch 23 taken
25: branch 24 taken
25: branch 25 taken
25: branch 26 taken
25: branch 27 taken
25: branch 28 taken
25: branch 29 taken
25: branch 30 taken
25: branch 31 taken
25: branch 32 taken
25: branch 33 taken
25: branch 34 taken
25: branch 35 taken
25: branch 36 taken
25: branch 37 taken
25: branch 38 taken
25: branch 39 taken
25: branch 40 taken
25: branch 41 taken
25: branch 42 taken
25: branch 43 taken
25: branch 44 taken
25: branch 45 taken
25: branch 46 taken
25: branch 47 taken
25: branch 48 taken
25: branch 49 taken
25: branch 50 taken
25: branch 51 taken
102 300: for (unsigned k=0; k<sizeof(g_types)/sizeof(g_types[0]); k++) {
103 250: Expr::Width resultType = g_types[k];
104 :
105 : // nasty hack to give only Trunc/ZExt/SExt the right types
45: branch 0 taken
80: branch 1 taken
45: branch 2 taken
80: branch 3 taken
106 250: if (T::kind == Expr::SExt || T::kind == Expr::ZExt) {
107 : if (Expr::getMinBytesForWidth(type) >=
108 : Expr::getMinBytesForWidth(resultType))
109 : continue;
110 : }
111 :
112 90: testOperation<T>(solver, value, type, resultType);
113 : }
114 : }
115 : }
116 : }
117 :
1: branch 5 taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
118 5: TEST(SolverTest, Evaluation) {
119 1: STPSolver *stpSolver = new STPSolver(true);
120 1: Solver *solver = stpSolver;
121 :
122 1: solver = createCexCachingSolver(solver);
123 1: solver = createCachingSolver(solver);
124 1: solver = createIndependentSolver(solver);
125 :
126 : testOpcode<SelectExpr>(*solver);
127 : testOpcode<ZExtExpr>(*solver);
128 : testOpcode<SExtExpr>(*solver);
129 :
130 : testOpcode<AddExpr>(*solver);
131 : testOpcode<SubExpr>(*solver);
132 : testOpcode<MulExpr>(*solver, false, true, 8);
133 : testOpcode<SDivExpr>(*solver, false, false, 8);
134 : testOpcode<UDivExpr>(*solver, false, false, 8);
135 : testOpcode<SRemExpr>(*solver, false, false, 8);
136 : testOpcode<URemExpr>(*solver, false, false, 8);
137 : testOpcode<ShlExpr>(*solver, false);
138 : testOpcode<LShrExpr>(*solver, false);
139 : testOpcode<AShrExpr>(*solver, false);
140 : testOpcode<AndExpr>(*solver);
141 : testOpcode<OrExpr>(*solver);
142 : testOpcode<XorExpr>(*solver);
143 :
144 : testOpcode<EqExpr>(*solver);
145 : testOpcode<NeExpr>(*solver);
146 : testOpcode<UltExpr>(*solver);
147 : testOpcode<UleExpr>(*solver);
148 : testOpcode<UgtExpr>(*solver);
149 : testOpcode<UgeExpr>(*solver);
150 : testOpcode<SltExpr>(*solver);
151 : testOpcode<SleExpr>(*solver);
152 : testOpcode<SgtExpr>(*solver);
153 : testOpcode<SgeExpr>(*solver);
154 :
1: branch 0 taken
0: branch 1 not taken
155 1: delete solver;
156 1: }
157 :
1: branch 0 taken
0: branch 1 not taken
1: branch 2 taken
0: branch 3 not taken
158 2: }
Generated: 2009-05-17 22:47 by zcov