Skip to content

Commit 4a23411

Browse files
author
Thomas Kiley
committed
Add unit test for the restructured normal step printing
1 parent 96c8aa4 commit 4a23411

File tree

2 files changed

+162
-0
lines changed

2 files changed

+162
-0
lines changed

unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ SRC += analyses/ai/ai.cpp \
3535
goto-programs/label_function_pointer_call_sites.cpp \
3636
goto-programs/osx_fat_reader.cpp \
3737
goto-programs/restrict_function_pointers.cpp \
38+
goto-programs/structured_trace_util.cpp \
3839
goto-programs/remove_returns.cpp \
3940
goto-programs/xml_expr.cpp \
4041
goto-symex/apply_condition.cpp \
Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
/*******************************************************************\
2+
3+
Module: structured_trace_util
4+
5+
Author: Diffblue
6+
7+
\*******************************************************************/
8+
#include <testing-utils/use_catch.h>
9+
10+
#include <goto-programs/goto_trace.h>
11+
#include <goto-programs/structured_trace_util.h>
12+
13+
void link_edges(goto_programt::targett source, goto_programt::targett target)
14+
{
15+
source->targets.push_back(target);
16+
target->incoming_edges.insert(source);
17+
}
18+
19+
TEST_CASE("structured_trace_util", "[core][util][trace]")
20+
{
21+
goto_programt::instructionst instructions;
22+
23+
source_locationt nil_location;
24+
25+
source_locationt unrelated_location;
26+
unrelated_location.set_file("foo.c");
27+
unrelated_location.set_line(1);
28+
29+
source_locationt no_file_location;
30+
unrelated_location.set_line(1);
31+
32+
source_locationt basic_location;
33+
basic_location.set_file("test.c");
34+
basic_location.set_line(1);
35+
36+
source_locationt loop_head_location;
37+
loop_head_location.set_file("test.c");
38+
loop_head_location.set_line(2);
39+
40+
source_locationt back_edge_location;
41+
back_edge_location.set_file("test.c");
42+
back_edge_location.set_line(3);
43+
44+
// 0 # normal_location
45+
// 1 # loop_head
46+
// 2: goto 1 # back_edge
47+
// 3: no_location
48+
// 4: no_file
49+
goto_programt::instructiont normal_instruction;
50+
normal_instruction.location_number = 0;
51+
normal_instruction.source_location = basic_location;
52+
instructions.push_back(normal_instruction);
53+
54+
goto_programt::instructiont loop_head;
55+
loop_head.location_number = 1;
56+
loop_head.source_location = loop_head_location;
57+
instructions.push_back(loop_head);
58+
59+
goto_programt::instructiont back_edge;
60+
back_edge.source_location = back_edge_location;
61+
back_edge.location_number = 2;
62+
back_edge.type = GOTO;
63+
instructions.push_back(back_edge);
64+
65+
goto_programt::instructiont no_location;
66+
no_location.location_number = 3;
67+
instructions.push_back(no_location);
68+
69+
goto_programt::instructiont no_file;
70+
no_file.location_number = 4;
71+
no_file.source_location = no_file_location;
72+
instructions.push_back(no_file);
73+
74+
link_edges(
75+
std::next(instructions.begin(), 2), std::next(instructions.begin(), 1));
76+
77+
SECTION("location-only steps")
78+
{
79+
goto_trace_stept step;
80+
step.step_nr = 1;
81+
step.thread_nr = 2;
82+
step.hidden = true;
83+
SECTION("Simple step")
84+
{
85+
step.pc = instructions.begin();
86+
87+
const auto parsed_step = default_step(step, unrelated_location);
88+
89+
REQUIRE(parsed_step);
90+
REQUIRE(parsed_step->step_number == 1);
91+
REQUIRE(parsed_step->thread_number == 2);
92+
REQUIRE(parsed_step->hidden);
93+
REQUIRE(parsed_step->kind == default_step_kindt::LOCATION_ONLY);
94+
REQUIRE(parsed_step->location == basic_location);
95+
}
96+
SECTION("Invalid previous step")
97+
{
98+
step.pc = instructions.begin();
99+
100+
const auto parsed_step = default_step(step, nil_location);
101+
102+
REQUIRE(parsed_step);
103+
REQUIRE(parsed_step->step_number == 1);
104+
REQUIRE(parsed_step->thread_number == 2);
105+
REQUIRE(parsed_step->hidden);
106+
REQUIRE(parsed_step->kind == default_step_kindt::LOCATION_ONLY);
107+
REQUIRE(parsed_step->location == basic_location);
108+
}
109+
110+
SECTION("Duplicate step")
111+
{
112+
step.pc = instructions.begin();
113+
const auto parsed_step = default_step(step, basic_location);
114+
REQUIRE_FALSE(parsed_step);
115+
}
116+
SECTION("No source location")
117+
{
118+
step.pc = std::next(instructions.begin(), 3);
119+
120+
const auto parsed_step = default_step(step, unrelated_location);
121+
REQUIRE_FALSE(parsed_step);
122+
}
123+
SECTION("No file")
124+
{
125+
step.pc = std::next(instructions.begin(), 4);
126+
127+
const auto parsed_step = default_step(step, unrelated_location);
128+
REQUIRE_FALSE(parsed_step);
129+
}
130+
}
131+
SECTION("Loop head steps")
132+
{
133+
goto_trace_stept step;
134+
step.step_nr = 1;
135+
step.thread_nr = 2;
136+
step.hidden = true;
137+
step.pc = std::next(instructions.begin(), 1);
138+
SECTION("Simple step")
139+
{
140+
const auto parsed_step = default_step(step, unrelated_location);
141+
142+
REQUIRE(parsed_step);
143+
REQUIRE(parsed_step->step_number == 1);
144+
REQUIRE(parsed_step->thread_number == 2);
145+
REQUIRE(parsed_step->hidden);
146+
REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD);
147+
REQUIRE(parsed_step->location == loop_head_location);
148+
}
149+
150+
SECTION("Duplicate step")
151+
{
152+
const auto parsed_step = default_step(step, loop_head_location);
153+
REQUIRE(parsed_step);
154+
REQUIRE(parsed_step->step_number == 1);
155+
REQUIRE(parsed_step->thread_number == 2);
156+
REQUIRE(parsed_step->hidden);
157+
REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD);
158+
REQUIRE(parsed_step->location == loop_head_location);
159+
}
160+
}
161+
}

0 commit comments

Comments
 (0)