Skip to content

Commit 2a75ab4

Browse files
author
Daniel Kroening
committed
fix for return, debug output
1 parent a4a9475 commit 2a75ab4

File tree

2 files changed

+3
-1
lines changed

2 files changed

+3
-1
lines changed

src/path-symex/path_symex.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -922,6 +922,7 @@ void path_symext::operator()(
922922
case RETURN:
923923
// sets the return value
924924
state.record_step();
925+
state.next_pc();
925926

926927
if(instruction.code.operands().size()==1)
927928
set_return_value(state, instruction.code.op0());

src/symex/path_search.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,8 @@ path_searcht::resultt path_searcht::operator()(
7676
// record we have seen it
7777
loc_data[state.get_pc().loc_number].visited=true;
7878

79-
debug() << "Queue: " << queue.size()
79+
debug() << "Loc: #" << state.get_pc().loc_number
80+
<< ", queue: " << queue.size()
8081
<< ", depth: " << state.get_depth();
8182
for(const auto & s : queue)
8283
debug() << ' ' << s.get_depth();

0 commit comments

Comments
 (0)