32 for(symex_target_equationt::SSA_stepst::const_iterator
s_it =
37 if(!
s_it->is_assert())
45 if(
s_it->source.pc->source_location().is_not_nil())
46 out <<
s_it->source.pc->source_location() <<
'\n';
48 if(!
s_it->comment.empty())
49 out <<
s_it->comment <<
'\n';
51 symex_target_equationt::SSA_stepst::const_iterator
p_it =
55 symex_target_equationt::SSA_stepst::const_iterator
last_it =
59 if(
p_it->is_assume() ||
p_it->is_assignment() ||
p_it->is_constraint())
67 out <<
"GUARD: " <<
format(
p_it->guard) <<
'\n';
77 for(
unsigned i = 0;
i < 26;
i++)
89 std::size_t count = 1;
118 for(symex_target_equationt::SSA_stepst::const_iterator
s_it =
123 if(!
s_it->is_assert())
130 s_it->source.pc->source_location();
132 object[
"sourceLocation"] =
json(source_location);
134 const std::string &s =
s_it->comment;
139 symex_target_equationt::SSA_stepst::const_iterator
last_it =
144 for(symex_target_equationt::SSA_stepst::const_iterator
p_it =
150 (
p_it->is_assume() ||
p_it->is_assignment() ||
p_it->is_constraint()) &&
174 const std::string &filename = options.
get_option(
"outfile");
175 bool have_file = !filename.empty() && filename !=
"-";
184 "failed to open output file: " + filename,
"--outfile");
189 switch(ui_message_handler.
get_ui())
202 msg.
status() <<
"Verification conditions written to file"
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::vector< exprt > operandst
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
static const commandt reset
return to default formatting, as defined by the terminal
static const commandt faint
render text with faint font
mstreamt & status() const
const std::string get_option(const std::string &option) const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual uit get_ui() const
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.
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.
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.
Output of the verification conditions (VCCs)
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Generate Equation using Symbolic Execution.