From 1538ca44389d854154a52cb6e1fae16f3f9da8d2 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 3 Dec 2018 15:50:00 +0000 Subject: [PATCH] Fix symex-backtrace when the stack is empty This happens when symex is about to exit; in this (and AFAIK only this) situation the iterator source is invalid. --- src/goto-symex/goto_symex_state.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index bed62f95b28..e3751fa3ef0 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -765,6 +765,12 @@ void goto_symex_statet::get_l1_name(exprt &expr) const /// \param out: stream to write to void goto_symex_statet::print_backtrace(std::ostream &out) const { + if(threads[source.thread_nr].call_stack.empty()) + { + out << "No stack!\n"; + return; + } + out << source.pc->function << " " << source.pc->location_number << "\n"; for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),