Skip to content

Commit e640b99

Browse files
owen-mc-diffblueowen-mc-diffblue
committed
Unit tests for goto_state::apply_condition
All the main branches are now covered
1 parent 0d56ddd commit e640b99

File tree

2 files changed

+208
-0
lines changed

2 files changed

+208
-0
lines changed

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ SRC += analyses/ai/ai.cpp \
3131
goto-programs/osx_fat_reader.cpp \
3232
goto-programs/remove_returns.cpp \
3333
goto-programs/xml_expr.cpp \
34+
goto-symex/apply_condition.cpp \
3435
goto-symex/expr_skeleton.cpp \
3536
goto-symex/goto_symex_state.cpp \
3637
goto-symex/ssa_equation.cpp \

‎unit/goto-symex/apply_condition.cpp

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for goto_statet::apply_condition
4+
5+
Author: Owen Mansel-Chan, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/message.h>
10+
#include <testing-utils/use_catch.h>
11+
12+
#include <goto-symex/goto_symex.h>
13+
14+
static void add_to_symbol_table(
15+
symbol_tablet &symbol_table,
16+
const symbol_exprt &symbol_expr)
17+
{
18+
symbolt symbol;
19+
symbol.name = symbol_expr.get_identifier();
20+
symbol.type = symbol_expr.type();
21+
symbol.value = symbol_expr;
22+
symbol.is_thread_local = true;
23+
symbol_table.insert(symbol);
24+
}
25+
26+
SCENARIO(
27+
"Apply condition and update constant propagator and value-set",
28+
"[core][goto-symex][apply_condition]")
29+
{
30+
const symbol_exprt b{"b", bool_typet{}};
31+
const symbol_exprt c{"c", bool_typet{}};
32+
33+
// Add symbols to symbol table
34+
symbol_tablet symbol_table;
35+
namespacet ns{symbol_table};
36+
add_to_symbol_table(symbol_table, b);
37+
add_to_symbol_table(symbol_table, c);
38+
39+
// Initialize goto state
40+
std::list<goto_programt::instructiont> target;
41+
symex_targett::sourcet source{"fun", target.begin()};
42+
guard_managert guard_manager;
43+
std::size_t count = 0;
44+
auto fresh_name = [&count](const irep_idt &) { return count++; };
45+
goto_symex_statet state{source,
46+
DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
47+
guard_manager,
48+
fresh_name};
49+
50+
goto_statet goto_state{state};
51+
const exprt renamed_b = state.rename<L2>(b, ns).get();
52+
const exprt renamed_c = state.rename<L2>(c, ns).get();
53+
54+
WHEN("Applying the condition 'b'")
55+
{
56+
const exprt condition = renamed_b;
57+
goto_state.apply_condition(condition, state, ns);
58+
59+
THEN("b should be in the constant propagator with value 'true'")
60+
{
61+
auto it = goto_state.propagation.find(
62+
to_ssa_expr(renamed_b).get_l1_object_identifier());
63+
REQUIRE(it);
64+
REQUIRE(it->get() == true_exprt{});
65+
}
66+
}
67+
68+
WHEN("Applying the condition '!b'")
69+
{
70+
const exprt condition = not_exprt{renamed_b};
71+
goto_state.apply_condition(condition, state, ns);
72+
73+
THEN("b should be in the constant propagator with value 'false'")
74+
{
75+
auto it = goto_state.propagation.find(
76+
to_ssa_expr(renamed_b).get_l1_object_identifier());
77+
REQUIRE(it);
78+
REQUIRE(it->get() == false_exprt{});
79+
}
80+
}
81+
82+
WHEN("Applying the condition 'b == true'")
83+
{
84+
const exprt condition = equal_exprt{renamed_b, true_exprt{}};
85+
goto_state.apply_condition(condition, state, ns);
86+
87+
THEN("b should be in the constant propagator with value 'true'")
88+
{
89+
auto it = goto_state.propagation.find(
90+
to_ssa_expr(renamed_b).get_l1_object_identifier());
91+
REQUIRE(it);
92+
REQUIRE(it->get() == true_exprt{});
93+
}
94+
}
95+
96+
WHEN("Applying the condition 'b == false'")
97+
{
98+
const exprt condition = equal_exprt{renamed_b, false_exprt{}};
99+
goto_state.apply_condition(condition, state, ns);
100+
101+
THEN("b should be in the constant propagator with value 'false'")
102+
{
103+
auto it = goto_state.propagation.find(
104+
to_ssa_expr(renamed_b).get_l1_object_identifier());
105+
REQUIRE(it);
106+
REQUIRE(it->get() == false_exprt{});
107+
}
108+
}
109+
110+
WHEN("Applying the condition '!(b == true)'")
111+
{
112+
const exprt condition = not_exprt{equal_exprt{renamed_b, true_exprt{}}};
113+
goto_state.apply_condition(condition, state, ns);
114+
115+
THEN("b should be in the constant propagator with value 'false'")
116+
{
117+
auto it = goto_state.propagation.find(
118+
to_ssa_expr(renamed_b).get_l1_object_identifier());
119+
REQUIRE(it);
120+
REQUIRE(it->get() == false_exprt{});
121+
}
122+
}
123+
124+
WHEN("Applying the condition '!(b == false)'")
125+
{
126+
const exprt condition = not_exprt{equal_exprt{renamed_b, false_exprt{}}};
127+
goto_state.apply_condition(condition, state, ns);
128+
129+
THEN("b should be in the constant propagator with value 'true'")
130+
{
131+
auto it = goto_state.propagation.find(
132+
to_ssa_expr(renamed_b).get_l1_object_identifier());
133+
REQUIRE(it);
134+
REQUIRE(it->get() == true_exprt{});
135+
}
136+
}
137+
138+
WHEN("Applying the condition 'b != true'")
139+
{
140+
const exprt condition = notequal_exprt{renamed_b, true_exprt{}};
141+
goto_state.apply_condition(condition, state, ns);
142+
143+
THEN("b should be in the constant propagator with value 'false'")
144+
{
145+
auto it = goto_state.propagation.find(
146+
to_ssa_expr(renamed_b).get_l1_object_identifier());
147+
REQUIRE(it);
148+
REQUIRE(it->get() == false_exprt{});
149+
}
150+
}
151+
152+
WHEN("Applying the condition 'b != false'")
153+
{
154+
const exprt condition = notequal_exprt{renamed_b, false_exprt{}};
155+
goto_state.apply_condition(condition, state, ns);
156+
157+
THEN("b should be in the constant propagator with value 'true'")
158+
{
159+
auto it = goto_state.propagation.find(
160+
to_ssa_expr(renamed_b).get_l1_object_identifier());
161+
REQUIRE(it);
162+
REQUIRE(it->get() == true_exprt{});
163+
}
164+
}
165+
166+
WHEN("Applying the condition '!(b != true)'")
167+
{
168+
const exprt condition = not_exprt{notequal_exprt{renamed_b, true_exprt{}}};
169+
goto_state.apply_condition(condition, state, ns);
170+
171+
THEN("b should be in the constant propagator with value 'true'")
172+
{
173+
auto it = goto_state.propagation.find(
174+
to_ssa_expr(renamed_b).get_l1_object_identifier());
175+
REQUIRE(it);
176+
REQUIRE(it->get() == true_exprt{});
177+
}
178+
}
179+
180+
WHEN("Applying the condition '!(b != false)'")
181+
{
182+
const exprt condition = not_exprt{notequal_exprt{renamed_b, false_exprt{}}};
183+
goto_state.apply_condition(condition, state, ns);
184+
185+
THEN("b should be in the constant propagator with value 'false'")
186+
{
187+
auto it = goto_state.propagation.find(
188+
to_ssa_expr(renamed_b).get_l1_object_identifier());
189+
REQUIRE(it);
190+
REQUIRE(it->get() == false_exprt{});
191+
}
192+
}
193+
194+
WHEN("Applying the condition 'b && c'")
195+
{
196+
const exprt condition = and_exprt{renamed_b, renamed_c};
197+
goto_state.apply_condition(condition, state, ns);
198+
199+
THEN("b should be in the constant propagator with value 'true'")
200+
{
201+
auto it = goto_state.propagation.find(
202+
to_ssa_expr(renamed_b).get_l1_object_identifier());
203+
REQUIRE(it);
204+
REQUIRE(it->get() == true_exprt{});
205+
}
206+
}
207+
}

0 commit comments

Comments
 (0)