GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/context/context_white.cpp Lines: 117 117 100.0 %
Date: 2021-03-23 Branches: 318 1444 22.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file context_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief White box testing of CVC4::context::Context.
13
 **
14
 ** White box testing of CVC4::context::Context.
15
 **/
16
17
#include "base/check.h"
18
#include "context/cdo.h"
19
#include "test_context.h"
20
21
namespace CVC4 {
22
23
using namespace context;
24
25
namespace test {
26
27
4
class TestContextWhite : public TestContext
28
{
29
};
30
31
10
TEST_F(TestContextWhite, simple)
32
{
33
2
  Scope* s = d_context->getTopScope();
34
35
2
  ASSERT_EQ(s, d_context->getBottomScope());
36
2
  ASSERT_EQ(d_context->getLevel(), 0);
37
2
  ASSERT_EQ(d_context->d_scopeList.size(), 1);
38
39
2
  ASSERT_EQ(s->d_pContext, d_context.get());
40
2
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
41
2
  ASSERT_EQ(s->d_level, 0);
42
2
  ASSERT_EQ(s->d_pContextObjList, nullptr);
43
44
4
  CDO<int> a(d_context.get());
45
46
2
  ASSERT_EQ(s->d_pContext, d_context.get());
47
2
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
48
2
  ASSERT_EQ(s->d_level, 0);
49
2
  ASSERT_EQ(s->d_pContextObjList, &a);
50
51
2
  ASSERT_EQ(a.d_pScope, s);
52
2
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
53
2
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
54
2
  ASSERT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList);
55
56
4
  CDO<int> b(d_context.get());
57
58
2
  ASSERT_EQ(s->d_pContext, d_context.get());
59
2
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
60
2
  ASSERT_EQ(s->d_level, 0);
61
2
  ASSERT_EQ(s->d_pContextObjList, &b);
62
63
2
  ASSERT_EQ(a.d_pScope, s);
64
2
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
65
2
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
66
2
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
67
68
2
  ASSERT_EQ(b.d_pScope, s);
69
2
  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
70
2
  ASSERT_EQ(b.d_pContextObjNext, &a);
71
2
  ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
72
73
2
  d_context->push();
74
2
  Scope* t = d_context->getTopScope();
75
2
  ASSERT_NE(s, t);
76
77
2
  ASSERT_EQ(s, d_context->getBottomScope());
78
2
  ASSERT_EQ(d_context->getLevel(), 1);
79
2
  ASSERT_EQ(d_context->d_scopeList.size(), 2);
80
81
2
  ASSERT_EQ(s->d_pContext, d_context.get());
82
2
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
83
2
  ASSERT_EQ(s->d_level, 0);
84
2
  ASSERT_EQ(s->d_pContextObjList, &b);
85
86
2
  ASSERT_EQ(t->d_pContext, d_context.get());
87
2
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
88
2
  ASSERT_EQ(t->d_level, 1);
89
2
  ASSERT_EQ(t->d_pContextObjList, nullptr);
90
91
2
  ASSERT_EQ(a.d_pScope, s);
92
2
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
93
2
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
94
2
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
95
96
2
  ASSERT_EQ(b.d_pScope, s);
97
2
  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
98
2
  ASSERT_EQ(b.d_pContextObjNext, &a);
99
2
  ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
100
101
2
  a = 5;
102
103
2
  ASSERT_EQ(t->d_pContext, d_context.get());
104
2
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
105
2
  ASSERT_EQ(t->d_level, 1);
106
2
  ASSERT_EQ(t->d_pContextObjList, &a);
107
108
2
  ASSERT_EQ(a.d_pScope, t);
109
2
  ASSERT_NE(a.d_pContextObjRestore, nullptr);
110
2
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
111
2
  ASSERT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList);
112
113
2
  b = 3;
114
115
2
  ASSERT_EQ(t->d_pContext, d_context.get());
116
2
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
117
2
  ASSERT_EQ(t->d_level, 1);
118
2
  ASSERT_EQ(t->d_pContextObjList, &b);
119
120
2
  ASSERT_EQ(a.d_pScope, t);
121
2
  ASSERT_NE(a.d_pContextObjRestore, nullptr);
122
2
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
123
2
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
124
125
2
  ASSERT_EQ(b.d_pScope, t);
126
2
  ASSERT_NE(b.d_pContextObjRestore, nullptr);
127
2
  ASSERT_EQ(b.d_pContextObjNext, &a);
128
2
  ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
129
130
2
  d_context->push();
131
2
  Scope* u = d_context->getTopScope();
132
2
  ASSERT_NE(u, t);
133
2
  ASSERT_NE(u, s);
134
135
4
  CDO<int> c(d_context.get());
136
2
  c = 4;
137
138
2
  ASSERT_EQ(c.d_pScope, u);
139
2
  ASSERT_NE(c.d_pContextObjRestore, nullptr);
140
2
  ASSERT_EQ(c.d_pContextObjNext, nullptr);
141
2
  ASSERT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList);
142
143
2
  d_context->pop();
144
145
2
  ASSERT_EQ(t->d_pContext, d_context.get());
146
2
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
147
2
  ASSERT_EQ(t->d_level, 1);
148
2
  ASSERT_EQ(t->d_pContextObjList, &b);
149
150
2
  ASSERT_EQ(a.d_pScope, t);
151
2
  ASSERT_NE(a.d_pContextObjRestore, nullptr);
152
2
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
153
2
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
154
155
2
  ASSERT_EQ(b.d_pScope, t);
156
2
  ASSERT_NE(b.d_pContextObjRestore, nullptr);
157
2
  ASSERT_EQ(b.d_pContextObjNext, &a);
158
2
  ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
159
160
2
  d_context->pop();
161
162
2
  ASSERT_EQ(s->d_pContext, d_context.get());
163
2
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
164
2
  ASSERT_EQ(s->d_level, 0);
165
2
  ASSERT_EQ(s->d_pContextObjList, &c);
166
167
2
  ASSERT_EQ(a.d_pScope, s);
168
2
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
169
2
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
170
2
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
171
172
2
  ASSERT_EQ(b.d_pScope, s);
173
2
  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
174
2
  ASSERT_EQ(b.d_pContextObjNext, &a);
175
2
  ASSERT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext);
176
177
2
  ASSERT_EQ(c.d_pScope, s);
178
2
  ASSERT_EQ(c.d_pContextObjRestore, nullptr);
179
2
  ASSERT_EQ(c.d_pContextObjNext, &b);
180
2
  ASSERT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList);
181
}
182
}  // namespace test
183
6
}  // namespace CVC4