Go to the documentation of this file.
35 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
40 if(!s_it->is_assert())
48 if(s_it->source.pc->source_location.is_not_nil())
49 out << s_it->source.pc->source_location <<
'\n';
51 if(!s_it->comment.empty())
52 out << s_it->comment <<
'\n';
54 symex_target_equationt::SSA_stepst::const_iterator p_it =
58 symex_target_equationt::SSA_stepst::const_iterator last_it =
59 has_threads ? equation.
SSA_steps.end() : s_it;
61 for(std::size_t count = 1; p_it != last_it; p_it++)
62 if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
67 <<
format(p_it->cond_expr) <<
'\n';
70 out <<
"GUARD: " <<
format(p_it->guard) <<
'\n';
80 for(
unsigned i = 0; i < 26; i++)
87 if(s_it->cond_expr.id() == ID_or)
90 disjuncts.push_back(s_it->cond_expr);
92 std::size_t count = 1;
93 for(
const auto &disjunct : disjuncts)
96 <<
format(disjunct) <<
'\n';
121 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
126 if(!s_it->is_assert())
134 object[
"sourceLocation"] =
json(source_location);
136 const std::string &s = s_it->comment;
141 symex_target_equationt::SSA_stepst::const_iterator last_it =
142 has_threads ? equation.
SSA_steps.end() : s_it;
146 for(symex_target_equationt::SSA_stepst::const_iterator p_it =
152 (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
155 std::ostringstream string_value;
156 string_value <<
format(p_it->cond_expr);
161 std::ostringstream string_value;
162 string_value <<
format(s_it->cond_expr);
163 object[
"expression"] =
json_stringt(string_value.str());
166 out <<
",\n" << json_result;
176 const std::string &filename = options.
get_option(
"outfile");
177 bool have_file = !filename.empty() && filename !=
"-";
186 "failed to open output file: " + filename,
"--outfile");
189 std::ostream &
out = have_file ? of : std::cout;
191 switch(ui_message_handler.
get_ui())
204 msg.
status() <<
"Verification conditions written to file"
Class that provides messages with a built-in verbosity 'level'.
Generate Equation using Symbolic Execution.
static const commandt reset
return to default formatting, as defined by the terminal
Output of the verification conditions (VCCs)
const std::string get_option(const std::string &option) const
mstreamt & status() const
static void show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
Output equations from equation in the JSON format to the given output stream out.
json_objectt & make_object()
virtual uit get_ui() const
static const commandt faint
render text with faint font
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
static void show_vcc_plain(messaget::mstreamt &out, const symex_target_equationt &equation)
Output equations from equation in plain text format to the given output stream out.
std::vector< exprt > operandst
json_arrayt & make_array()
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Output equations from equation to a file or to the standard output.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
jsont & push_back(const jsont &json)