Go to the documentation of this file.
31 if(src.
id()==ID_symbol)
33 else if(src.
id()==ID_member)
35 else if(src.
id()==ID_index)
37 else if(src.
id()==ID_typecast)
40 src.
id() == ID_byte_extract_little_endian ||
41 src.
id() == ID_byte_extract_big_endian)
56 std::ostream &out)
const
58 for(
const auto &step :
steps)
64 std::ostream &out)
const
81 out <<
"ATOMIC_BEGIN";
88 out <<
"FUNCTION RETURN";
break;
113 if(!
pc->source_location.is_nil())
114 out <<
pc->source_location <<
'\n';
116 out <<
pc->type <<
'\n';
122 out <<
"Violated property:" <<
'\n';
123 if(
pc->source_location.is_nil())
124 out <<
" " <<
pc->source_location <<
'\n';
129 out <<
" " <<
format(
pc->get_condition()) <<
'\n';
155 const typet &underlying_type =
156 expr_type.
id() == ID_c_enum_tag
177 std::ostringstream oss;
179 for(
const auto c : result)
182 if(++i % 8 == 0 && result.size() != i)
186 return prefix + oss.str();
198 if(expr.
id()==ID_constant)
200 if(type.
id()==ID_unsignedbv ||
201 type.
id()==ID_signedbv ||
203 type.
id()==ID_fixedbv ||
204 type.
id()==ID_floatbv ||
205 type.
id()==ID_pointer ||
206 type.
id()==ID_c_bit_field ||
207 type.
id()==ID_c_bool ||
208 type.
id()==ID_c_enum ||
209 type.
id()==ID_c_enum_tag)
213 else if(type.
id()==ID_bool)
217 else if(type.
id()==ID_integer)
219 const auto i = numeric_cast<mp_integer>(expr);
220 if(i.has_value() && *i >= 0)
229 else if(expr.
id()==ID_array)
244 else if(expr.
id()==ID_struct)
246 std::string result=
"{ ";
257 else if(expr.
id()==ID_union)
269 const exprt &full_lhs,
275 if(lhs_object.has_value())
276 identifier=lhs_object->get_identifier();
278 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
281 out <<
"(assignment removed)";
299 const auto &source_location = state.
pc->source_location;
301 if(!source_location.get_file().empty())
302 result +=
"file " +
id2string(source_location.get_file());
312 if(!source_location.get_line().empty())
316 result +=
"line " +
id2string(source_location.get_line());
336 out <<
"Initial State";
338 out <<
"State " << step_nr;
341 out <<
"----------------------------------------------------" <<
'\n';
346 out <<
"----------------------------------------------------" <<
'\n';
352 if(src.
id()==ID_index)
354 else if(src.
id()==ID_member)
356 else if(src.
id()==ID_symbol)
373 std::size_t function_depth = 0;
375 for(
const auto &step : goto_trace.
steps)
377 if(step.is_function_call())
379 else if(step.is_function_return())
393 if(!step.pc->source_location.is_nil())
398 if(step.pc->is_assert())
401 <<
from_expr(ns, step.function_id, step.pc->get_condition())
411 step.assignment_type ==
419 if(!step.pc->source_location.get_line().empty())
428 step.get_lhs_object(),
437 if(!step.pc->source_location.get_file().empty())
441 if(!step.pc->source_location.get_line().empty())
451 const auto &f_symbol = ns.
lookup(step.called_function);
452 out << f_symbol.display_name();
456 auto arg_strings =
make_range(step.function_arguments)
457 .map([&ns, &step](
const exprt &arg) {
458 return from_expr(ns, step.function_id, arg);
462 join_strings(out, arg_strings.begin(), arg_strings.end(),
", ");
501 unsigned prev_step_nr=0;
502 bool first_step=
true;
503 std::size_t function_depth=0;
505 for(
const auto &step : goto_trace.
steps)
518 if(!step.pc->source_location.is_nil())
525 if(step.pc->is_assert())
528 <<
from_expr(ns, step.function_id, step.pc->get_condition())
537 if(step.cond_value && step.pc->is_assume())
540 out <<
"Assumption:\n";
542 if(!step.pc->source_location.is_nil())
545 out <<
" " <<
from_expr(ns, step.function_id, step.pc->get_condition())
557 if(step.pc->is_assign() ||
558 step.pc->is_return() ||
559 step.pc->is_function_call() ||
560 (step.pc->is_other() && step.full_lhs.is_not_nil()))
562 if(prev_step_nr!=step.step_nr || first_step)
565 prev_step_nr=step.step_nr;
573 step.get_lhs_object(),
581 if(prev_step_nr!=step.step_nr || first_step)
584 prev_step_nr=step.step_nr;
590 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
597 printf_formatter(
id2string(step.format_string), step.io_args);
598 printf_formatter.
print(out);
604 out <<
" OUTPUT " << step.io_id <<
':';
606 for(std::list<exprt>::const_iterator
607 l_it=step.io_args.begin();
608 l_it!=step.io_args.end();
611 if(l_it!=step.io_args.begin())
614 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
626 out <<
" INPUT " << step.io_id <<
':';
628 for(std::list<exprt>::const_iterator
629 l_it=step.io_args.begin();
630 l_it!=step.io_args.end();
633 if(l_it!=step.io_args.begin())
636 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
649 out <<
"\n#### Function call: " << step.called_function;
653 for(
auto &arg : step.function_arguments)
660 out <<
from_expr(ns, step.function_id, arg);
663 out <<
") (depth " << function_depth <<
") ####\n";
671 out <<
"\n#### Function return from " << step.function_id <<
" (depth "
672 << function_depth <<
") ####\n";
698 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
702 unsigned thread_to_show = 0;
704 for(
auto s_it = goto_trace.
steps.begin(); s_it != goto_trace.
steps.end();
707 const auto &step = *s_it;
708 auto &stack = call_stacks[step.thread_nr];
714 stack.push_back(s_it);
715 thread_to_show = step.thread_nr;
718 else if(step.is_function_call())
720 stack.push_back(s_it);
722 else if(step.is_function_return())
728 const auto &stack = call_stacks[thread_to_show];
731 for(
auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
733 const auto &step = **s_it;
736 out <<
" assertion failure";
737 if(!step.pc->source_location.is_nil())
741 else if(step.is_function_call())
743 out <<
" " << step.called_function;
747 for(
auto &arg : step.function_arguments)
754 out <<
from_expr(ns, step.function_id, arg);
759 if(!step.pc->source_location.is_nil())
785 std::set<irep_idt> property_ids;
786 for(
const auto &step :
steps)
788 if(step.is_assert() && !step.cond_value)
789 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)
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
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)