33 for(symex_target_equationt::SSA_stepst::const_iterator
s_it =
38 if(!
s_it->is_assert())
46 if(
s_it->source.pc->source_location().is_not_nil())
47 out <<
s_it->source.pc->source_location() <<
'\n';
49 if(!
s_it->comment.empty())
50 out <<
s_it->comment <<
'\n';
52 symex_target_equationt::SSA_stepst::const_iterator
p_it =
56 symex_target_equationt::SSA_stepst::const_iterator
last_it =
60 if(
p_it->is_assume() ||
p_it->is_assignment() ||
p_it->is_constraint())
68 out <<
"GUARD: " <<
format(
p_it->guard) <<
'\n';
78 for(
unsigned i = 0; i < 26; i++)
90 std::size_t count = 1;
119 for(symex_target_equationt::SSA_stepst::const_iterator
s_it =
124 if(!
s_it->is_assert())
131 s_it->source.pc->source_location();
133 object[
"sourceLocation"] =
json(source_location);
135 const std::string &s =
s_it->comment;
140 symex_target_equationt::SSA_stepst::const_iterator
last_it =
145 for(symex_target_equationt::SSA_stepst::const_iterator
p_it =
151 (
p_it->is_assume() ||
p_it->is_assignment() ||
p_it->is_constraint()) &&
175 const std::string &filename = options.
get_option(
"outfile");
176 bool have_file = !filename.empty() && filename !=
"-";
185 "failed to open output file: " + filename,
"--outfile");
190 switch(ui_message_handler.
get_ui())
203 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
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.