32 if(src.
id()==ID_symbol)
34 else if(src.
id()==ID_member)
36 else if(src.
id()==ID_index)
38 else if(src.
id()==ID_typecast)
41 src.
id() == ID_byte_extract_little_endian ||
42 src.
id() == ID_byte_extract_big_endian)
57 std::ostream &out)
const
59 for(
const auto &step :
steps)
65 std::ostream &out)
const
82 out <<
"ATOMIC_BEGIN";
89 out <<
"FUNCTION RETURN";
break;
114 if(!
pc->source_location.is_nil())
115 out <<
pc->source_location <<
'\n';
117 out <<
pc->type <<
'\n';
123 out <<
"Violated property:" <<
'\n';
124 if(
pc->source_location.is_nil())
125 out <<
" " <<
pc->source_location <<
'\n';
130 out <<
" " <<
format(
pc->get_condition()) <<
'\n';
170 const typet &underlying_type =
171 expr_type.
id() == ID_c_enum_tag
192 std::ostringstream oss;
194 for(
const auto c : result)
197 if(++i % 8 == 0 && result.size() != i)
201 return prefix + oss.str();
213 if(expr.
id()==ID_constant)
215 if(type.
id()==ID_unsignedbv ||
216 type.
id()==ID_signedbv ||
218 type.
id()==ID_fixedbv ||
219 type.
id()==ID_floatbv ||
220 type.
id()==ID_pointer ||
221 type.
id()==ID_c_bit_field ||
222 type.
id()==ID_c_bool ||
223 type.
id()==ID_c_enum ||
224 type.
id()==ID_c_enum_tag)
228 else if(type.
id()==ID_bool)
232 else if(type.
id()==ID_integer)
234 const auto i = numeric_cast<mp_integer>(expr);
235 if(i.has_value() && *i >= 0)
244 else if(expr.
id()==ID_array)
259 else if(expr.
id()==ID_struct)
261 std::string result=
"{ ";
272 else if(expr.
id()==ID_union)
284 const exprt &full_lhs,
290 if(lhs_object.has_value())
291 identifier=lhs_object->get_identifier();
293 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
296 out <<
"(assignment removed)";
314 const auto &source_location = state.
pc->source_location;
316 if(!source_location.get_file().empty())
317 result +=
"file " +
id2string(source_location.get_file());
327 if(!source_location.get_line().empty())
331 result +=
"line " +
id2string(source_location.get_line());
351 out <<
"Initial State";
353 out <<
"State " << step_nr;
356 out <<
"----------------------------------------------------" <<
'\n';
361 out <<
"----------------------------------------------------" <<
'\n';
367 if(src.
id()==ID_index)
369 else if(src.
id()==ID_member)
371 else if(src.
id()==ID_symbol)
388 std::size_t function_depth = 0;
390 for(
const auto &step : goto_trace.
steps)
392 if(step.is_function_call())
394 else if(step.is_function_return())
408 if(!step.pc->source_location.is_nil())
413 if(step.pc->is_assert())
416 <<
from_expr(ns, step.function_id, step.pc->get_condition())
426 step.assignment_type ==
434 if(!step.pc->source_location.get_line().empty())
443 step.get_lhs_object(),
452 if(!step.pc->source_location.get_file().empty())
456 if(!step.pc->source_location.get_line().empty())
466 const auto &f_symbol = ns.
lookup(step.called_function);
467 out << f_symbol.display_name();
471 auto arg_strings =
make_range(step.function_arguments)
472 .map([&ns, &step](
const exprt &arg) {
473 return from_expr(ns, step.function_id, arg);
477 join_strings(out, arg_strings.begin(), arg_strings.end(),
", ");
516 unsigned prev_step_nr=0;
517 bool first_step=
true;
518 std::size_t function_depth=0;
520 for(
const auto &step : goto_trace.
steps)
533 if(!step.pc->source_location.is_nil())
540 if(step.pc->is_assert())
543 <<
from_expr(ns, step.function_id, step.pc->get_condition())
552 if(step.cond_value && step.pc->is_assume())
555 out <<
"Assumption:\n";
557 if(!step.pc->source_location.is_nil())
560 out <<
" " <<
from_expr(ns, step.function_id, step.pc->get_condition())
572 if(step.pc->is_assign() ||
573 step.pc->is_return() ||
574 step.pc->is_function_call() ||
575 (step.pc->is_other() && step.full_lhs.is_not_nil()))
577 if(prev_step_nr!=step.step_nr || first_step)
580 prev_step_nr=step.step_nr;
588 step.get_lhs_object(),
596 if(prev_step_nr!=step.step_nr || first_step)
599 prev_step_nr=step.step_nr;
605 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
612 printf_formatter(
id2string(step.format_string), step.io_args);
613 printf_formatter.
print(out);
619 out <<
" OUTPUT " << step.io_id <<
':';
621 for(std::list<exprt>::const_iterator
622 l_it=step.io_args.begin();
623 l_it!=step.io_args.end();
626 if(l_it!=step.io_args.begin())
629 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
641 out <<
" INPUT " << step.io_id <<
':';
643 for(std::list<exprt>::const_iterator
644 l_it=step.io_args.begin();
645 l_it!=step.io_args.end();
648 if(l_it!=step.io_args.begin())
651 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
664 out <<
"\n#### Function call: " << step.called_function;
668 for(
auto &arg : step.function_arguments)
675 out <<
from_expr(ns, step.function_id, arg);
678 out <<
") (depth " << function_depth <<
") ####\n";
686 out <<
"\n#### Function return from " << step.function_id <<
" (depth "
687 << function_depth <<
") ####\n";
713 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
717 unsigned thread_to_show = 0;
719 for(
auto s_it = goto_trace.
steps.begin(); s_it != goto_trace.
steps.end();
722 const auto &step = *s_it;
723 auto &stack = call_stacks[step.thread_nr];
729 stack.push_back(s_it);
730 thread_to_show = step.thread_nr;
733 else if(step.is_function_call())
735 stack.push_back(s_it);
737 else if(step.is_function_return())
743 const auto &stack = call_stacks[thread_to_show];
746 for(
auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
748 const auto &step = **s_it;
751 out <<
" assertion failure";
752 if(!step.pc->source_location.is_nil())
756 else if(step.is_function_call())
758 out <<
" " << step.called_function;
762 for(
auto &arg : step.function_arguments)
769 out <<
from_expr(ns, step.function_id, arg);
774 if(!step.pc->source_location.is_nil())
800 std::set<irep_idt> property_ids;
801 for(
const auto &step :
steps)
803 if(step.is_assert() && !step.cond_value)
804 property_ids.insert(step.property_id);
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
std::size_t get_width() const
A constant literal expression.
const irep_idt & get_value() const
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.
typet & type()
Return the type of the expression.
Step of the trace of a GOTO program.
std::vector< exprt > function_arguments
bool is_function_call() const
optionalt< symbol_exprt > get_lhs_object() const
bool is_assignment() const
goto_programt::const_targett pc
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace step in ASCII to a given stream.
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
const irep_idt & id() const
source_locationt source_location
static const commandt reset
return to default formatting, as defined by the terminal
static const commandt faint
render text with faint font
static const commandt red
render text with red foreground color
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
const typet & subtype() const
#define forall_operands(it, expr)
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
void show_state_header(messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options)
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
static std::string numeric_representation(const constant_exprt &expr, const namespacet &ns, const trace_optionst &options)
Returns the numeric representation of an expression, based on options.
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
static void trace_value(messaget::mstreamt &out, const namespacet &ns, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options)
bool is_index_member_symbol(const exprt &src)
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
void show_compact_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
show a compact variant of the goto trace on the console
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const std::string integer2string(const mp_integer &n, unsigned base)
const std::string integer2binary(const mp_integer &n, std::size_t width)
nonstd::optional< T > optionalt
std::string as_string(resultt result)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define UNREACHABLE
This should be used to mark dead code.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Options for printing the trace using show_goto_trace.
static const trace_optionst default_options
bool hex_representation
Represent plain trace values in hex.
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
bool show_code
Show original code in plain text trace.
bool compact_trace
Give a compact trace.
bool show_function_calls
Show function calls in plain text trace.
bool stack_trace
Give a stack trace only.