34 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
39 if(!s_it->is_assert())
47 if(s_it->source.pc->source_location.is_not_nil())
50 if(s_it->comment !=
"")
51 out << s_it->comment <<
'\n';
53 symex_target_equationt::SSA_stepst::const_iterator p_it =
57 symex_target_equationt::SSA_stepst::const_iterator last_it =
60 for(std::size_t count = 1; p_it != last_it; p_it++)
61 if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
66 <<
format(p_it->cond_expr) <<
'\n';
69 out <<
"GUARD: " <<
format(p_it->guard) <<
'\n';
79 for(
unsigned i = 0; i < 26; i++)
86 if(s_it->cond_expr.id() == ID_or)
89 disjuncts.push_back(s_it->cond_expr);
91 std::size_t count = 1;
92 for(
const auto &disjunct : disjuncts)
95 <<
format(disjunct) <<
'\n';
113 for(symex_target_equationt::SSA_stepst::const_iterator s_it =
118 if(!s_it->is_assert())
126 object[
"sourceLocation"] =
json(source_location);
128 const std::string &s = s_it->comment;
133 symex_target_equationt::SSA_stepst::const_iterator last_it =
138 for(symex_target_equationt::SSA_stepst::const_iterator p_it =
144 (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
147 std::ostringstream string_value;
148 string_value <<
format(p_it->cond_expr);
153 std::ostringstream string_value;
154 string_value <<
format(s_it->cond_expr);
155 object[
"expression"] =
json_stringt(string_value.str());
158 out <<
",\n" << json_result;
168 const std::string &filename = options.
get_option(
"outfile");
169 bool have_file = !filename.empty() && filename !=
"-";
178 "failed to open output file: " + filename,
"--outfile");
181 std::ostream &out = have_file ? of : std::cout;
183 switch(ui_message_handler.
get_ui())
196 msg.
status() <<
"Verification conditions written to file"
Generate Equation using Symbolic Execution.
Output of the verification conditions (VCCs)
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.
static const commandt reset
return to default formatting, as defined by the terminal
json_arrayt & make_array()
jsont & push_back(const jsont &json)
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
source_locationt source_location
const std::string get_option(const std::string &option) const
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'.
void show_vcc_plain(messaget::mstreamt &out, const symex_target_equationt &equation)
std::vector< exprt > operandst
static const commandt faint
render text with faint font
mstreamt & status() const
json_objectt & make_object()
json_objectt json(const source_locationt &location)
void show_vcc_json(std::ostream &out, const symex_target_equationt &equation)