diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 0612b04e2df..7e938118ba7 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -224,7 +224,9 @@ void build_goto_trace( symex_target_equationt::assignment_typet::PHI || SSA_step.assignment_type== symex_target_equationt::assignment_typet::GUARD)) + { continue; + } goto_tracet::stepst &steps=time_map[current_time]; steps.push_back(goto_trace_stept()); diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h index 2aae977f71f..eafea6d7e39 100644 --- a/src/goto-symex/symex_target.h +++ b/src/goto-symex/symex_target.h @@ -53,7 +53,12 @@ class symex_targett enum class assignment_typet { - STATE, HIDDEN, VISIBLE_ACTUAL_PARAMETER, HIDDEN_ACTUAL_PARAMETER, PHI, GUARD + STATE, + HIDDEN, + VISIBLE_ACTUAL_PARAMETER, + HIDDEN_ACTUAL_PARAMETER, + PHI, + GUARD, }; // read event diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 5b5206aff71..0b7bc15a955 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -1002,17 +1002,23 @@ void symex_target_equationt::SSA_stept::output( switch(assignment_type) { case assignment_typet::HIDDEN: - out << "HIDDEN"; break; + out << "HIDDEN"; + break; case assignment_typet::STATE: - out << "STATE"; break; + out << "STATE"; + break; case assignment_typet::VISIBLE_ACTUAL_PARAMETER: - out << "VISIBLE_ACTUAL_PARAMETER"; break; + out << "VISIBLE_ACTUAL_PARAMETER"; + break; case assignment_typet::HIDDEN_ACTUAL_PARAMETER: - out << "HIDDEN_ACTUAL_PARAMETER"; break; + out << "HIDDEN_ACTUAL_PARAMETER"; + break; case assignment_typet::PHI: - out << "PHI"; break; + out << "PHI"; + break; case assignment_typet::GUARD: - out << "GUARD"; break; + out << "GUARD"; + break; default: { } diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index e7f0274aac1..aac51725ad9 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -204,7 +204,7 @@ class symex_target_equationt:public symex_targett bool is_atomic_end() const { return type==goto_trace_stept::typet::ATOMIC_END; } // we may choose to hide - bool hidden; + bool hidden=false; exprt guard; literalt guard_literal; @@ -213,7 +213,7 @@ class symex_target_equationt:public symex_targett ssa_exprt ssa_lhs; exprt ssa_full_lhs, original_full_lhs; exprt ssa_rhs; - assignment_typet assignment_type; + assignment_typet assignment_type=assignment_typet::STATE; // for ASSUME/ASSERT/GOTO/CONSTRAINT exprt cond_expr; @@ -222,7 +222,7 @@ class symex_target_equationt:public symex_targett // for INPUT/OUTPUT irep_idt format_string, io_id; - bool formatted; + bool formatted=false; std::list io_args; std::list converted_io_args; @@ -230,10 +230,10 @@ class symex_target_equationt:public symex_targett irep_idt identifier; // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END - unsigned atomic_section_id; + unsigned atomic_section_id=0; // for slicing - bool ignore; + bool ignore=false; SSA_stept(): type(goto_trace_stept::typet::NONE),