 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
24.1% |
14 / 58 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
24.1% |
14 / 58 |
| |
|
Line Coverage: |
28.1% |
18 / 64 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/IncompleteSolver.h"
4 :
5 : #include "klee/Constraints.h"
6 : // FIXME: This shouldn't be here.
7 : #include "klee/Memory.h"
8 :
9 : using namespace klee;
10 : using namespace llvm;
11 :
12 : /***/
13 :
14 : IncompleteSolver::PartialValidity
15 1487: IncompleteSolver::negatePartialValidity(PartialValidity pv) {
786: branch 0 taken
142: branch 1 taken
83: branch 2 taken
281: branch 3 taken
195: branch 4 taken
0: branch 5 not taken
16 1487: switch(pv) {
17 786: case MustBeTrue: return MustBeFalse;
18 142: case MustBeFalse: return MustBeTrue;
19 83: case MayBeTrue: return MayBeFalse;
20 281: case MayBeFalse: return MayBeTrue;
21 195: case TrueOrFalse: return TrueOrFalse;
22 0: default: assert(0 && "invalid partial validity");
23 : }
24 : }
25 :
26 : IncompleteSolver::PartialValidity
27 0: IncompleteSolver::computeValidity(const Query& query) {
28 0: PartialValidity trueResult = computeTruth(query);
29 :
0: branch 0 not taken
0: branch 1 not taken
30 0: if (trueResult == MustBeTrue) {
31 0: return MustBeTrue;
32 : } else {
33 0: PartialValidity falseResult = computeTruth(query.negateExpr());
34 :
0: branch 0 not taken
0: branch 1 not taken
35 0: if (falseResult == MustBeTrue) {
36 0: return MustBeFalse;
37 : } else {
38 0: bool trueCorrect = trueResult != None,
39 0: falseCorrect = falseResult != None;
40 :
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
41 0: if (trueCorrect && falseCorrect) {
42 0: return TrueOrFalse;
0: branch 0 not taken
0: branch 1 not taken
43 0: } else if (trueCorrect) { // ==> trueResult == MayBeFalse
44 0: return MayBeFalse;
0: branch 0 not taken
0: branch 1 not taken
45 0: } else if (falseCorrect) { // ==> falseResult == MayBeFalse
46 0: return MayBeTrue;
47 : } else {
48 0: return None;
49 : }
50 : }
51 : }
52 : }
53 :
54 : /***/
55 :
56 : StagedSolverImpl::StagedSolverImpl(IncompleteSolver *_primary,
57 1: Solver *_secondary)
58 : : primary(_primary),
59 2: secondary(_secondary) {
60 1: }
61 :
62 1: StagedSolverImpl::~StagedSolverImpl() {
1: branch 0 taken
0: branch 1 not taken
1: branch 3 taken
1: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
63 1: delete primary;
1: branch 0 taken
0: branch 1 not taken
1: branch 4 taken
1: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
64 1: delete secondary;
1: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
65 1: }
66 :
67 0: bool StagedSolverImpl::computeTruth(const Query& query, bool &isValid) {
68 0: IncompleteSolver::PartialValidity trueResult = primary->computeTruth(query);
69 :
0: branch 0 not taken
0: branch 1 not taken
70 0: if (trueResult != IncompleteSolver::None) {
71 0: isValid = (trueResult == IncompleteSolver::MustBeTrue);
72 0: return true;
73 : }
74 :
75 0: return secondary->impl->computeTruth(query, isValid);
76 : }
77 :
78 : bool StagedSolverImpl::computeValidity(const Query& query,
79 0: Solver::Validity &result) {
80 : bool tmp;
81 :
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
82 0: switch(primary->computeValidity(query)) {
83 : case IncompleteSolver::MustBeTrue:
84 0: result = Solver::True;
85 0: break;
86 : case IncompleteSolver::MustBeFalse:
87 0: result = Solver::False;
88 0: break;
89 : case IncompleteSolver::TrueOrFalse:
90 0: result = Solver::Unknown;
91 0: break;
92 : case IncompleteSolver::MayBeTrue:
0: branch 1 not taken
0: branch 2 not taken
93 0: if (!secondary->impl->computeTruth(query, tmp))
94 0: return false;
0: branch 0 not taken
0: branch 1 not taken
95 0: result = tmp ? Solver::True : Solver::Unknown;
96 0: break;
97 : case IncompleteSolver::MayBeFalse:
0: branch 2 not taken
0: branch 3 not taken
98 0: if (!secondary->impl->computeTruth(query.negateExpr(), tmp))
99 0: return false;
0: branch 0 not taken
0: branch 1 not taken
100 0: result = tmp ? Solver::False : Solver::Unknown;
101 0: break;
102 : default:
0: branch 1 not taken
0: branch 2 not taken
103 0: if (!secondary->impl->computeValidity(query, result))
104 0: return false;
105 : break;
106 : }
107 :
108 0: return true;
109 : }
110 :
111 : bool StagedSolverImpl::computeValue(const Query& query,
112 0: ref<Expr> &result) {
0: branch 1 not taken
0: branch 2 not taken
113 0: if (primary->computeValue(query, result))
114 0: return true;
115 :
116 0: return secondary->impl->computeValue(query, result);
117 : }
118 :
119 : bool
120 : StagedSolverImpl::computeInitialValues(const Query& query,
121 : const std::vector<const MemoryObject*>
122 : &objects,
123 : std::vector< std::vector<unsigned char> >
124 : &values,
125 371: bool &hasSolution) {
177: branch 1 taken
194: branch 2 taken
126 371: if (primary->computeInitialValues(query, objects, values, hasSolution))
127 177: return true;
128 :
129 : return secondary->impl->computeInitialValues(query, objects, values,
130 194: hasSolution);
131 : }
Generated: 2009-05-17 22:47 by zcov