35 if(src.
id()==ID_symbol)
37 else if(src.
id()==ID_member)
39 else if(src.
id()==ID_index)
41 else if(src.
id()==ID_typecast)
44 src.
id() == ID_byte_extract_little_endian ||
45 src.
id() == ID_byte_extract_big_endian)
60 std::ostream &out)
const
62 for(
const auto &step :
steps)
68 std::ostream &out)
const
85 out <<
"ATOMIC_BEGIN";
92 out <<
"FUNCTION RETURN";
break;
117 if(!
pc->source_location().is_nil())
118 out <<
pc->source_location() <<
'\n';
120 out <<
pc->type() <<
'\n';
126 out <<
"Violated property:" <<
'\n';
127 if(
pc->source_location().is_nil())
128 out <<
" " <<
pc->source_location() <<
'\n';
173 const typet &underlying_type =
174 expr_type.
id() == ID_c_enum_tag
195 std::ostringstream oss;
197 for(
const auto c : result)
204 return prefix + oss.str();
218 if(type.
id()==ID_unsignedbv ||
219 type.
id()==ID_signedbv ||
221 type.
id()==ID_fixedbv ||
222 type.
id()==ID_floatbv ||
223 type.
id()==ID_pointer ||
224 type.
id()==ID_c_bit_field ||
225 type.
id()==ID_c_bool ||
226 type.
id()==ID_c_enum ||
227 type.
id()==ID_c_enum_tag)
231 else if(type.
id()==ID_bool)
235 else if(type.
id()==ID_integer)
237 const auto i = numeric_cast<mp_integer>(expr);
238 if(i.has_value() && *i >= 0)
247 else if(expr.
id() == ID_annotated_pointer_constant)
249 const auto &annotated_pointer_constant =
252 auto &value = annotated_pointer_constant.get_value();
256 else if(expr.
id()==ID_array)
260 for(
const auto &op : expr.
operands())
271 else if(expr.
id()==ID_struct)
273 std::string result=
"{ ";
284 else if(expr.
id()==ID_union)
295 const std::optional<symbol_exprt> &lhs_object,
296 const exprt &full_lhs,
302 if(lhs_object.has_value())
303 identifier=lhs_object->get_identifier();
305 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
308 out <<
"(assignment removed)";
326 const auto &source_location = state.
pc->source_location();
328 if(!source_location.get_file().empty())
329 result +=
"file " +
id2string(source_location.get_file());
339 if(!source_location.get_line().empty())
343 result +=
"line " +
id2string(source_location.get_line());
363 out <<
"Initial State";
365 out <<
"State " << step_nr;
368 out <<
"----------------------------------------------------" <<
'\n';
373 out <<
"----------------------------------------------------" <<
'\n';
379 if(src.
id()==ID_index)
381 else if(src.
id()==ID_member)
383 else if(src.
id()==ID_symbol)
400 for(
const auto &step : goto_trace.
steps)
413 if(!step.pc->source_location().is_nil())
418 if(step.pc->is_assert())
421 <<
from_expr(ns, step.function_id, step.original_condition)
431 step.assignment_type ==
439 if(!step.pc->source_location().get_line().empty())
448 step.get_lhs_object(),
457 if(!step.pc->source_location().get_file().empty())
461 if(!step.pc->source_location().get_line().empty())
464 << step.pc->source_location().get_line();
472 const auto &f_symbol = ns.
lookup(step.called_function);
473 out << f_symbol.display_name();
477 auto arg_strings =
make_range(step.function_arguments)
478 .map([&ns, &step](
const exprt &arg) {
479 return from_expr(ns, step.function_id, arg);
483 join_strings(out, arg_strings.begin(), arg_strings.end(),
", ");
522 unsigned prev_step_nr=0;
523 bool first_step=
true;
524 std::size_t function_depth=0;
526 for(
const auto &step : goto_trace.
steps)
539 if(!step.pc->source_location().is_nil())
546 if(step.pc->is_assert())
549 <<
from_expr(ns, step.function_id, step.original_condition)
558 if(step.cond_value && step.pc->is_assume())
561 out <<
"Assumption:\n";
563 if(!step.pc->source_location().is_nil())
566 out <<
" " <<
from_expr(ns, step.function_id, step.original_condition)
579 step.pc->is_assign() ||
580 step.pc->is_set_return_value() ||
581 step.pc->is_function_call() ||
582 (step.pc->is_other() && step.full_lhs.is_not_nil()))
584 if(prev_step_nr!=step.step_nr || first_step)
587 prev_step_nr=step.step_nr;
595 step.get_lhs_object(),
603 if(prev_step_nr!=step.step_nr || first_step)
606 prev_step_nr=step.step_nr;
612 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
619 printf_formatter(
id2string(step.format_string), step.io_args);
620 printf_formatter.
print(out);
626 out <<
" OUTPUT " << 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);
648 out <<
" INPUT " << step.io_id <<
':';
650 for(std::list<exprt>::const_iterator
651 l_it=step.io_args.begin();
652 l_it!=step.io_args.end();
655 if(l_it!=step.io_args.begin())
658 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
671 out <<
"\n#### Function call: " << step.called_function;
675 for(
auto &arg : step.function_arguments)
682 out <<
from_expr(ns, step.function_id, arg);
685 out <<
") (depth " << function_depth <<
") ####\n";
693 out <<
"\n#### Function return from " << step.function_id <<
" (depth "
694 << function_depth <<
") ####\n";
720 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
724 unsigned thread_to_show = 0;
726 for(
auto s_it = goto_trace.
steps.begin(); s_it != goto_trace.
steps.end();
729 const auto &step = *s_it;
730 auto &stack = call_stacks[step.thread_nr];
736 stack.push_back(s_it);
737 thread_to_show = step.thread_nr;
740 else if(step.is_function_call())
742 stack.push_back(s_it);
744 else if(step.is_function_return())
750 const auto &stack = call_stacks[thread_to_show];
753 for(
auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
755 const auto &step = **s_it;
758 out <<
" assertion failure";
759 if(!step.pc->source_location().is_nil())
763 else if(step.is_function_call())
765 out <<
" " << step.called_function;
769 for(
auto &arg : step.function_arguments)
776 out <<
from_expr(ns, step.function_id, arg);
781 if(!step.pc->source_location().is_nil())
807 std::set<irep_idt> property_ids;
808 for(
const auto &step :
steps)
810 if(step.is_assert() && !step.cond_value)
811 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)
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
struct configt::ansi_ct ansi_c
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.
bool is_constant() const
Return whether the expression is a constant.
Step of the trace of a GOTO program.
std::vector< exprt > function_arguments
bool is_function_call() const
bool is_assignment() const
goto_programt::const_targett pc
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
std::optional< symbol_exprt > get_lhs_object() const
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.
Fixed-width bit-vector with unsigned binary interpretation.
#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 std::optional< symbol_exprt > get_object_rec(const exprt &src)
bool is_index_member_symbol(const exprt &src)
static void trace_value(messaget::mstreamt &out, const namespacet &ns, const std::optional< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options)
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)
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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.