Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/context/context_white.cpp	Lines:	117	117	100.0 %
Date:	2021-05-22	Branches:	318	1444	22.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * White box testing of cvc5::context::Context.
 */

#include "base/check.h"
#include "context/cdo.h"
#include "test_context.h"

namespace cvc5 {

using namespace context;

namespace test {

class TestContextWhite : public TestContext
{
};

TEST_F(TestContextWhite, simple)
{
  Scope* s = d_context->getTopScope();

  ASSERT_EQ(s, d_context->getBottomScope());
  ASSERT_EQ(d_context->getLevel(), 0);
  ASSERT_EQ(d_context->d_scopeList.size(), 1);

  ASSERT_EQ(s->d_pContext, d_context.get());
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(s->d_level, 0);
  ASSERT_EQ(s->d_pContextObjList, nullptr);

  CDO<int> a(d_context.get());

  ASSERT_EQ(s->d_pContext, d_context.get());
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(s->d_level, 0);
  ASSERT_EQ(s->d_pContextObjList, &a);

  ASSERT_EQ(a.d_pScope, s);
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
  ASSERT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList);

  CDO<int> b(d_context.get());

  ASSERT_EQ(s->d_pContext, d_context.get());
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(s->d_level, 0);
  ASSERT_EQ(s->d_pContextObjList, &b);

  ASSERT_EQ(a.d_pScope, s);
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);

  ASSERT_EQ(b.d_pScope, s);
  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
  ASSERT_EQ(b.d_pContextObjNext, &a);
  ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);

  d_context->push();
  Scope* t = d_context->getTopScope();
  ASSERT_NE(s, t);

  ASSERT_EQ(s, d_context->getBottomScope());
  ASSERT_EQ(d_context->getLevel(), 1);
  ASSERT_EQ(d_context->d_scopeList.size(), 2);

  ASSERT_EQ(s->d_pContext, d_context.get());
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(s->d_level, 0);
  ASSERT_EQ(s->d_pContextObjList, &b);

  ASSERT_EQ(t->d_pContext, d_context.get());
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(t->d_level, 1);
  ASSERT_EQ(t->d_pContextObjList, nullptr);

  ASSERT_EQ(a.d_pScope, s);
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);

  ASSERT_EQ(b.d_pScope, s);
  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
  ASSERT_EQ(b.d_pContextObjNext, &a);
  ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);

  a = 5;

  ASSERT_EQ(t->d_pContext, d_context.get());
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(t->d_level, 1);
  ASSERT_EQ(t->d_pContextObjList, &a);

  ASSERT_EQ(a.d_pScope, t);
  ASSERT_NE(a.d_pContextObjRestore, nullptr);
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
  ASSERT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList);

  b = 3;

  ASSERT_EQ(t->d_pContext, d_context.get());
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(t->d_level, 1);
  ASSERT_EQ(t->d_pContextObjList, &b);

  ASSERT_EQ(a.d_pScope, t);
  ASSERT_NE(a.d_pContextObjRestore, nullptr);
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);

  ASSERT_EQ(b.d_pScope, t);
  ASSERT_NE(b.d_pContextObjRestore, nullptr);
  ASSERT_EQ(b.d_pContextObjNext, &a);
  ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);

  d_context->push();
  Scope* u = d_context->getTopScope();
  ASSERT_NE(u, t);
  ASSERT_NE(u, s);

  CDO<int> c(d_context.get());
  c = 4;

  ASSERT_EQ(c.d_pScope, u);
  ASSERT_NE(c.d_pContextObjRestore, nullptr);
  ASSERT_EQ(c.d_pContextObjNext, nullptr);
  ASSERT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList);

  d_context->pop();

  ASSERT_EQ(t->d_pContext, d_context.get());
  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(t->d_level, 1);
  ASSERT_EQ(t->d_pContextObjList, &b);

  ASSERT_EQ(a.d_pScope, t);
  ASSERT_NE(a.d_pContextObjRestore, nullptr);
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);

  ASSERT_EQ(b.d_pScope, t);
  ASSERT_NE(b.d_pContextObjRestore, nullptr);
  ASSERT_EQ(b.d_pContextObjNext, &a);
  ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);

  d_context->pop();

  ASSERT_EQ(s->d_pContext, d_context.get());
  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
  ASSERT_EQ(s->d_level, 0);
  ASSERT_EQ(s->d_pContextObjList, &c);

  ASSERT_EQ(a.d_pScope, s);
  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
  ASSERT_EQ(a.d_pContextObjNext, nullptr);
  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);

  ASSERT_EQ(b.d_pScope, s);
  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
  ASSERT_EQ(b.d_pContextObjNext, &a);
  ASSERT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext);

  ASSERT_EQ(c.d_pScope, s);
  ASSERT_EQ(c.d_pContextObjRestore, nullptr);
  ASSERT_EQ(c.d_pContextObjNext, &b);
  ASSERT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList);
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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