Skip to content

Commit 0f7a99d

Browse files
author
Daniel Kroening
committed
added constructor for goto_symex_statet::framet
This enables removing the default constructor for sourcet.
1 parent fca695a commit 0f7a99d

File tree

2 files changed

+12
-2
lines changed

2 files changed

+12
-2
lines changed

src/goto-symex/goto_symex_state.h

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -196,6 +196,11 @@ class goto_symex_statet final
196196
bool is_recursion = false;
197197
};
198198
std::unordered_map<irep_idt, loop_infot> loop_iterations;
199+
200+
explicit framet(const symex_targett::sourcet &_calling_location)
201+
: calling_location(_calling_location)
202+
{
203+
}
199204
};
200205

201206
typedef std::vector<framet> call_stackt;
@@ -224,8 +229,14 @@ class goto_symex_statet final
224229
return call_stack().back();
225230
}
226231

227-
framet &new_frame() { call_stack().push_back(framet()); return top(); }
232+
framet &new_frame()
233+
{
234+
call_stack().emplace_back(source);
235+
return top();
236+
}
237+
228238
void pop_frame() { call_stack().pop_back(); }
239+
229240
const framet &previous_frame() { return *(--(--call_stack().end())); }
230241

231242
void print_backtrace(std::ostream &) const;

src/goto-symex/symex_function_call.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,6 @@ void goto_symext::symex_function_call_code(
311311

312312
frame.end_of_function=--goto_function.body.instructions.end();
313313
frame.return_value=call.lhs();
314-
frame.calling_location=state.source;
315314
frame.function_identifier=identifier;
316315
frame.hidden_function=goto_function.is_hidden();
317316

0 commit comments

Comments
 (0)