28 out <<
"\n" <<
"VERIFICATION CONDITIONS:" <<
"\n" <<
"\n";
34 for(symex_target_equationt::SSA_stepst::iterator
39 if(!s_it->is_assert())
42 if(s_it->source.pc->source_location.is_not_nil())
43 out << s_it->source.pc->source_location <<
"\n";
46 out << s_it->comment <<
"\n";
48 symex_target_equationt::SSA_stepst::const_iterator
52 symex_target_equationt::SSA_stepst::const_iterator
55 for(
unsigned count=1; p_it!=last_it; p_it++)
56 if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
60 std::string string_value;
61 languages.
from_expr(p_it->cond_expr, string_value);
62 out <<
"{-" << count <<
"} " << string_value <<
"\n";
65 languages.
from_expr(p_it->guard_expr, string_value);
66 out <<
"GUARD: " << string_value <<
"\n";
74 out <<
"|--------------------------" <<
"\n";
76 std::string string_value;
77 languages.
from_expr(s_it->cond_expr, string_value);
78 out <<
"{" << 1 <<
"} " << string_value <<
"\n";
94 for(symex_target_equationt::SSA_stepst::iterator
99 if(!s_it->is_assert())
107 object[
"sourceLocation"]=
json(source_location);
109 const std::string &s=s_it->comment;
114 symex_target_equationt::SSA_stepst::const_iterator
119 for(symex_target_equationt::SSA_stepst::const_iterator p_it
121 p_it!=last_it; p_it++)
123 if((p_it->is_assume() ||
124 p_it->is_assignment() ||
125 p_it->is_constraint()) &&
128 std::string string_value;
129 languages.
from_expr(p_it->cond_expr, string_value);
134 std::string string_value;
135 languages.
from_expr(s_it->cond_expr, string_value);
139 out <<
",\n" << json_result;
145 bool have_file=!filename.empty() && filename!=
"-";
153 throw "failed to open file "+filename;
156 std::ostream &out=have_file?of:std::cout;
161 error() <<
"XML UI not supported" <<
eom;
virtual void show_vcc_plain(std::ostream &out)
bool from_expr(const exprt &expr, std::string &code)
languaget * new_ansi_c_language()
static mstreamt & eom(mstreamt &m)
json_arrayt & make_array()
jsont & push_back(const jsont &json)
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)