33 if(src.
id()==ID_symbol)
35 else if(src.
id()==ID_member)
37 else if(src.
id()==ID_index)
39 else if(src.
id()==ID_typecast)
42 src.
id() == ID_byte_extract_little_endian ||
43 src.
id() == ID_byte_extract_big_endian)
58 std::ostream &out)
const
60 for(
const auto &step :
steps)
66 std::ostream &out)
const
83 out <<
"ATOMIC_BEGIN";
90 out <<
"FUNCTION RETURN";
break;
115 if(!
pc->source_location.is_nil())
116 out <<
pc->source_location <<
'\n';
118 out <<
pc->type <<
'\n';
124 out <<
"Violated property:" <<
'\n';
125 if(
pc->source_location.is_nil())
126 out <<
" " <<
pc->source_location <<
'\n';
131 out <<
" " <<
format(
pc->get_condition()) <<
'\n';
171 const typet &underlying_type =
172 expr_type.
id() == ID_c_enum_tag
193 std::ostringstream oss;
195 for(
const auto c : result)
198 if(++i % 8 == 0 && result.size() != i)
202 return prefix + oss.str();
214 if(expr.
id()==ID_constant)
216 if(type.
id()==ID_unsignedbv ||
217 type.
id()==ID_signedbv ||
219 type.
id()==ID_fixedbv ||
220 type.
id()==ID_floatbv ||
221 type.
id()==ID_pointer ||
222 type.
id()==ID_c_bit_field ||
223 type.
id()==ID_c_bool ||
224 type.
id()==ID_c_enum ||
225 type.
id()==ID_c_enum_tag)
229 else if(type.
id()==ID_bool)
233 else if(type.
id()==ID_integer)
235 const auto i = numeric_cast<mp_integer>(expr);
236 if(i.has_value() && *i >= 0)
245 else if(expr.
id()==ID_array)
260 else if(expr.
id()==ID_struct)
262 std::string result=
"{ ";
273 else if(expr.
id()==ID_union)
285 const exprt &full_lhs,
291 if(lhs_object.has_value())
292 identifier=lhs_object->get_identifier();
294 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
297 out <<
"(assignment removed)";
315 const auto &source_location = state.
pc->source_location;
317 if(!source_location.get_file().empty())
318 result +=
"file " +
id2string(source_location.get_file());
328 if(!source_location.get_line().empty())
332 result +=
"line " +
id2string(source_location.get_line());
352 out <<
"Initial State";
354 out <<
"State " << step_nr;
357 out <<
"----------------------------------------------------" <<
'\n';
362 out <<
"----------------------------------------------------" <<
'\n';
368 if(src.
id()==ID_index)
370 else if(src.
id()==ID_member)
372 else if(src.
id()==ID_symbol)
389 std::size_t function_depth = 0;
391 for(
const auto &step : goto_trace.
steps)
393 if(step.is_function_call())
395 else if(step.is_function_return())
409 if(!step.pc->source_location.is_nil())
414 if(step.pc->is_assert())
417 <<
from_expr(ns, step.function_id, step.pc->get_condition())
427 step.assignment_type ==
435 if(!step.pc->source_location.get_line().empty())
444 step.get_lhs_object(),
453 if(!step.pc->source_location.get_file().empty())
457 if(!step.pc->source_location.get_line().empty())
467 const auto &f_symbol = ns.
lookup(step.called_function);
468 out << f_symbol.display_name();
472 auto arg_strings =
make_range(step.function_arguments)
473 .map([&ns, &step](
const exprt &arg) {
474 return from_expr(ns, step.function_id, arg);
478 join_strings(out, arg_strings.begin(), arg_strings.end(),
", ");
517 unsigned prev_step_nr=0;
518 bool first_step=
true;
519 std::size_t function_depth=0;
521 for(
const auto &step : goto_trace.
steps)
534 if(!step.pc->source_location.is_nil())
541 if(step.pc->is_assert())
544 <<
from_expr(ns, step.function_id, step.pc->get_condition())
553 if(step.cond_value && step.pc->is_assume())
556 out <<
"Assumption:\n";
558 if(!step.pc->source_location.is_nil())
561 out <<
" " <<
from_expr(ns, step.function_id, step.pc->get_condition())
574 step.pc->is_assign() ||
575 step.pc->is_set_return_value() ||
576 step.pc->is_function_call() ||
577 (step.pc->is_other() && step.full_lhs.is_not_nil()))
579 if(prev_step_nr!=step.step_nr || first_step)
582 prev_step_nr=step.step_nr;
590 step.get_lhs_object(),
598 if(prev_step_nr!=step.step_nr || first_step)
601 prev_step_nr=step.step_nr;
607 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
614 printf_formatter(
id2string(step.format_string), step.io_args);
615 printf_formatter.
print(out);
621 out <<
" OUTPUT " << step.io_id <<
':';
623 for(std::list<exprt>::const_iterator
624 l_it=step.io_args.begin();
625 l_it!=step.io_args.end();
628 if(l_it!=step.io_args.begin())
631 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
643 out <<
" INPUT " << step.io_id <<
':';
645 for(std::list<exprt>::const_iterator
646 l_it=step.io_args.begin();
647 l_it!=step.io_args.end();
650 if(l_it!=step.io_args.begin())
653 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
666 out <<
"\n#### Function call: " << step.called_function;
670 for(
auto &arg : step.function_arguments)
677 out <<
from_expr(ns, step.function_id, arg);
680 out <<
") (depth " << function_depth <<
") ####\n";
688 out <<
"\n#### Function return from " << step.function_id <<
" (depth "
689 << function_depth <<
") ####\n";
715 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
719 unsigned thread_to_show = 0;
721 for(
auto s_it = goto_trace.
steps.begin(); s_it != goto_trace.
steps.end();
724 const auto &step = *s_it;
725 auto &stack = call_stacks[step.thread_nr];
731 stack.push_back(s_it);
732 thread_to_show = step.thread_nr;
735 else if(step.is_function_call())
737 stack.push_back(s_it);
739 else if(step.is_function_return())
745 const auto &stack = call_stacks[thread_to_show];
748 for(
auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
750 const auto &step = **s_it;
753 out <<
" assertion failure";
754 if(!step.pc->source_location.is_nil())
758 else if(step.is_function_call())
760 out <<
" " << step.called_function;
764 for(
auto &arg : step.function_arguments)
771 out <<
from_expr(ns, step.function_id, arg);
776 if(!step.pc->source_location.is_nil())
802 std::set<irep_idt> property_ids;
803 for(
const auto &step :
steps)
805 if(step.is_assert() && !step.cond_value)
806 property_ids.insert(step.property_id);
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
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
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.
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
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.
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.