25 out <<
"\n" <<
"VERIFICATION CONDITIONS:" <<
"\n" <<
"\n";
29 for(symex_target_equationt::SSA_stepst::iterator
34 if(!s_it->is_assert())
37 if(s_it->source.pc->source_location.is_not_nil())
38 out << s_it->source.pc->source_location <<
"\n";
41 out << s_it->comment <<
"\n";
43 symex_target_equationt::SSA_stepst::const_iterator
47 symex_target_equationt::SSA_stepst::const_iterator
50 for(std::size_t count=1; p_it!=last_it; p_it++)
51 if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
55 std::string string_value=
56 from_expr(
ns, p_it->source.pc->function, p_it->cond_expr);
57 out <<
"{-" << count <<
"} " << string_value <<
"\n";
60 languages.from_expr(p_it->guard_expr, string_value);
61 out <<
"GUARD: " << string_value <<
"\n";
69 out <<
"|--------------------------" <<
"\n";
71 std::string string_value=
72 from_expr(
ns, s_it->source.pc->function, s_it->cond_expr);
73 out <<
"{" << 1 <<
"} " << string_value <<
"\n";
87 for(symex_target_equationt::SSA_stepst::iterator
92 if(!s_it->is_assert())
100 object[
"sourceLocation"]=
json(source_location);
102 const std::string &s=s_it->comment;
107 symex_target_equationt::SSA_stepst::const_iterator
112 for(symex_target_equationt::SSA_stepst::const_iterator p_it
114 p_it!=last_it; p_it++)
116 if((p_it->is_assume() ||
117 p_it->is_assignment() ||
118 p_it->is_constraint()) &&
121 std::string string_value=
122 from_expr(
ns, p_it->source.pc->function, p_it->cond_expr);
127 std::string string_value=
128 from_expr(
ns, s_it->source.pc->function, s_it->cond_expr);
132 out <<
",\n" << json_result;
138 bool have_file=!filename.empty() && filename!=
"-";
146 throw "failed to open file "+filename;
149 std::ostream &out=have_file?of:std::cout;
154 error() <<
"XML UI not supported" <<
eom;
virtual void show_vcc_plain(std::ostream &out)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static mstreamt & eom(mstreamt &m)
json_arrayt & make_array()
jsont & push_back(const jsont &json)
ui_message_handlert::uit ui
const std::string get_option(const std::string &option) const
virtual void show_vcc_json(std::ostream &out)
Bounded Model Checking for ANSI-C + HDL.
symex_target_equationt equation
json_objectt & make_object()
json_objectt json(const source_locationt &location)