33 const std::string &annotation,
41 std::cout <<
'(' << count <<
") ";
42 if(annotation.empty())
43 std::cout << string_value;
45 std::cout << annotation <<
'(' << string_value <<
')';
50 const std::string guard_string =
from_expr(ns, function_id, step.
guard);
52 std::cout <<
"guard: " << guard_string <<
'\n';
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);
87 template <
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;
96 if(can_cast_expr<expr_typet>(e))
115 const exprt &ssa_expr)
118 const std::string ssa_expr_as_string =
from_expr(ns, function_id, ssa_expr);
121 out << ssa_step.
source.
pc->source_location.as_string() <<
"\n"
123 out << ssa_expr_as_string <<
"\n";
129 const exprt &ssa_expr)
131 const std::string key_srcloc =
"sourceLocation";
132 const std::string key_ssa_expr =
"ssaExpr";
133 const std::string key_ssa_expr_as_string =
"ssaExprString";
136 const std::string ssa_expr_as_string =
from_expr(ns, function_id, ssa_expr);
139 {key_srcloc,
json(ssa_step.
source.
pc->source_location)},
140 {key_ssa_expr_as_string,
json_stringt(ssa_expr_as_string)},
143 return json_ssa_step;
146 template <
typename expr_typet>
152 std::size_t equation_byte_op_count = 0;
153 for(
const auto &step : equation.
SSA_steps)
158 const exprt &ssa_expr = step.get_ssa_expr();
159 const std::size_t ssa_expr_byte_op_count =
160 count_expr_typed<expr_typet>(ssa_expr);
162 if(ssa_expr_byte_op_count == 0)
165 equation_byte_op_count += ssa_expr_byte_op_count;
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: ";
176 out << equation_byte_op_count <<
'\n';
180 template <
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";
191 template <
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";
202 template <
typename expr_typet>
214 const std::string key_byte_op_list = json_get_key_byte_op_list<expr_typet>();
215 const std::string key_byte_op_num = json_get_key_byte_op_num<expr_typet>();
220 std::size_t equation_byte_op_count = 0;
221 for(
const auto &step : equation.
SSA_steps)
226 const exprt &ssa_expr = step.get_ssa_expr();
227 const std::size_t ssa_expr_byte_op_count =
228 count_expr_typed<expr_typet>(ssa_expr);
230 if(ssa_expr_byte_op_count == 0)
233 equation_byte_op_count += ssa_expr_byte_op_count;
237 byte_op_stats[key_byte_op_num] =
240 return byte_op_stats;
247 template <
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 !=
"-");
278 show_byte_op_plain<byte_extract_exprt>(mout.
status(), ns, equation);
281 show_byte_op_plain<byte_update_exprt>(mout.
status(), ns, equation);
286 show_byte_op_plain<byte_extract_exprt>(msg.
status(), ns, equation);
289 show_byte_op_plain<byte_update_exprt>(msg.
status(), ns, equation);
299 {json_get_key_byte_op_stats<byte_extract_exprt>(),
300 get_byte_op_json<byte_extract_exprt>(ns, equation)},
301 {json_get_key_byte_op_stats<byte_update_exprt>(),
302 get_byte_op_json<byte_update_exprt>(ns, equation)}};
305 json_result[
"byteOpsStats"] = byte_ops_stats;
307 out <<
",\n" << json_result;
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");
339 std::ostream &out = outfile_given ? of : std::cout;
341 switch(ui_message_handler.
get_ui())