34 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
39 if(!s_it->is_assert())
47 if(s_it->source.pc->source_location.is_not_nil())
50 if(s_it->comment !=
"")
51 out << s_it->comment <<
'\n';
53 symex_target_equationt::SSA_stepst::const_iterator p_it =
57 symex_target_equationt::SSA_stepst::const_iterator last_it =
60 for(std::size_t count = 1; p_it != last_it; p_it++)
61 if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
66 <<
format(p_it->cond_expr) <<
'\n';
69 out <<
"GUARD: " <<
format(p_it->guard) <<
'\n';
79 for(
unsigned i = 0; i < 26; i++)
86 if(s_it->cond_expr.id() == ID_or)
89 disjuncts.push_back(s_it->cond_expr);
91 std::size_t count = 1;
92 for(
const auto &disjunct : disjuncts)
95 <<
format(disjunct) <<
'\n';
113 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
118 if(!s_it->is_assert())
126 object[
"sourceLocation"] =
json(source_location);
128 const std::string &s = s_it->comment;
133 symex_target_equationt::SSA_stepst::const_iterator last_it =
138 for(symex_target_equationt::SSA_stepst::const_iterator p_it =
144 (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
147 std::ostringstream string_value;
148 string_value <<
format(p_it->cond_expr);
153 std::ostringstream string_value;
154 string_value <<
format(s_it->cond_expr);
155 object[
"expression"] =
json_stringt(string_value.str());
158 out <<
",\n" << json_result;
168 const std::string &filename = options.
get_option(
"outfile");
169 bool have_file = !filename.empty() && filename !=
"-";
178 "failed to open output file: " + filename,
"--outfile");
181 std::ostream &out = have_file ? of : std::cout;
183 switch(ui_message_handler.
get_ui())
196 msg.
status() <<
"Verification conditions written to file"