Go to the documentation of this file.
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);
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
bool compact_trace
Give a compact trace.
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
const typet & subtype() const
optionalt< symbol_exprt > get_lhs_object() const
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
static const commandt reset
return to default formatting, as defined by the terminal
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
bool show_code
Show original code in plain text trace.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Base class for all expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool is_true() const
Return whether the expression is a constant representing true.
Step of the trace of a GOTO program.
bool is_function_call() const
bool is_assignment() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression classes for byte-level operators.
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
static const commandt faint
render text with faint font
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace step in ASCII to a given stream.
const std::string & id2string(const irep_idt &d)
source_locationt source_location
#define forall_operands(it, expr)
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.
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)
std::vector< exprt > function_arguments
goto_programt::const_targett pc
bool is_index_member_symbol(const exprt &src)
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
Ranges: pair of begin and end iterators, which can be initialized from containers,...
nonstd::optional< T > optionalt
void show_state_header(messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options)
std::size_t get_width() const
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
bool hex_representation
Represent plain trace values in hex.
bool stack_trace
Give a stack trace only.
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 const commandt red
render text with red foreground color
Options for printing the trace using show_goto_trace.
bool show_function_calls
Show function calls in plain text trace.
static const trace_optionst default_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.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
std::string as_string(resultt result)
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const std::string integer2binary(const mp_integer &n, std::size_t width)
unsignedbv_typet size_type()
A constant literal expression.
const irep_idt & get_value() const
ranget< iteratort > make_range(iteratort begin, iteratort end)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)