32 const std::string &annotation,
41 std::cout <<
"(sliced) ";
43 std::cout <<
'(' << count <<
") ";
44 if(annotation.empty())
53 std::cout << std::string(std::to_string(count).size() + 3,
' ');
62 std::size_t count = 1;
64 std::cout <<
'\n' <<
"Program constraints:" <<
'\n';
66 for(
const auto &step : equation.
SSA_steps)
68 std::cout <<
"// " << step.source.pc->location_number <<
" ";
69 std::cout << step.source.pc->source_location().as_string() <<
"\n";
71 if(step.is_assignment())
73 else if(step.is_assert())
75 else if(step.is_assume())
77 else if(step.is_constraint())
82 else if(step.is_shared_read())
83 show_step(ns, step,
"SHARED_READ", count);
84 else if(step.is_shared_write())
85 show_step(ns, step,
"SHARED_WRITE", count);
89template <
typename expr_typet>
93 std::is_base_of<exprt, expr_typet>::value,
94 "`expr_typet` is expected to be a type of `exprt`.");
96 std::size_t count = 0;
123 out <<
ssa_step.source.pc->source_location().as_string() <<
"\n"
133 const std::string
key_srcloc =
"sourceLocation";
148template <
typename expr_typet>
155 for(
const auto &step : equation.
SSA_steps)
171 if(std::is_same<expr_typet, byte_extract_exprt>::value)
172 out <<
'\n' <<
"Number of byte extracts: ";
173 else if(std::is_same<expr_typet, byte_update_exprt>::value)
174 out <<
'\n' <<
"Number of byte updates: ";
182template <
typename expr_typet>
185 if(std::is_same<expr_typet, byte_extract_exprt>::value)
186 return "byteExtractList";
187 else if(std::is_same<expr_typet, byte_update_exprt>::value)
188 return "byteUpdateList";
193template <
typename expr_typet>
196 if(std::is_same<expr_typet, byte_extract_exprt>::value)
197 return "numOfExtracts";
198 else if(std::is_same<expr_typet, byte_update_exprt>::value)
199 return "numOfUpdates";
204template <
typename expr_typet>
223 for(
const auto &step : equation.
SSA_steps)
249template <
typename expr_typet>
252 if(std::is_same<expr_typet, byte_extract_exprt>::value)
253 return "byteExtractStats";
254 else if(std::is_same<expr_typet, byte_update_exprt>::value)
255 return "byteUpdateStats";
262 const std::string &filename = options.
get_option(
"outfile");
263 return (!filename.empty() && filename !=
"-");
316 <<
"XML UI not supported for displaying byte extracts and updates."
328 const std::string &filename = options.
get_option(
"outfile");
335 of.open(filename, std::fstream::out);
338 "failed to open output file: " + filename,
"--outfile");
343 switch(ui_message_handler.
get_ui())
Expression classes for byte-level operators.
Single SSA step in the equation.
bool is_shared_write() const
symex_targett::sourcet source
bool is_shared_read() const
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
void visit_pre(std::function< void(exprt &)>)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
json_objectt convert_from_irep(const irept &) const
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees.
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
std::string json_get_key_byte_op_list()
void show_ssa_step_plain(messaget::mstreamt &out, const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
std::string json_get_key_byte_op_stats()
std::string json_get_key_byte_op_num()
static void show_step(const namespacet &ns, const SSA_stept &step, const std::string &annotation, std::size_t &count)
Output a single SSA step.
json_objectt get_ssa_step_json(const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
std::size_t count_expr_typed(const exprt &expr)
void show_byte_op_plain(messaget::mstreamt &out, const namespacet &ns, const symex_target_equationt &equation)
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
bool duplicated_previous_step(const SSA_stept &ssa_step)
bool is_outfile_specified(const optionst &options)
void show_byte_ops_json(std::ostream &out, const namespacet &ns, const symex_target_equationt &equation)
void show_byte_ops_xml(ui_message_handlert &ui_message_handler)
void show_byte_ops_plain(ui_message_handlert &ui_message_handler, std::ostream &out, bool outfile_given, const namespacet &ns, const symex_target_equationt &equation)
json_objectt get_byte_op_json(const namespacet &ns, const symex_target_equationt &equation)
void show_byte_ops(const optionst &options, ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation)
Count and display all byte extract and byte update operations from equation on standard output or fil...
Output of the program (SSA) constraints.
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
Generate Equation using Symbolic Execution.