30 if(src.
id()==ID_symbol)
32 else if(src.
id()==ID_member)
34 else if(src.
id()==ID_index)
36 else if(src.
id()==ID_typecast)
49 std::ostream &out)
const 51 for(
const auto &step :
steps)
57 std::ostream &out)
const 73 out <<
"ATOMIC_BEGIN";
80 out <<
"FUNCTION RETURN";
break;
82 out <<
"unknown type: " <<
static_cast<int>(
type) << std::endl;
103 if(!
pc->source_location.is_nil())
104 out <<
pc->source_location <<
'\n';
106 out <<
pc->type <<
'\n';
112 out <<
"Violated property:" <<
'\n';
113 if(
pc->source_location.is_nil())
114 out <<
" " <<
pc->source_location <<
'\n';
119 out <<
" " <<
format(
pc->guard) <<
'\n';
145 const typet &underlying_type =
146 expr_type.
id() == ID_c_enum_tag
167 std::ostringstream oss;
169 for(
const auto c : result)
172 if(++i % 8 == 0 && result.size() != i)
176 return prefix + oss.str();
188 if(expr.
id()==ID_constant)
190 if(type.
id()==ID_unsignedbv ||
191 type.
id()==ID_signedbv ||
193 type.
id()==ID_fixedbv ||
194 type.
id()==ID_floatbv ||
195 type.
id()==ID_pointer ||
196 type.
id()==ID_c_bit_field ||
197 type.
id()==ID_c_bool ||
198 type.
id()==ID_c_enum ||
199 type.
id()==ID_c_enum_tag)
203 else if(type.
id()==ID_bool)
207 else if(type.
id()==ID_integer)
210 if(i.has_value() && *i >= 0)
219 else if(expr.
id()==ID_array)
234 else if(expr.
id()==ID_struct)
236 std::string result=
"{ ";
247 else if(expr.
id()==ID_union)
260 const exprt &full_lhs,
266 if(lhs_object.has_value())
267 identifier=lhs_object->get_identifier();
269 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
272 out <<
"(assignment removed)";
290 const auto &source_location = state.
pc->source_location;
292 if(!source_location.get_file().empty())
293 result +=
"file " +
id2string(source_location.get_file());
303 if(!source_location.get_line().empty())
307 result +=
"line " +
id2string(source_location.get_line());
327 out <<
"Initial State";
329 out <<
"State " << step_nr;
332 out <<
"----------------------------------------------------" <<
'\n';
337 out <<
"----------------------------------------------------" <<
'\n';
343 if(src.
id()==ID_index)
345 else if(src.
id()==ID_member)
347 else if(src.
id()==ID_symbol)
364 std::size_t function_depth = 0;
366 for(
const auto &step : goto_trace.
steps)
368 if(step.is_function_call())
370 else if(step.is_function_return())
384 if(!step.pc->source_location.is_nil())
389 if(step.pc->is_assert())
390 out <<
" " <<
from_expr(ns, step.function, step.pc->guard) <<
'\n';
398 step.assignment_type ==
406 if(!step.pc->source_location.get_line().empty())
415 step.get_lhs_object(),
424 if(!step.pc->source_location.get_file().empty())
428 if(!step.pc->source_location.get_line().empty())
438 const auto &f_symbol = ns.
lookup(step.called_function);
439 out << f_symbol.display_name();
443 auto arg_strings =
make_range(step.function_arguments)
444 .map([&ns, &step](
const exprt &arg) {
445 return from_expr(ns, step.function, arg);
449 join_strings(out, arg_strings.begin(), arg_strings.end(),
", ");
485 unsigned prev_step_nr=0;
486 bool first_step=
true;
487 std::size_t function_depth=0;
489 for(
const auto &step : goto_trace.
steps)
502 if(!step.pc->source_location.is_nil())
509 if(step.pc->is_assert())
510 out <<
" " <<
from_expr(ns, step.function, step.pc->guard) <<
'\n';
520 out <<
"Violated assumption:" <<
'\n';
521 if(!step.pc->source_location.is_nil())
524 if(step.pc->is_assume())
525 out <<
" " <<
from_expr(ns, step.function, step.pc->guard) <<
'\n';
538 if(step.pc->is_assign() ||
539 step.pc->is_return() ||
540 step.pc->is_function_call() ||
541 (step.pc->is_other() && step.full_lhs.is_not_nil()))
543 if(prev_step_nr!=step.step_nr || first_step)
546 prev_step_nr=step.step_nr;
554 step.get_lhs_object(),
562 if(prev_step_nr!=step.step_nr || first_step)
565 prev_step_nr=step.step_nr;
571 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
578 printf_formatter(
id2string(step.format_string), step.io_args);
579 printf_formatter.
print(out);
585 out <<
" OUTPUT " << step.io_id <<
':';
587 for(std::list<exprt>::const_iterator
588 l_it=step.io_args.begin();
589 l_it!=step.io_args.end();
592 if(l_it!=step.io_args.begin())
595 out <<
' ' <<
from_expr(ns, step.function, *l_it);
607 out <<
" INPUT " << step.io_id <<
':';
609 for(std::list<exprt>::const_iterator
610 l_it=step.io_args.begin();
611 l_it!=step.io_args.end();
614 if(l_it!=step.io_args.begin())
617 out <<
' ' <<
from_expr(ns, step.function, *l_it);
630 out <<
"\n#### Function call: " << step.called_function;
634 for(
auto &arg : step.function_arguments)
641 out <<
from_expr(ns, step.function, arg);
644 out <<
") (depth " << function_depth <<
") ####\n";
652 out <<
"\n#### Function return from " << step.function <<
" (depth " 653 << function_depth <<
") ####\n";
679 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
683 unsigned thread_to_show = 0;
685 for(
auto s_it = goto_trace.
steps.begin(); s_it != goto_trace.
steps.end();
688 const auto &step = *s_it;
689 auto &
stack = call_stacks[step.thread_nr];
695 stack.push_back(s_it);
696 thread_to_show = step.thread_nr;
699 else if(step.is_function_call())
701 stack.push_back(s_it);
703 else if(step.is_function_return())
709 const auto &
stack = call_stacks[thread_to_show];
712 for(
auto s_it =
stack.rbegin(); s_it !=
stack.rend(); s_it++)
714 const auto &step = **s_it;
717 out <<
" assertion failure";
718 if(!step.pc->source_location.is_nil())
722 else if(step.is_function_call())
724 out <<
" " << step.called_function;
728 for(
auto &arg : step.function_arguments)
735 out <<
from_expr(ns, step.function, arg);
740 if(!step.pc->source_location.is_nil())
The type of an expression, extends irept.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
void show_state_header(messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
A constant literal expression.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
static const commandt reset
return to default formatting, as defined by the terminal
goto_programt::const_targett pc
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Stream & join_strings(Stream &os, const It b, const It e, const Delimiter &delimiter)
Prints items to an stream, separated by a constant delimiter.
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
bool is_function_call() const
const irep_idt & id() const
bool is_index_member_symbol(const exprt &src)
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Ranges: pair of begin and end iterators, which can be initialized from containers, provide useful methods such as map, filter and concat which only manipulate iterators, and can be used with ranged-for.
source_locationt source_location
nonstd::optional< T > optionalt
static const commandt red
render text with red foreground color
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
optionalt< symbol_exprt > get_lhs_object() const
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
ranget< iteratort > make_range(iteratort begin, iteratort end)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
std::size_t get_width() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
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)
const irep_idt & display_name() const
Return language specific display name if present.
static const commandt faint
render text with faint font
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
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, 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.
Base class for all expressions.
const exprt & struct_op() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
#define UNREACHABLE
This should be used to mark dead code.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool is_assignment() const
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
static const trace_optionst default_options
const typet & subtype() const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().