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