Skip to content

Commit 68e6eed

Browse files
committed
Output search heuristic and initialisation time
1 parent e246a87 commit 68e6eed

File tree

1 file changed

+30
-0
lines changed

1 file changed

+30
-0
lines changed

src/symex/path_search.cpp

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,31 @@ path_searcht::resultt path_searcht::operator()(
130130

131131
status() << "Starting symbolic simulation" << eom;
132132

133+
switch(search_heuristic)
134+
{
135+
case search_heuristict::DFS:
136+
status() << "Search heuristic: DFS" << eom;
137+
break;
138+
case search_heuristict::RAN_DFS:
139+
status() << "Search heuristic: randomized DFS" << eom;
140+
break;
141+
case search_heuristict::BFS:
142+
status() << "Search heuristic: BFS" << eom;
143+
break;
144+
case search_heuristict::SHORTEST_PATH:
145+
status() << "Search heuristic: shortest path" << eom;
146+
break;
147+
case search_heuristict::SHORTEST_PATH_PER_FUNC:
148+
status() << "Search heuristic: shortest path per function" << eom;
149+
break;
150+
case search_heuristict::RAN_SHORTEST_PATH:
151+
status() << "Search heuristic: randomized shortest path" << eom;
152+
break;
153+
case search_heuristict::LOCS:
154+
status() << "Search heuristic: LOCS" << eom;
155+
break;
156+
}
157+
133158
// this is the container for the history-forest
134159
path_symex_historyt history;
135160

@@ -166,6 +191,11 @@ path_searcht::resultt path_searcht::operator()(
166191
queue.push_back(init_state);
167192
initial_distance_to_property=init_state.get_shortest_path();
168193

194+
time_periodt initialisation_time=current_time()-start_time;
195+
status() << "Initialisation took "<< initialisation_time << "s" << eom;
196+
start_time=current_time();
197+
last_reported_time=start_time;
198+
169199
while(!queue.empty())
170200
{
171201
number_of_steps++;

0 commit comments

Comments
 (0)