41 std::cout <<
'(' << count <<
") ";
51 std::cout << std::string(std::to_string(count).size() + 3,
' ');
60 std::size_t count = 1;
62 std::cout <<
'\n' <<
"Program constraints:" <<
'\n';
64 for(
const auto &step : equation.
SSA_steps)
66 std::cout <<
"// " << step.source.pc->location_number <<
" ";
67 std::cout << step.source.pc->source_location().as_string() <<
"\n";
69 if(step.is_assignment())
71 else if(step.is_assert())
73 else if(step.is_assume())
75 else if(step.is_constraint())
80 else if(step.is_shared_read())
81 show_step(ns, step,
"SHARED_READ", count);
82 else if(step.is_shared_write())
83 show_step(ns, step,
"SHARED_WRITE", count);
87template <
typename expr_typet>
91 std::is_base_of<exprt, expr_typet>::value,
92 "`expr_typet` is expected to be a type of `exprt`.");
94 std::size_t count = 0;
121 out <<
ssa_step.source.pc->source_location().as_string() <<
"\n"
131 const std::string
key_srcloc =
"sourceLocation";
146template <
typename expr_typet>
153 for(
const auto &step : equation.
SSA_steps)
169 if(std::is_same<expr_typet, byte_extract_exprt>::value)
170 out <<
'\n' <<
"Number of byte extracts: ";
171 else if(std::is_same<expr_typet, byte_update_exprt>::value)
172 out <<
'\n' <<
"Number of byte updates: ";
180template <
typename expr_typet>
183 if(std::is_same<expr_typet, byte_extract_exprt>::value)
184 return "byteExtractList";
185 else if(std::is_same<expr_typet, byte_update_exprt>::value)
186 return "byteUpdateList";
191template <
typename expr_typet>
194 if(std::is_same<expr_typet, byte_extract_exprt>::value)
195 return "numOfExtracts";
196 else if(std::is_same<expr_typet, byte_update_exprt>::value)
197 return "numOfUpdates";
202template <
typename expr_typet>
221 for(
const auto &step : equation.
SSA_steps)
247template <
typename expr_typet>
250 if(std::is_same<expr_typet, byte_extract_exprt>::value)
251 return "byteExtractStats";
252 else if(std::is_same<expr_typet, byte_update_exprt>::value)
253 return "byteUpdateStats";
260 const std::string &filename = options.
get_option(
"outfile");
261 return (!filename.empty() && filename !=
"-");
314 <<
"XML UI not supported for displaying byte extracts and updates."
326 const std::string &filename = options.
get_option(
"outfile");
333 of.open(filename, std::fstream::out);
336 "failed to open output file: " + filename,
"--outfile");
341 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
mstreamt & status() const
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.